25 Formalized Content Not Yet Written Up Individually

The chapters above are hand-written narrative treatments. This chapter closes the gap between that narrative and the repository: every module below contains kernel-checked results that had no blueprint entry before 2026-08-31. Each section names the module, its own stated source, and its principal results, all of which carry .

These entries are deliberately terse — they record what is proved and where, so nothing formalized is invisible. Promoting a thread to a full narrative chapter above is separate work.

Declarations prefixed open_ are omitted throughout: those are open results parked as stubs, not theorems.

25.1 Riemann Hypothesis — Supporting Tower

25.1.1 GammaPlancherelDefect

This file formalizes the positive-kernel core of Theorem 62.1 in Toupin’s

Proved (28 declarations):

• digamma_add_nat

• archimedeanG_add_two_nat

• gammaDefect_even_eq_sum

• defectIntegrand_even_eq_expSum

• exp_resolvent_integrable

• evenShiftExpSum_integrable

• defectIntegrand_even_integrable

• defectKernel_even_eq_sum

• gammaDefect_even_eq_kernel

• evenShiftDefectSum_nonneg

• …and 18 further results in this module.

25.1.2 PrimeFermionDirac

The fermion/spinor analogy can be made exact at one prime. The exterior algebra on one

Proved (19 declarations):

• create

• annihilate

• grading

• grading_sq

• create_sq

• annihilate_sq

• car

• create_adjoint

• supercharge_sq

• supercharge_adjoint

• …and 9 further results in this module.

25.1.3 RHProofStructure

Sources:

Proved (17 declarations):

• gr24_betti

• gr24_euler_char

• gr24_over_Fq

• gr24_over_F1

• gr24_over_F2

• gr24_schubert_dims_sum

• canonical_dictionary_alpha

• dictionary_involution_compat

• casimir_eigenvalue

• plucker_weight

• …and 7 further results in this module.

25.1.4 CayleyDicksonFockBridge

The finite-prime fermionic construction and the Cayley–Dickson tower share one exact

Proved (14 declarations):

• fockDim

• cayleyDicksonDim

• fockDim_eq_cayleyDicksonDim

• fockDim_succ

• cayleyDicksonDim_succ

• common_doubling_step

• first_four_common_dimensions

• three_channel_dimension

• fourth_doubling_dimension

• finiteHodgeEnergy_nonneg

• …and 4 further results in this module.

25.1.5 PrimeDoubletDirac

The gap-two graph on the primes has an exact singlet/doublet decomposition above the

Proved (13 declarations):

• singletAdjacency

• doubletAdjacency

• symmetricState

• antisymmetricState

• doubletAdjacency_eq_dirac_one

• doubletAdjacency_selfAdjoint

• doubletAdjacency_mulVec_symmetric

• doubletAdjacency_mulVec_antisymmetric

• antisymmetricState_ne_zero

• doubletAdjacency_not_posSemidef

• …and 3 further results in this module.

25.1.6 CayleyDicksonFockOperator

This file isolates the exact algebraic hypotheses needed for the multi-channel Hodge–Dirac

Proved (11 declarations):

• coeff_conj_pair

• coeff_swap_cancel

• pairSum_swap

• pairSum_eq_neg

• pairSum_eq_zero

• supercharge_sq_eq_pairSum

• supercharge_sq_zero

• mixed_products_eq

• mixed_products_eq_energy

• dirac_sq_energy

• …and 1 further results in this module.

25.1.7 PadicHaarTransfer

Step 5 of the ‘ℚ_p^ב-scaling-law plan (‘PadicMultiplicativeMeasure.lean‘), executed: the

Proved (11 declarations):

• coeAddHom

• range_coeAddHom

• isOpenEmbedding_coeAddHom

• comap_apply

• isAddHaarMeasure_comap

• isProbabilityMeasure_comap

• isProbabilityMeasure_haarMeasure

• comap_eq_haarMeasure

• fieldHaarMeasure_image

• image_span_pow_eq_closedBall

• …and 1 further results in this module.

25.1.8 QuartetPerturbation

Thread Q of ‘docs/FORMALIZATION_PLAN.md‘, from the entanglement/shadow-positivity memo

Proved (11 declarations):

• sq_coords

• quartet_contribution

• pair_contribution

• quartet_neg_of_cos_neg

• cos_neg_of_quartet_neg

• quartet_amplification

• positiveType_comp_addMonoidHom

• cesaro_gram_sq_nonneg

• below

• abel_state_comp_neg_eq

• …and 1 further results in this module.

25.1.9 SechFourthIntegral

Thread A2 of ‘docs/FORMALIZATION_PLAN.md‘: the exact value of the Yakaboylu eigenstate

Proved (11 declarations):

• one_div_cosh_sq

• hasDerivAt_tanh’

• hasDerivAt_sechFourthAntideriv

• sechFourthAntideriv_zero

• one_div_cosh_sq_le

• tendsto_sechFourthAntideriv

• integral_id_div_cosh_fourth

• hasDerivAt_tHalfAntideriv

• tendsto_tHalfAntideriv

• integral_t_div_cosh_half_fourth

• …and 1 further results in this module.

25.1.10 CauchyKernelPositive

Thread K of ‘docs/FORMALIZATION_PLAN.md‘, companion to the form-domain note on Yakaboylu

Proved (10 declarations):

• integrableOn_exp_neg_mul_cos

• hasDerivAt_dampedCosAntideriv

• tendsto_dampedCosAntideriv

• integral_exp_neg_mul_cos

• cauchy_kernel_eq_integral

• cauchy_kernel_positive_type

• matrix_element_on_line

• matrix_element_off_line_diag

• off_line_diag_neg

• tendsto_offline_min_eigenvalue

25.1.11 PrimeGreenAmplitude

This is the next bridge after ‘EulerFactorLogDeriv.lean‘. The nonzero Fourier modes of

Proved (10 declarations):

• primePowerBoundaryWeight_pos

• primePowerBoundaryLocation_pos

• primePowerBoundaryWeight_eq_coeff

• primePowerBoundaryLocation_eq_frequency

• massiveGreenAtZero_pos

• boundaryWeight_mul_green_eq

• finitePrimeGreenAmplitude_eq

• finitePrimeGreenAmplitude_nonneg

• finitePrimeDirichletAmplitude_nonneg

• crossTerm_eq_doubled_norm_difference

25.1.12 ZetaGibbsFisher

For real ‘β > 1‘, logarithmic derivatives of zeta are exactly Gibbs cumulants of

Proved (10 declarations):

• zetaVarianceResponse_eq_ofReal_logEnergyVariance

• zetaThirdCumulantResponse_eq_ofReal_logEnergyThirdCumulant

• logEnergyVariance_nonneg

• zetaVarianceResponse_im_eq_zero

• zetaThirdCumulantResponse_im_eq_zero

• zetaVarianceResponse_re_nonneg

• heatCapacity_nonneg

• entropyBetaDerivative_nonpos

• entropyBetaDerivative_sq_eq_heatCapacity_mul_variance

• entropyBetaDerivative_sq_nonneg

25.1.13 ZetaGibbsMoments

On the half-plane ‘Re s > 1‘, the Riemann zeta function is exactly the L-series

Proved (10 declarations):

• zetaHalfPlane

• isOpen_zetaHalfPlane

• riemannZeta_eq_LSeries_one

• riemannZeta_eqOn_LSeries_one

• iteratedDeriv_riemannZeta_eq_iteratedDeriv_LSeries_one

• iteratedDeriv_riemannZeta_eq_logMomentLSeries

• deriv_riemannZeta_eq_neg_logMomentLSeries

• iteratedDeriv_two_riemannZeta_eq_logSqMomentLSeries

• iteratedDeriv_three_riemannZeta_eq_neg_logCubeMomentLSeries

• iteratedDeriv_four_riemannZeta_eq_logFourthMomentLSeries

25.1.14 VonMangoldtCosineBridge

This file simplifies the real part of each absolutely-convergent von-Mangoldt

Proved (9 declarations):

• natCast_neg_cpow_re

• vonMangoldt_term_re_eq_exp_cos

• vonMangoldt_term_zero_re

• neg_zeta_logDeriv_re_eq_vonMangoldt_cosine_tsum

• cosine_frequency_positiveType

• positiveType_nonneg_scalar

• vonMangoldt_mode_positiveType

• positiveType_finset_sum_modes

• finite_vonMangoldt_cosine_positiveType

25.1.15 HaarPositivityWeil

Source: haar_positivity_weil_wightman.tex

Proved (8 declarations):

• PositiveType

• const_one_positive_type

• positive_type_at_zero

• finiteHaarProjection_isIdempotentElem

• finiteSum_end_apply

• finiteHaarProjection_range_eq_invariants

• finiteHaarProjection_isSelfAdjoint

• haar_squares_always_positive

25.1.16 PositiveDefiniteGNS

Source: haar_positivity_weil_wightman.tex, thm:gns-positive. Closes the stub open_gns_from_positive_type (2026-09-26).

Construction. Kolmogorov’s: the form \(\langle \delta _x, \delta _y\rangle = P(x^{-1}y)\) on finitely supported functions \(G \to _0 \mathbb {C}\) is a semi-inner product (Hermitian symmetry is GppFiniteGNS.PositiveDefinite.conj_symm); Mathlib’s PreInnerProductSpace.Core accepts it as is, and the Hilbert space is the completion. Left translation preserves the form, so it extends to unitaries on the completion.

Why this sat as a stub. It was labelled a library gap twice: first “GNS not in Mathlib”, then “Mathlib has GNS for C\(^\star \)-algebras; the missing bridge is a C\(^\star \)-norm on the group algebra”. The second was true of the C\(^\star \) route, and the route was not needed: a representation of the group never passes through the group C\(^\star \)-algebra.

What this does not give. Bochner’s theorem (a continuous positive-definite function on \(\mathbb {R}\) is the Fourier transform of a finite positive measure), which needs the spectral theorem for the one-parameter group \(\pi \); and continuity of \(\pi \), which needs continuity of \(P\).

25.1.17 ZetaGibbsSummability

For real ‘β > 1‘ the three real series needed for the Gibbs variance,

Proved (8 declarations):

• constant_abscissa_le_one

• real_log_abscissa_le_one

• real_log_sq_abscissa_le_one

• summable_gibbsWeight

• summable_gibbsWeight_mul_logEnergy

• summable_gibbsWeight_mul_logEnergy_sq

• gibbsWeight_tsum_pos

• gibbs_logEnergy_variance_nonneg

25.1.18 FiniteFisherMomentBridge

This module isolates the scalar algebra sitting between the finite-support

Proved (7 declarations):

• fisherDet

• fisherNumerator

• momentDiscriminant

• six_fisherNumerator_eq_mass_mul_momentDiscriminant

• fisherNumerator_one_eq_fisherDet

• momentDiscriminant_one_eq_six_fisherDet

• six_fisherDet_eq_momentDiscriminant_one

25.1.19 LiCriterion

Task #75 (long pending): a second equivalence for RH. Li’s criterion (Li 1997) states

Proved (7 declarations):

• riemannXi_entire

• riemannXi_one

• hasDerivAt_mul_sub_one_at_one

• deriv_riemannXi_one

• li_lambda_one

• eulerMascheroniConstant_gt_log_four_pi_sub_two

• li_lambda_one_pos

25.1.20 PadicFullZetaIntegral

Continuing toward the full geometric-series zeta integral (Tate’s-thesis lecture notes,

Proved (7 declarations):

• shell

• measurableSet_shell

• mem_shell_valuation

• shell_pairwise_disjoint

• univ_eq_shells

• singleton_disjoint_shells

• measurableSet_shell_iUnion

25.1.21 TruncatedTransport

Thread T. The memo’s section 6.1 transport question is blocked at the idele-class-group

Proved (7 declarations):

• PositiveTypeOn

• positiveTypeOn_real_iff

• that

• positiveTypeOn_comp_addMonoidHom

• truncatedLogHom

• truncated_transport

• logPrime_lattice_injective

25.1.22 WeilSupportLadder

Thread L of ‘docs/FORMALIZATION_PLAN.md‘, after Connes–Consani (arXiv:2106.01715, §2.2):

Proved (7 declarations):

• HasSupportIn

• convolution_hasSupportIn

• primeSide_term_eq_zero

• primeSide_eq_truncation

• primeSide_eq_zero_of_support_lt_log_two

• weil_nonneg_of_arch_nonneg_rung_zero

• integral_exp_neg_abs_mul_cos

25.1.23 ZetaFisherStrictMonotonicity

For ‘β > 1‘ the Fisher metric has the positive arithmetic expansion

Proved (7 declarations):

• logMul_term_re_eq_fisherSummand

• summable_fisherSummand

• fisherSummand_nonneg

• fisherSummand_antitone_pair

• fisherSummand_two_strict

• fisher_tsum_strictAnti

• logMul_vonMangoldt_re_eq_fisher_tsum

25.1.24 ZetaGibbsMomentBridge

For real ‘β > 1‘, the constant-one L-series and its first four logarithmic coefficient

Proved (7 declarations):

• natSucc_cpow_eq_ofReal_rpow

• natSucc_clog_eq_ofReal_log

• LSeries_one_eq_ofReal_gibbsWeight_tsum

• LSeries_logMul_one_eq_ofReal_firstMoment

• LSeries_logMul_logMul_one_eq_ofReal_secondMoment

• LSeries_logMul_logMul_logMul_one_eq_ofReal_thirdMoment

• LSeries_logMul_four_one_eq_ofReal_fourthMoment

25.1.25 AlternatingHarmonicLog2

Thread C1 of ‘docs/FORMALIZATION_PLAN.md‘: ‘η(1) = log 2‘ in its classical series form —

Proved (6 declarations):

• integral_one_div_one_add

• sum_neg_pow_eq

• log_two_sub_partial

• remainder_pointwise

• remainder_bound

• tendsto_alternating_harmonic_log_two

25.1.26 CompletedZetaDerivativeSymmetry

Mathlib proves the completed functional equation

Proved (6 declarations):

• one_sub_ne_zero

• one_sub_ne_one

• completedRiemannZeta_deriv_reflection

• completedRiemannZeta_deriv_one_sub

• completedRiemannZeta_logDeriv_reflection

• completedRiemannZeta_deriv_one_half

25.1.27 FinitePrimeDiracCompletion

This file specializes the abstract finite CAR/Koszul Hodge–Dirac theorem to the actual

Proved (6 declarations):

• finitePrimeDirac_sq

• add_sq_of_anticommute

• completed_sq_of_clifford_orthogonal

• cross_term_forced_of_completed_zero

• positive_energy_sum_ne_zero

• completed_square_nonzero_of_positive_orthogonal

25.1.28 GlobalVonMangoldtBridge

On the half-plane of absolute convergence, Mathlib proves that the L-series of the

Proved (6 declarations):

• vonMangoldtLSeries_eq_neg_zeta_logDeriv

• riemannZeta_ne_zero_right_half_plane

• neg_zeta_logDeriv_eq_vonMangoldtLSeries

• neg_zeta_logDeriv_eq_tsum_vonMangoldt_terms

• neg_zeta_logDeriv_eq_tsum_vonMangoldt_div

• neg_zeta_logDeriv_re_eq_tsum_re_terms

25.1.29 HaarSubgroupIndex

Real infrastructure toward the p-adic/adelic integral computations underlying Tate’s

Proved (6 declarations):

• smul_eq_preimage_inv_mul

• measure_smul_set

• measurableSet_smul

• cosets_pairwise_disjoint

• index_smul_measure_eq_univ

• index_vadd_measure_eq_univ

25.1.30 PadicZetaIntegralClosedForm

The capstone of this session’s p-adic infrastructure thread: the exact geometric-series

Proved (6 declarations):

• normRpow_const_on_shell

• shell_term_eq

• lintegral_norm_rpow

• lintegral_norm_rpow_zero

• lintegral_norm_rpow_one

• tate_local_zeta_integral

25.1.31 PrimeFisherMomentSummability

For ‘β > 1‘, the repaired all-order ‘logMul‘ convergence theorem implies absolute

Proved (6 declarations):

• iterated_logMul_apply_general

• iterated_logMul_apply

• natCast_neg_cpow_eq_ofReal_exp

• iterated_logMul_term_eq_ofReal_fisher_moment

• iterated_logMul_term_re_eq_fisher_moment

• summable_fisherWeight_mul_log_pow

25.1.32 PrimeHankelGram

Proved (6 declarations):

• finite_weighted_polynomial_gram_nonneg

• finite_type_weighted_polynomial_gram_nonneg

• two_support_hankel_det_pos

• two_support_hankel_det_factor

• three_support_hankel_det_factor

• three_support_hankel_det_pos

25.1.33 ThermalCriticalLineBridge

This file packages exact facts motivating a thermal interpretation of the Riemann critical line

Proved (6 declarations):

• equilibrium_involution_iff_critical_line

• principalSeries_gamma_modulus_eq_planck_weight

• planck_weight_first_moment

• planck_weight_third_moment

• completed_partition_im_zero

• equilibrium_response_re_zero

25.1.34 VonMangoldtCubicPositivity

For real ‘β > 1‘, the arithmetic series

Proved (6 declarations):

• logMul_logMul_term_re_eq_cubicSummand

• summable_cubicSummand

• cubicSummand_nonneg

• cubicSummand_two_pos

• tsum_cubicSummand_pos

• logMul_logMul_vonMangoldt_re_pos

25.1.35 ArchimedeanEulerNonvanishing

The completed zeta factorization is multiplicative at the local-factor level. This file

Proved (5 declarations):

• gamma_half_ne_zero_of_re_pos

• archFactor_ne_zero_of_re_pos

• eulerHolonomy_ne_zero_of_re_pos

• finiteEulerProduct_ne_zero_of_re_pos

• finiteCompletedLocalProduct_ne_zero

25.1.36 ConvolutionSquarePositive

Thread B of ‘docs/FORMALIZATION_PLAN.md‘. ‘HaarPositivityWeil.lean‘ (PR #45) honestly

Proved (5 declarations):

• integrable_shift_mul_shift

• convolution_shift

• mul_ofReal_re

• gram_square_nonneg

• convolution_square_positive_type

25.1.37 EigenstateNormStrip

Thread A1 of ‘docs/FORMALIZATION_PLAN.md‘: for every ‘σ > 0‘ (in particular throughout the

Proved (5 declarations):

• one_div_cosh_fourth_le

• integrableOn_eigenstateNorm_integrand

• eigenstateNorm_integral_pos

• eigenstateNorm_pos

• eigenstateNorm_at_half

25.1.38 GlobalCompletedFactorization

Mathlib’s analytically continued completed zeta function satisfies, away from ‘s = 0‘,

Proved (5 declarations):

• completedRiemannZeta_eq_GammaR_mul_zeta

• completedRiemannZeta_eq_zero_iff_zeta_eq_zero

• criticalStrip_completed_zero_iff_zeta_zero

• criticalLine_completed_zero_iff_zeta_zero

• criticalLine_not_in_vonMangoldt_convergence_halfplane

25.1.39 NumberEntropy

This file isolates the canonical thermodynamics of the zeta / prime-gas system in the

Proved (5 declarations):

• integer_partition_sum_eq_zeta

• integerGibbsWeight_tsum_eq_one

• numberEntropy_eq_logZ_add_sU

• internalEnergy_eq_vonMangoldt

• numberEntropy_eq_logZ_add_vonMangoldt

25.1.40 VonMangoldtCumulantDerivativeBridge

On the open half-plane ‘Re s > 1‘, the genuine negative logarithmic derivative

Proved (5 declarations):

• negZetaLogDeriv_eqOn_vonMangoldtLSeries

• iteratedDeriv_negZetaLogDeriv_eq_logMomentLSeries

• iteratedDeriv_two_negZetaLogDeriv_eq_logMul_logMul

• iteratedDeriv_three_negZetaLogDeriv_eq_neg_logMul_three

• iteratedDeriv_two_negZetaLogDeriv_re_pos

25.1.41 BlackbodyMellinZeta

(‘blackbody_law_qg_dtoupin_v1.tex‘), which states that "the Riemann zeta function is

Proved (4 declarations):

• hasSum_exp_planckKernel

• mellin_planckKernel_eq

• hasSum_exp_oddPlanckKernel

• mellin_oddPlanckKernel_eq

25.1.42 CompletedZetaReality

The completed zeta function has two exact symmetries:

Proved (4 declarations):

• GammaR_conj

• completedZeta_eq_GammaR_mul_zeta

• completedRiemannZeta_conj

• completedRiemannZeta_im_eq_zero_of_re_half

25.1.43 FiniteCompletedFactorNonvanishing

‘ArchimedeanEulerNonvanishing.lean‘ proves nonvanishing for the Euler holonomies

Proved (4 declarations):

• zetaP_ne_zero_of_re_pos

• finiteEulerZetaProduct_ne_zero_of_re_pos

• finiteCompletedZetaProduct_ne_zero_of_re_pos

• finiteCompletedZetaProduct_critical_ne_zero

25.1.44 FiniteVandermondeEnergy

This module isolates the positivity half of the general finite-support

Proved (4 declarations):

• orderedVandermondeEnergy

• weighted_vandermonde_sq_nonneg

• weighted_vandermonde_sq_pos

• orderedVandermondeEnergy_nonneg

25.1.45 IdeleGroup

Not paper-sourced — genuine new infrastructure, building on Mathlib’s

Proved (4 declarations):

• resolution

• RationalIdeleGroup

• diagonalEmbedding_injective

• adicCompletionIntegers_toSubring_eq_integer

25.1.46 PrimeHankelInfiniteLift

A strictly positive finite truncation of a summable nonnegative series forces the

Proved (4 declarations):

• tsum_pos_of_finite_sum_pos

• weighted_sq_tsum_pos

• finite_weighted_eval_comp_sq_sum_pos

• weighted_polynomial_tsum_pos

25.1.47 ScaleMassDiagnostic

For a positive scale ‘a‘, the half-density-normalized multiplicative character is

Proved (4 declarations):

• norm_dilationCharacter

• critical_line_dilation_unitary

• critical_line_of_dilation_unitary

• critical_line_iff_dilation_unitary

25.1.48 ScaleShadowHalfDensity

For

Proved (4 declarations):

• shadow_centered_exponent

• dilationCharacter_shadow_eq_inv

• dilationCharacter_shadow_involution

• critical_line_iff_unitary_with_shadow

25.1.49 VonMangoldtCumulantSummability

The strict zeta-Gibbs cumulant signs require more than termwise positivity: the

Proved (4 declarations):

• abscissa_vonMangoldtComplex_le_one

• summable_logMul_vonMangoldt

• summable_logMul_logMul_vonMangoldt

• summable_iterated_logMul_vonMangoldt

25.1.50 LogDerivativeProduct

At the local-factor level Tate completion is multiplicative. The logarithmic derivative

Proved (3 declarations):

• neg_logDeriv_mul_algebra

• neg_logDeriv_product_of_hasDerivAt

• hasDerivAt_completed_product

25.1.51 MomentumGeneratorNoPointSpectrum

Source: On the Nature of Nature v5.2.1.3 (Zenodo record 21260806, "On the Nature of Nature: Celestial

Proved (3 declarations):

• not_isFiniteMeasure_volume_real

• rotation_normSq_const

• no_nonzero_globally_L2_rotation_solution

25.1.52 PadicEulerFactorBridge

Mathlib already proves the Euler product for the Riemann zeta function:

Proved (3 declarations):

• riemannZeta_factor_eq_ofReal

• euler_factor_toReal_eq

• euler_factor_bridge

25.1.53 PrimeHankelPolynomialSummability

Once every weighted monomial ‘w n * x n ^ r‘ is summable, finite polynomial

Proved (3 declarations):

• summable_weight_mul_polynomial_eval

• summable_weight_mul_polynomial_eval_sq

• summable_fisherWeight_mul_polynomial_eval_sq

25.1.54 PrimeOccupationBridge

The local Euler logarithmic derivative has exactly the algebraic form of a geometric

Proved (3 declarations):

• occupation_recursion

• minusLogDerivZetaP_eq_log_mul_occupation

• minusLogDerivZetaP_eq_bose

25.1.55 SchurWeilClass

Thread S2 (the composition step of the S-truncated transport programme). The classical

Proved (3 declarations):

• positiveType_weighted_gram

• positiveType_mul_convSquare

• cauchyKernel_mul_convSquare_positive_type

25.1.56 TwoPointCriterion

Thread D2. ‘rh_iff_weil_pairedForm_nonneg‘ (Thread D, PR #65) proved RH equivalent to

Proved (3 declarations):

• involution_fixed_of_two_point_nonneg

• rh_iff_two_point_pairedForm_nonneg

• rh_of_two_point_pairedForm_nonneg

25.1.57 WeightedVarianceFinite

This file isolates the algebraic positivity mechanism needed by the zeta Gibbs/Fisher

Proved (3 declarations):

• weighted_first_moment_sq_le

• weighted_variance_numerator_nonneg

• normalized_weighted_variance_nonneg

25.1.58 YakaboyluPositivityKernel

The final step of Yakaboylu, *Nontrivial Riemann Zeros as Spectrum* (arXiv:2408.15135v14,

Proved (3 declarations):

• swap_test_vector_exists

• swap_test_vector_value

• diagonal_form_nonneg

25.1.59 ArchimedeanZetaIntegral

Tate’s thesis needs a local factor at every place of ‘ℚ‘, including the archimedean

Proved (2 declarations):

• archimedean_zeta_integral

• archimedean_zeta_integral_one

25.1.60 CasimirIdentity

Source: verify_blackbody_capstone.py (companion to "The Blackbody Law of

Proved (2 declarations):

• casimir_eq_neg_riemann_form

• casimir_value

25.1.61 CompletedLogDerivativeBridge

The earlier version of this file attempted to formalize several finite-product derivative

Proved (2 declarations):

• realArchFactor_ne_zero

• finiteWp_eq_two_mul_re_finitePrimeLogDerivative

25.1.62 FiniteMomentFactorization

A bookkeeping lemma for the arbitrary finite-support Fisher/Vandermonde identity.

Proved (2 declarations):

• rawMoment

• triple_monomial_factorization

25.1.63 PadicFieldHaarMeasure

The first brick toward a genuine multiplicative Haar measure on ‘ℚ_p^ב (Tate’s-thesis

Proved (2 declarations):

• to

• fieldHaarMeasure_closedBall

25.1.64 PadicIndexPn

Real infrastructure toward Tate’s-thesis p-adic zeta integral (the newly uploaded lecture

Proved (2 declarations):

• toZModPow_surjective

• card_quotient_span_pow

25.1.65 PadicMultiplicativeMeasure

Tate’s-thesis local zeta integrals are stated against the *multiplicative* Haar measure

Proved (2 declarations):

• in

• measurable_multiplicativeDensity

25.1.66 PadicScalingHaar

First concrete step toward the ‘ℚ_p^ב-scaling law documented in

Proved (2 declarations):

• isAddHaarMeasure_map_scaleAddEquiv

• map_scaleAddEquiv_apply

25.1.67 PadicShellMeasure

Real infrastructure continuing the p-adic zeta integral thread (Tate’s-thesis lecture

Proved (2 declarations):

• measurableSet_span_pow

• haarMeasure_shell

25.1.68 PrimeHankelFisherSpecialization

This file instantiates the abstract infinite weighted-polynomial positivity theorem

Proved (2 declarations):

• fisherWeight_nonneg

• fisher_polynomial_tsum_pos

25.1.69 PrimeHankelRootEscape

A nonzero real polynomial of degree at most ‘N‘ cannot vanish on ‘N+1‘

Proved (2 declarations):

• exists_eval_ne_zero_of_natDegree_lt_card

• exists_eval_ne_zero_of_card_gt_degree_bound

25.1.70 SpectralWeil

This file formalizes ‘thm:spectral-weil‘ (On the Nature of Nature v5.2, cited 10×):

Proved (1 declaration):

• test_function_fe_symmetric

Open (1 declaration):

• open_digamma_series_form — a True-stub. It carried \leanok until 2026-08-31, i.e. this blueprint published it as machine-verified while it asserted nothing. It was unprefixed at the time and so invisible to the stub-naming gate; see §26.

  Narrowed 2026-09-02. The stub is still open, but it now stands for one step rather than for the whole series. RiemannHypothesis/DigammaSeries.lean proves, unconditionally, that the Gauss series converges absolutely off the non-positive integers (), that it satisfies \(F(s+1) = F(s) + 1/s\) — the functional equation Mathlib’s Complex.digamma_apply_add_one proves for \(\psi \) — (), and that at \(s = 1\) it telescopes to \(-\gamma \), agreeing with Complex.digamma_one (). Mathlib derives that value from the derivative of \(\Gamma \) at \(1\), so the agreement is a genuine check of the formula at a point.

  What remains is the identification \(F = \psi \) itself. The difference of the two is \(1\)-periodic and vanishes at \(1\); eliminating it requires a growth or convexity input (Wielandt / Bohr–Mollerup uniqueness), which is a library gap: Mathlib 4.33.1 has Complex.digamma but lists Gauss’ representation under TODO in its own module header.

25.1.71 WeightedVarianceInfinite

This file passes the finite weighted Cauchy–Schwarz inequality to an infinite

Proved (2 declarations):

• weighted_variance_numerator_nonneg_tsum

• normalized_weighted_variance_nonneg_tsum

25.1.72 CharacterOrthogonality

Source: Tate’s-thesis lecture notes (Warwick "tateweek4" notes, Lemma 4.15/Example 4.16)

Proved (1 declaration):

• integral_eq_zero_of_ne_one

25.1.73 FiniteVandermondeExpansionKernel

Pointwise polynomial expansion underlying the arbitrary finite-support

Proved (1 declaration):

• vandermonde_sq_expansion

25.1.74 GramPositivityBoundary

Yakaboylu (arXiv:2408.15135v15) constructs ‘V̂ := ∫₀^∞ ω(t)⁻² |t⟩⟨t| dt‘ (eq. 42) and notes

Proved (1 declaration):

• gram_posSemidef

25.1.75 PadicHaarMeasure

Real infrastructure toward Tate’s-thesis local zeta integral computations (the p-adic

Proved (1 declaration):

• haarMeasure_univ

25.1.76 PadicOriginMeasure

Real infrastructure continuing the p-adic zeta integral thread (Tate’s-thesis lecture

Proved (1 declaration):

• haarMeasure_singleton_zero

25.1.77 PadicShellNorm

Real infrastructure continuing the p-adic zeta integral thread (Tate’s-thesis lecture

Proved (1 declaration):

• norm_eq_of_mem_shell

25.1.78 PadicZetaIntegral

The payoff of ‘HaarSubgroupIndex.lean‘ + ‘PadicHaarMeasure.lean‘ + ‘PadicIndexPn.lean‘: the

Proved (1 declaration):

• haarMeasure_span_pow

25.1.79 PrimeFockPartition

The occupation-basis (sum) side of the prime-gas dictionary, which the Euler-product form does not give: configurations of the primon gas biject with the positive integers, so the spectrum is non-degenerate and equal to \(\{ \log N : N \geq 1\} \), and the partition function \(\sum _n e^{-sE(n)}\) is \(\zeta (s)\) on \(\operatorname {Re} s {\gt} 1\). All of it is unique factorization; no Fock space, Hamiltonian or Hilbert space is constructed, and there is no critical-strip content.

Proved (4 declarations):

• occEnergy_injective

• occEnergy_range

• exp_occEnergy_range

• partition_eq_riemannZeta

25.1.80 PrimeGasPartition

For a prime mode ‘p‘, the local Euler factor

Proved (1 declaration):

• partition_eq_riemannZeta

25.1.81 PrimeHankelFiniteGramStrict

This file packages the root-escape theorem into the exact positivity statement

Proved (1 declaration):

• weighted_eval_sq_sum_pos

25.2 Riemann Hypothesis — Codex Workbench Formalizations (2026-09-28)

Exact results from Codex’s GPPDiscovery2 workbench and queue, formalized here. None of these proves or assumes RH; each entry states its scope.

25.2.1 ArchimedeanFloor

An unconditional lower bound on the archimedean term of Weil’s explicit formula: for every test profile \(r\) with \(r(0)=1\) and \(r\le 1\) on \((0,\infty )\), \(A_\infty (r)\ \ge \ -\gamma -\log \pi -\pi /2-3\log 2\).

Proved (10 declarations):

• antideriv_zero

• continuous_antideriv

• hasDerivAt_antideriv

• constKernel_nonpos

• tendsto_antideriv

• archimedean_constant_integral

• integrableOn_constKernel

• archimedeanIntegrand_split

• archimedean_decomposition

• archimedean_floor

25.2.2 KMSCriticalLimit

The KMS state at inverse temperature \(\beta \) converges to the critical one quantitatively: \(\| c_1-c_\beta \| ^2\le (\beta -1)^2(\log N)^6\) for every \(N\ge 3\).

Proved (5 declarations):

• kmsDual_primePow

• midpoint_diff_bounds

• kms_term_bound

• kms_critical_limit

• kms_critical_limit_clean

25.2.3 HalfDensityZetaGauge

The half-density gauge on a divisor-closed set \(S\): the conjugated zeta and Möbius operators are mutually inverse (\(MZ=ZM=I\)), and \(MDZ-D=L_\Lambda \), i.e. conjugating the log-dilation \(D\) by the zeta gauge produces exactly the von Mangoldt operator.

Proved (13 declarations):

• filter_dvd_eq

• conv_apply

• halfConv_eq

• halfZeta_eq

• halfMobius_eq

• halfVonMangoldt_eq

• conv_lift_congr

• lift_halfZeta

• lift_halfMobius

• inv_sqrt_mul_lift

• halfMobius_halfZeta

• halfZeta_halfMobius

• half_density_gauge

25.2.4 SeedSynthesisBound

A Schur-test synthesis bound: if \(\langle v_m,v_n\rangle =(mn)^{-1/2}K(\log n-\log m)\) with \(|K(a)|\le Ae^{-q|a|}\) and \(q{\gt}\tfrac 12\), then \(\| \sum c_n v_n\| ^2\le A\bigl(2+\tfrac 1{q-1/2}+\tfrac 1{q+1/2}\bigr)\sum c_n^2\).

Proved (9 declarations):

• schurWeight_nonneg

• schurWeight_symm

• schurWeight_eq

• tail_sum_le

• head_sum_le

• rpow_pair

• schurWeight_row_sum

• schur_quadratic

• synthesis_bound

25.2.5 FixedWindowTransform

Closed form of the fixed-window transform \(H_\ell \) and its exact zero set: \(H_\ell (z)=0\) iff \(z=2\pi ik/\ell \) with \(k\ne 0\). Correction: the source note’s claim that \(H_\ell \) never vanishes at zeta exponents is false as stated; it vanishes exactly on that purely imaginary lattice (and never off the imaginary axis).

Proved (8 declarations):

• integral_right

• integral_left

• integrable_window

• windowTransform_eq

• windowTransform_eq_sinh

• windowTransform_zero

• windowTransform_eq_zero_iff

• windowTransform_ne_zero_of_re_ne_zero

25.2.6 CayleyLiHiggs

The Cayley variable \(u(t)=(t+i/2)/(t-i/2)=1-1/\rho \) for \(\rho =\tfrac 12+it\), and the two-sided bound \(0\le 1-\operatorname {Re}u^n\le n^2/(2(t^2+\tfrac 14))\), summed over any finite set of ordinates. Finite sums only; no statement about Li’s full criterion.

Proved (11 declarations):

• denom_ne_zero

• cayley_eq_li_ratio

• normSq_num

• normSq_den

• norm_cayley

• norm_one_sub_sq

• one_sub_re_cayley

• one_sub_re_pow_nonneg

• one_sub_re_pow_le_of_norm_one

• one_sub_re_pow_le

• finite_li_sum_bounds

25.2.7 OperatorValuedKoszulHomotopy

Operator-valued Koszul complex: with commuting inverses and CAR generators, \(dh+hd=1\) and \(d^2=0\); for any bounded contracting homotopy, \(\| \psi \| \le \sqrt2\, \| h\| \, \| (d+d^*)\psi \| \).

Proved (3 declarations):

• koszul_homotopy

• koszul_sq_zero

• norm_le_of_contracting_homotopy

25.2.8 PositiveFredholmFactor

For Hermitian \(A\), \(\det (I+cA)=\prod _i(1+c\lambda _i)\); if \(A\succeq 0\) then \(\det (I+z^2A)\) has zeros only on the imaginary axis. A negative eigenvalue produces a real zero.

Proved (5 declarations):

• positive_factor_zero

• det_one_add_smul_eq_prod

• fredholm_zero_on_imaginary_axis

• fredholm_ne_zero_off_axis

• negative_factor_real_zero

25.2.9 TFDParitySewing

Thermofield-double parity sewing: \(Q(I+xS)=I-xS\), the Cayley identity, parity currents, the Schur complement \(\tfrac 1{2q}\tfrac {1-x^2}{1+x^2}\), \(\det (I-\bigoplus _p x_pS)=\prod _p(1-x_p^2)\), and traces of \((xS)^m\).

Proved (14 declarations):

• coth_eq

• csch_eq

• tanh_eq

• one_sub_sq_ne

• Q_mul

• cayley_Q

• Q_inv

• \(\Gamma \)_symm

• \(\Gamma \)_anti

• parity_currents

• schur_complement

• det_one_sub_exchange

• det_block_exchange

• trace_exchange_pow

25.2.10 FisherZeroLogConcavityNoGo

A no-go: a log-concave density (\((\log q)''\le -A+\varepsilon b^2/(1-\varepsilon )\)) whose characteristic function nevertheless has the explicit off-axis zero \(t_0=(A/b)\bigl(\log (C_0+\sqrt{C_0^2-1})+i\pi \bigr)\). Log-concavity alone does not force real zeros.

Proved (10 declarations):

• density_pos

• gauss

• charFun_eq

• cosh_add_pi_I

• real_cosh_log

• charFun_zero

• one_add_pos

• hasDerivAt_log_density

• hasDerivAt_logDeriv1

• logDeriv2_le

25.2.11 HolographicReflectionPositivity

The finite core of arithmetic holography. For an involution \(\tau \) with positive \(\tau \)-invariant weights, the form \(Q(v)=\sum _z m_z v_z\overline{v_{\tau z}}\) is real, each mirror pair \(z\ne \tau z\) spans a hyperbolic plane (\(Q=\pm (m_z+m_{\tau z})\)), and \(Q\ge 0\) for all \(v\) iff \(\tau \) fixes every point. Finite algebra only; the passage to Weil’s criterion (explicit formula, independent prescribability of \(F(\rho )\)) is not formalized and is RH-strength.

Proved (4 declarations):

• reflectionForm_im

• reflectionForm_nonneg_of_fixed

• mirror_pair_indefinite

• reflectionForm_nonneg_iff

25.3 Thread Weil-Parity

25.3.1 OddEigenpairLift

From ‘public.formalization_queue‘ (Supabase project ‘dunrgpupddbmzffntwph‘), item

Proved (10 declarations):

• and

• CProj

• AplusBlock

• etaVec

• fromBlocks_mulVec_inr

• fromBlocks_mulVec_gen

• vecMulVec_mulVec’

• odd_eigenpair_defect_step1

• odd_eigenpair_defect_step2

• odd_eigenpair_canonical_lift

25.3.2 ArchimedeanTail

New thread, opened this session from ‘arithmetic_principal_series_RH_program34.tex‘,

Proved (5 declarations):

• archTailAntideriv_hasDerivAt

• archTailAntideriv_tendsto_atTop

• tail_integral

• tail_integral_closed_form

• archimedean_diagonal_tail

25.3.3 CrossResolvent

From ‘public.formalization_queue‘ (Supabase project ‘dunrgpupddbmzffntwph‘), section

Proved (4 declarations):

• cross_resolvent_det_identity

• vecMulVec_mulVec

• hermitian_dotProduct_mulVec

• parity_crossing_obstruction

25.4 Riemann Hypothesis — Gaussian Rigidity and the Hardy Kernel (2026-09-28)

Exact results from Codex’s 2026-09-27 GPPDiscovery2 notes, proved here in stronger form than her disposable checkers (which assumed the zeta constants and worked over \(\mathbb {R}\)). Neither uses or implies information about zeros.

25.4.1 FourComponentRigidity

In the number-circle Gaussian family \(Q_d=\frac1{2\pi }\sum _{a\le d}\sum _{n}G_{n,a}^2/n^2\), the mean \(\frac{d}{2\pi }\zeta (2)=\frac{d\pi }{12}\) equals \(2\xi (2)=\frac{\pi }{3}\) iff \(d=4\), with \(\Lambda (2)=\pi /6\) derived from Mathlib. The Laplace-transform product \(\prod _n(1+t/(\pi n^2))^{-d/2}\) converges to \((\sqrt{\pi t}/\sinh \sqrt{\pi t})^{d/2}\), which is \(P(\lambda )^{d/2}\) at \(t=\pi \lambda ^2\). The probabilistic steps and the full BPY identity are not formalized, and the count \(4\) is a property of the ansatz, not a spacetime dimension.

Proved (10 declarations):

• Gammaℝ_two

• completedRiemannZeta_two

• two_xi_two

• mean_radius

• component_count_forced

• sqrt_pi_mul

• tendsto_laplace_product

• sinh_div_pos

• tendsto_laplace_product_rpow

• laplace_at_pi_sq

25.4.2 CayleyHardyKernel

Over \(\mathbb {C}\): the Cayley map \(u\mapsto (1+u)/(1-u)\) sends the open disc exactly onto the right half-plane (\(\operatorname {Re}z=(1-|u|^2)/|1-u|^2\)); \(z+\bar\eta =2(1-u\bar v)/((1-u)(1-\bar v))\), so the half-plane Hardy kernel is a gauge factor times the disc kernel \((1-u\bar v)^{-1}\); and \(\zeta (1+q)-1/q\to \gamma \), so the Dirichlet–Hardy kernel \(\zeta (1+z+\bar\eta )\) is that Hardy kernel plus a part bounded at the boundary. The \(SU(1,1)\), \(k=\tfrac 12\) reading is a match of kernel shapes and is not formalized.

Proved (6 declarations):

• re_cayley

• re_cayley_pos_iff

• cayley_add_conj

• cayley_kernel

• one_sub_mul_conj_ne_zero

• tendsto_zeta_one_add_sub_inv

25.5 Riemann Hypothesis — Schur Gap Transfer and BPY Coercivity (2026-09-28)

Exact steps from Codex’s 2026-09-28 GPPDiscovery2 notes. Neither uses or implies information about zeros.

25.5.1 SchurGapTransfer

For a block matrix \(H=\begin{pmatrix} A & B \\ B^{\mathsf H} & C \end{pmatrix}\) with \(A\succ 0\): \(H-\mathrm{diag}(0,\mu I)\succeq 0\) iff the Schur complement satisfies \(C-B^{\mathsf H}A^{-1}B\succeq \mu I\), so \(\langle (x,y),H(x,y)\rangle \ge \mu \| y\| ^2\). A massive bulk block transfers no gap by itself; the physical gap is decided entirely by the Schur complement. The identification of the blocks with arithmetic objects, and the Yang–Mills programme, are not formalized.

Proved (4 declarations):

• fromBlocks_sub_gap

• schur_gap_iff

• schur_gap_quadratic

• scalar_schur_gap

25.5.2 CriticalBPYCoercivity

The exact steps of the critical BPY coercivity argument: the Neumann lower bound \(\| b_0x+\sum b_iU_ix\| \ge (|b_0|-\sum |b_i|)\| x\| \) for isometries \(U_i\); \((\pi ^2/6-1)(1+63/(16\pi ^2)){\lt}1\); and \(\xi (9/2)\, \zeta (5/2)=\frac{21}{4\pi }\, \zeta (9/2)\, \xi (5/2)\), derived from Mathlib’s completed zeta. The BPY field, the chaos coefficients and the Mellin identity are not formalized.

Proved (6 declarations):

• norm_isometry_sum_ge

• pi_sq_bounds

• tail_constant_lt_one

• Gammaℝ_nine_halves

• completed_eq_Gammaℝ_mul

• xi_ratio

25.6 Riemann Hypothesis — The Conformal Casimir and the TFD GCD Kernel (2026-09-28)

Exact results from Codex’s 2026-09-28 GPPDiscovery2 notes. Neither uses or implies information about zeros.

25.6.1 CasimirCriticalLine

In the \(PSL(2,\mathbb {R})\) Casimir variable \(c=s(1-s)\): \(\xi \) factors through \(c\); \(\operatorname {Im}\rho (1-\rho )=\gamma (1-2\beta )\), so \(\rho (1-\rho )\in \mathbb {R}\) iff \(\operatorname {Re}\rho =\tfrac 12\) or \(\rho \) is real; \(\rho (1-\rho )\) is real and \(\ge \tfrac 14\) iff \(\operatorname {Re}\rho =\tfrac 12\); and, for invertible \(A\) with \(C=\tfrac 14I+A^{-1}\), \(\det (I+(\tfrac 14-c)A)=\det (C-cI)\det A\). Constructing a self-adjoint \(C_{\mathrm{phys}}\ge \tfrac 14\) with spectral determinant \(\xi \) is the open, RH-strength step.

Proved (12 declarations):

• casimir_im

• casimir_re

• casimir_real_iff

• real_casimir_forces_half

• casimir_half_add

• casimir_ge_quarter_iff

• casimir_eq_iff

• xi_one_sub

• casimir_root

• xi_factors_through_casimir

• fredholm_casimir_matrix

• fredholm_casimir_det

25.6.2 TFDGCDMobiusWhitening

The combinatorial core of the GCD Gram kernel (\(mk=nj\) iff \((k,j)=(bt,at)\) with \(m=ga\), \(n=gb\)), the value \((ab)^{-\beta /2}=(g/\sqrt{mn})^\beta \), local Möbius whitening \((I-rS)\omega =e_0\) for \(\omega _k=r^k\), the Gram determinant \(1-r^2\), and the prime-power current \(\frac{d}{d\beta }\log (1-p^{-\beta })=\sum _{k\ge 1}(\log p)p^{-k\beta }=\log p/(p^\beta -1)\). The Hilbert-space and global limits are not formalized.

Proved (6 declarations):

• mul_eq_mul_iff

• gcd_kernel_eq

• whitening_local

• gram_det

• hasDerivAt_log_one_sub

• hasSum_prime_power_current

25.7 Riemann Hypothesis — Why One Half: the Prime-Torus Edge and the Casimir Trichotomy

The critical line is singled out twice, independently: on the prime torus by square summability (\(\| Z_s\| ^2=\sum _n n^{-2\sigma }=\zeta (2\sigma )\) and \(\sum _p p^{-2\sigma }\) are both finite iff \(\sigma {\gt}\tfrac 12\)), and at the Archimedean place as the unitary dual of scaling. In the Casimir variable \(c=\rho (1-\rho )\) every \(\rho \) is either off-line with non-real \(c\), on the line with real \(c\ge \tfrac 14\) (principal-series range), or real with \(c\le \tfrac 14\); real \(\rho \in (0,1)\) give the complementary-series range, and trivial zeros match discrete-series Casimir values only. Nothing here locates a zero: realizing the nontrivial zeros as the Casimir spectrum of a unitary representation built without zero data is equivalent to RH.

Proved (7 declarations):

• full_lift_summable_iff

• prime_sector_summable_iff

• full_lift_norm_sq

• off_line_nonreal_casimir

• real_strip_casimir

• trivial_zero_casimir

• casimir_trichotomy

25.8 Thread Weil-Parity — Metric Positivity of the Cross-Resolvent

From Codex’s KMS-metric note: with \(\eta =Ge_0\) and \(y=(A-z)^{-1}e_0\), the parity cross-resolvent is a \(G\)-energy, \(f(z)=\eta ^{\mathsf T}y=y^{\mathsf T}G(A-z)y\), for any matrix \(G\). Hence positivity of that single form gives \(f(z){\gt}0\), and conversely a nonpositive \(f(z)\) rules out every such \(G\) (the exact form of the earlier negative finding in the raw CCM basis). Symmetry of \(G\) and \(GA=A^{\mathsf T}G\) are needed only to read the positivity as “\(z\) below the \(G\)-spectrum”. Whether the Bost–Connes KMS Gram supplies such a \(G\) for the actual Weil block is open.

Proved (4 declarations):

• cross_resolvent_eq_energy

• cross_resolvent_pos_of_energy_pos

• no_metric_of_cross_resolvent_nonpos

• energy_pos_of_rayleigh

25.9 Riemann Hypothesis — Mathlib’s Statement in the Casimir Variable

Mathlib’s own RiemannHypothesis (all nontrivial zeros) is equivalent to: every nontrivial zero has real Casimir \(s(1-s)\ge \tfrac 14\), the principal-series range; equivalently, a real non-positive centered square \((s-\tfrac 12)^2\) (Codex’s criterion). These are equivalences of statements, not a proof. Also included: the parallel-sum identity \(\min \{ kx^2+Ny^2: x+y=z\} =\frac{kN}{k+N}z^2\), the scalar Schur core of the Shadow Euler bridge (ported from Codex).

Proved (7 declarations):

• casimir_eq_quarter_sub_centeredSq

• centeredSq_nonpos_real_iff

• riemannHypothesis_iff_casimir

• riemannHypothesis_iff_centeredSq

• parallel_sum_energy_identity

• parallel_sum_lower_bound

• parallel_sum_attained

25.10 Riemann Hypothesis — Prime Cayley Two-Channel Identities

From Codex’s prime-energy Cayley note: the local Cayley parameter \(c_p=(\sqrt p-1)/(\sqrt p+1)=\tanh (\tfrac 14\log p)\); the coupling \(\mu _p=2/\sqrt{p-1}\), equal to \(1\) exactly at \(p=5\); the two-channel matrix \(S(\mu )=D(\mu )/\sqrt{\mu ^2+4}\) with \(D=\mu \sigma _z+2\sigma _x\), \(D^2=(\mu ^2+4)I\), so \(S\) is a symmetric reflection with entries \(q=p^{-1/2}\), \(b=\sqrt{1-1/p}\) at \(\mu =\mu _p\). From the primitive-channel note: the repeated prime returns \(\sum _p\sum _{m\ge 3}(\log p)p^{-m/2}\) converge, so \(R_{\ge 3}(L)=O(1)\). Local algebra and one convergent sum; no RH claim.

Proved (9 declarations):

• cayley_eq_tanh

• coupling_eq_one_iff

• channel_entries

• dirac_sq

• channel_symm

• channel_sq

• channel_five

• repeated_returns_hasSum

• repeated_returns_summable

25.11 Riemann Hypothesis — Centered Principal-Series Casimir for Self-Dual L-Functions

From Codex’s universal centered principal-series note: for a completed L-function with symmetry center \(c\), put \(\Delta =1+(s-c)\); then \(s\mapsto 2c-s\) is \(\Delta \mapsto 2-\Delta \), and \(\mathcal C_{\rm ps}=\Delta (2-\Delta )=1-(s-c)^2\) is real and \(\ge 1\) iff \(\Re s=c\). For zeta (\(c=\tfrac 12\)), \(\mathcal C_{\rm ps}=s(1-s)+\tfrac 34\). Also the off-axis quartet \(Q(z)=((z-\delta )^2+\gamma ^2)((z+\delta )^2+\gamma ^2)\): even, conjugation-symmetric, \(Q(0){\gt}0\), vanishing at \(\pm \delta \pm i\gamma \). Correction recorded: the deformation \(\Xi Q/Q(0)\) can equally be read as a change of Archimedean factor, so what excludes it is the exact \(\Gamma _\mathbb R\) factor with the Dirichlet series (Hamburger), not merely the presence of some Archimedean term. No GRH claim.

Proved (14 declarations):

• delta

• psCasimir

• reflect_iff

• re_delta_eq_one_iff

• psCasimir_eq

• psCasimir_line

• psCasimir_ge_one_iff

• psCasimir_half

• quartet

• quartet_even

• quartet_conj

• quartet_zero

• quartet_zero_pos

• quartet_vanishes

25.12 Riemann Hypothesis — Wall/Krylov Coefficients and the Local Prime Poisson Identity

From Codex’s Wall/Krylov shell test and endpoint-BPY notes: the \(3\times 3\) Hankel determinant; invariance of \(\Delta _2,\Delta _3\) (hence of the Jacobi hoppings \(\beta _1,\beta _2\)) under translation of the spectral variable, so the Casimir shift \(K\mapsto e^{-t}K\) moves only the diagonal coefficients; \(\beta _1=(\log K)''\); the Poisson series \(1+2\sum _{m\ge 1}q^m\cos m\theta =(1-q^2)/(1-2q\cos \theta +q^2){\gt}0\) for \(0\le q{\lt}1\), which makes each prime tower half a positive local delay minus the vacuum; and the Dirichlet Green kernel \(e^{-|x-y|/2}-e^{-(x+y)/2}\) (symmetric, zero on the boundary, nonnegative). No RH claim.

Proved (15 declarations):

• hankel2

• hankel3

• hankel_three_det

• hankel_two_shift

• hankel_three_shift

• beta_one_eq_log_second

• hasSum_poisson_cos

• poisson_series

• poisson_pos

• greenD

• greenD_symm

• greenD_zero_left

• greenD_nonneg

• exp_half_second_deriv

• neumann_correction

25.13 Riemann Hypothesis — Prime TFD Weights and the Weighted Lax–Phillips Target

From Codex’s prime-TFD/primitive-lattice, critical half-density Lax–Phillips, and one-correlator notes: \(\varphi (n)/n=\prod _{p\mid n}(1-p^{-1})\), a product of local critical-TFD vacuum probabilities; the primitive-lattice embedding has \(\| V|n\rangle \| ^2=\varphi (n)/n\); the \(\omega \)-family weights \(c_\omega (n)=n^{\omega -1/2}\prod _{p\mid n}(1-p^{-2\omega })\) with \(c_{1/2}=\varphi /n\), \(c_\omega {\gt}0\) for \(\omega {\gt}0\), \(c_0(n)=0\) for \(n{\gt}1\); the zero/pole pair \(c_\rho \pm \omega /2\); the weighted conjugation \(M_a(A_c+a)M_a^{-1}=-d/d\tau \); the finite-interval boundary-flux identity; and the finite-dimensional core of the positive-metric criterion (a metric with \(C^\dagger \eta +\eta C=0\) forces imaginary spectrum). Precision notes recorded: the Beta-integral Laplace form needs \(\Re (s+\tfrac 14-\tfrac \omega 2){\gt}0\); the forms (A)–(D) of the number-hologram note are sufficient for RH, not equivalent. No RH claim.

Proved (14 declarations):

• totient_div_eq_prod

• embedding_norm_sq

• local_coeff

• hasSum_local_ratio

• cOmega

• c_omega_half

• c_omega_pos

• c_omega_zero

• zero_pole_pair

• weighted_conjugation

• boundary_flux

• re_eq_zero_of_metric

• metric_shift_iff

• re_eq_half_of_forall_omega

25.14 Riemann Hypothesis — Prime Cayley Channel: Golden Point and Cayley Inversion

Completing Codex’s formalization-queue rows of 2026-10-02 (the rest is in the Prime Cayley section): \(S(\mu )\) anticommutes with \(\tau =\begin{psmallmatrix} \end{psmallmatrix}0& -1\\ 1& 0\end{psmallmatrix}\); \(c_5=(\sqrt5-1)/(\sqrt5+1)=\varphi ^{-2}\); \((\varphi ,1)\) is the \(+1\) eigenline of \(S_5\); and scalar/finite-diagonal Cayley inversion \(A=(1-C)/(1+C)\). The point \(p=5\) is singled out by the normalization \(\mu =2/\sqrt{p-1}\). No RH content.

Proved (8 declarations):

• tau

• channel_anticomm

• phi

• sqrt5_sq

• cayley_five

• channel_five_golden_eigen

• cayley_inv

• cayley_diag_inv

25.15 Riemann Hypothesis — Prime TFD as an SU(1,1) Coherent State: Euler Factor, Blaschke Channel, Mass

From Codex’s local SU(1,1) closure notes: the paired coherent state is normalized (\(\sum (1-r^2)r^{2m}=1\)) with overlap \(\sqrt{(1-r^2)(1-s^2)}/(1-rs)\) and purity \((1-r^2)/(1+r^2)\), i.e. \((p-1)/(p+1)\) at \(r^2=1/p\); the Euler factor is the Poisson kernel, \((1-p^{-2\sigma })|\zeta _p(\sigma +it)|^2=P_{p^{-\sigma }}(t\log p)\); the local functional-equation transfer is a Blaschke automorphism, \(p^{1/2-s}\zeta _p(s)/\zeta _p(1-s)=B_{p^{-1/2}}(p^{1/2-s})\), unitary on the circle, with group delay equal to the Poisson kernel; the shadow is inversion \(z\mapsto z^{-1}\) and \(w\mapsto 1/\bar w\) in the disk coordinate; with \(\kappa =\operatorname {artanh}a\), \(P_a(0)=e^{2\kappa }\), \(P_a(\pi )=e^{-2\kappa }\) and \(\mu ^2=P_a(0)+P_a(\pi )-2\) for \(\mu =2\sinh \kappa \); and the algebraic part of the Archimedean exponential tilt. Local identities only; the global adelic sewing is open. No RH claim.

Proved (32 declarations):

• poisson

• blaschke

• coherent_normalization

• coherent_overlap

• purity_hasSum

• purity_prime

• euler_factor_intensity

• cpow_polar

• blaschke_euler_transfer

• blaschke_zero

• blaschke_inv

• blaschke_norm_one

• blaschke_hasDerivAt

• blaschke_boundary_delay

• zp

• shadow_inv

• norm_zp

• norm_zp_eq_one_iff

• shadow_conj_disk

• poisson_zero

• poisson_pi

• poisson_zero_mul_pi

• exp_two_artanh

• cayley_eq_exp

• poisson_zero_eq_exp

• poisson_pi_eq_exp

• mass_anisotropy

• cos_two_arctan

• overlap_trig

• mean_eq_tan

• var_sub_mean_sq

• var_eq_sec

25.16 Riemann Hypothesis — The \(k=\tfrac 12\) Character and Blaschke Defect Kernels

From Codex’s SU(1,1) character and de Branges defect notes: the heat character \(\sum _n e^{-2\ell (n+1/2)}=1/(2\sinh \ell )\) gives the prime covariances \(A_p=\sqrt p/(p-1)\), \(C_p=1/(p-1)\) and the Plancherel weight \(\ell /\sinh \ell =2\ell \chi (\ell )\); the Euler factor is a shifted character; the Schur defect kernel of a Blaschke factor is rank one with vector the TFD amplitude; the product rule \(D_{B_1B_2}=D_{B_1}+B_1\bar B_1D_{B_2}\) and quotient rule \(D_{A/B}=(D_A-D_B)/(B\bar B)\); finite cascades have an explicit positive Gram factorization; and positive semidefiniteness is invariant under congruence, so \(D_{A/B}\succeq 0\iff D_A-D_B\succeq 0\) on the disk. The last is an equivalence of statements, the kernel-domination form of the prime-versus-Archimedean problem, not a proof of either side. No RH claim.

Proved (23 declarations):

• heat_character

• prime_anomalous

• prime_normal

• celestial_weight

• euler_shifted_character

• casimir_half

• casimir_principal

• defect

• conj_blaschke

• defect_blaschke

• tfdAmp

• defect_blaschke_rank_one

• tfdAmp_boundary

• defect_mul

• defect_quotient

• IsPSD

• gram_psd

• psd_congruence_mp

• psd_congruence

• defect_quotient_psd_iff

• blaschke_defect_psd

• defect_cascade

• cascade_defect_psd

25.17 Riemann Hypothesis — SU(1,1) Lightcone Excess and Prime Tail Thresholds

From Codex’s von Mangoldt lightcone and \(\det _3\) tail notes: \(\langle K_0\rangle =(1+r^2)/(2(1-r^2))\), \(\langle K_1\rangle =r/(1-r^2)\), the hyperboloid \((2\langle K_0\rangle )^2-(2\langle K_1\rangle )^2=1\), forward and backward null excesses, the anomalous/normal covariance split, mass on the lightcone, the exact tail norm \(\| (I-\Pi _{{\lt}m})\Omega _r\| =r^m\), and the Schatten threshold \(\sum _pp^{-m\sigma }{\lt}\infty \iff m\sigma {\gt}1\) (so \(\det _2\) fails and \(\det _3\) succeeds at \(\sigma =\tfrac 12\)). Scalar series only. No RH claim.

Proved (16 declarations):

• K0_expectation

• K1_expectation

• two_K0_eq_cosh

• two_K1_eq_sinh

• hyperboloid

• null_sum_pos

• null_sum_neg

• anomalous_split

• normal_split

• mass_lightcone

• tail_norm_sq

• prime_tail_summable_iff

• det2_fails

• det3_works

• jacobi_P1

• jacobi_P2

25.18 Riemann Hypothesis — Antipodal Phases, Trivial-Zero Ladder, Heat Trace

From Codex’s antipodal, trivial-zero and \(K_0/K_1\) notes: \(A=\tfrac 14[P(0)-P(\pi )]\), \(C=\tfrac 14[P(0)+P(\pi )-2]\), \(\ell /\sinh \ell =(\ell /2)[P(0)-P(\pi )]\), the antipodal ratio \(q^2\) and negativity \(2\operatorname {artanh}r\); the trivial-zero ladder \(2K_0+\tfrac 32\) with spectrum \(2n+\tfrac 52\) matching the poles of \(\Gamma (\tfrac 54+\tfrac z2)\); the completed function \(\xi (s)=(s-1)\pi ^{-s/2}\Gamma (1+s/2)\zeta (s)\); and the heat-trace/Plancherel density identities. No RH claim.

Proved (10 declarations):

• anomalous_antipodal

• normal_antipodal

• sinh_weight_antipodal

• antipodal_ratio

• negativity_log

• triv_spec

• triv_pole

• xi_eq_gamma

• heat_trace_plancherel

• plancherel_density

25.19 Riemann Hypothesis — Finite Zeta-Graph Metric and Its Dual Norm

From Codex’s finite zeta-graph and half-density Möbius notes: on \(\{ 1,\dots ,N\} \) the Gram kernel of the half-density zeta synthesis is exactly \(G_N(d,e)=\frac{\gcd (d,e)}{\sqrt{de}}H_{\lfloor N/\operatorname {lcm}(d,e)\rfloor }\), the critical GCD kernel times a harmonic boundary taper; the prime-supported current \(\Lambda (n)/\sqrt n\) synthesizes to the smooth \(\log n/\sqrt n\); with \(c=M^Ta\) one has \(a=Z^Tc\), \(\langle a,b\rangle ^2\le \| M^Ta\| ^2\| Zb\| ^2\) with equality at \(b=Mc\) (so \(\| M^Ta\| ^2=a^TG^{-1}a\), the variational form of the dual norm); and for a profile \(a(n)=n^{-1/2}h(\log n-t)\) the dual vector is \(d^{-1/2}\sum _{m\le N/d}\frac{\mu (m)}{m}h(\log m-(t-\log d))\). Finite identities only; the boundary Fourier theory is open. No RH claim.

Proved (17 declarations):

• S

• divisorClosed

• zEntry

• gram

• harm

• gram_eq

• e1

• jN

• synth_current

• halfZetaT

• halfMobiusT

• halfZeta_adjoint

• halfMobius_adjoint

• halfZetaT_halfMobiusT

• dual_norm_le

• dual_norm_attained

• mobiusT_profile

25.20 Riemann Hypothesis — Prime Powers as Schur-Composed Massive Edges

From Codex’s massive-edge notes: the Dirichlet-to-Neumann matrix \(\Lambda (\ell )\) of an interval has inverse \([[\coth ,\operatorname {csch}],[\operatorname {csch},\coth ]]\); Schur elimination of a shared boundary adds lengths, \(\Lambda (\ell _1)\star \Lambda (\ell _2)=\Lambda (\ell _1+\ell _2)\); the hyperbolic transfer matrices satisfy \(M(\ell _1)M(\ell _2)=M(\ell _1+\ell _2)\) and \(M(\tfrac 12\log n)=\prod _{p\mid n}M(\tfrac 12\log p)\) over prime factors with multiplicity; at a prime the entries are the covariances \(C_p+\tfrac 12\) and \(A_p\), the smaller eigenvalue gives the Cayley coordinate \(q_p=(\sqrt p-1)/(\sqrt p+1)\), and \((\log p)p^{-m/2}=2\ell _pe^{-m\ell _p}\); and the Archimedean weight \(w_\infty (x)\) closed form. Finite \(2\times 2\) algebra. No RH claim.

Proved (18 declarations):

• coth

• csch

• dtn

• hyp

• schurStar

• dtn_inverse

• schur_dtn

• M_add

• M_zero

• M_pow

• M_list_prod

• M_primeFactorsList

• coth_prime

• dtn_eigen_tanh

• dtn_eigen_prime

• gamma_prime

• edge_amplitude

• w_infty_eq

25.21 Riemann Hypothesis — Prime Defect as a TFD-Dressed Delay Line

From Codex’s causal-delay note: the bare prime \(\phi (z)=e^{iz\log p}\) has defect kernel \(\int _0^{\log p}e^{itz}\overline{e^{itw}}dt\), a causal delay line; the Blaschke dressing identity \(D_{B_a\circ \phi }=f_a(\phi z)\overline{f_a(\phi w)}D_\phi \) (the TFD factor multiplicatively dresses the delay line); the feature-map Gram representation; the real-axis diagonal \(L\, P_a(Lx)\); and the free-delay-subtracted prime-power current \(\sum _{m\ge 1}2La^m\cos (mLx)=L(P_a(Lx)-1)\). No RH claim.

Proved (8 declarations):

• phi

• defectH

• delay_defect

• blaschke_one_sub

• dressing

• feature_gram

• diagonal_delay

• excess_delay_series

25.22 Riemann Hypothesis — Local Möbius Whitening Operator and Its Symbol

From Codex’s theta-whitening note: for \(u^*u=1\) and real \(r\), \((1-ru)^*(1-ru)=(1+r^2)-r(u+u^*)\), whose symbol is \(|1-re^{-i\theta }|^2=1-2r\cos \theta +r^2{\gt}0\) for \(|r|{\lt}1\). Abstract \(*\)-algebra; the Hilbert-space action and the theta-kernel bookkeeping identity are not formalized. No RH claim.

Proved (3 declarations):

• whitening_gram

• whitening_symbol

• whitening_symbol_pos

25.23 Riemann Hypothesis — Hilbert–Pólya Lemma, Growth Bounds and Unitary Defect Identities

From Codex’s unitary-causal-completion notes and queue rows: the one-line Hilbert–Pólya lemma (a nonzero bounded functional with \(\ell (U_tf)=e^{(\rho -1/2)t}\ell (f)\) under isometries forces \(\Re \rho =\tfrac 12\)); the norm-independent spectral-growth lower bound \(\| V_t\| \ge e^{(1/2-\Re \rho )t}\) and the exponential-type bound \(\omega \ge |\Re \rho -\tfrac 12|\) (why strip-norm engineering cannot itself prove RH); the Blaschke transform of an isometry is an isometry; the exact defect \(B^*XB-X=\ell (1-r^2)V^*V\) and its additivity; the optical identity \(D^*D-D_0^*D_0=(GD)^*(GD)\); contraction \(\iff \) defect positivity; and the translation-energy identity \(2\Re \langle f,Tf\rangle =2\| f\| ^2-\| f-Tf\| ^2\). Abstract algebra and normed-space estimates; the Hardy-space realizations are not formalized. No RH claim.

Proved (10 declarations):

• hilbert_polya_lemma

• growth_lower_bound

• type_lower_bound

• blaschke_isometry

• blaschke_defect

• defect_mul

• optical_identity

• contraction_defect

• contraction_iff_defect_nonneg

• isometry_energy_identity

25.24 Riemann Hypothesis — Prime Channel as a Householder Reflection and the Julia Colligation

From Codex’s golden-Householder, Julia-colligation and Feshbach notes: \(S(c)=2uu^T-I\) with \(u=(1,\sqrt c)/\sqrt{1+c}\) and \(S(\mu _p)=S(c_p)\) at the Cayley coordinate \(c_p=(\sqrt p-1)/(\sqrt p+1)\); \(S\tau S=-\tau \); the Julia matrix \([[r,b],[b,-r]]\) is a reflection with \(\det =-1\) and transfer function the Blaschke map; and the Feshbach projection-norm identity and Gram nonnegativity. Finite algebra. No RH claim.

Proved (10 declarations):

• sOfC

• householder_form

• channel_eq_householder

• reflection_conj

• julia

• julia_sq

• julia_det

• julia_transfer

• projection_norm_sq

• wedge_norm_nonneg

25.25 Riemann Hypothesis — Rank-One Pole Thresholds, Sobolev-Trace DtN, Midpoint Uniqueness, Theta Whitening

From four rows of Codex’s formalization queue: for symmetric invertible \(A\) with \(c^TA^{-1}c=-2\) and \(A\) positive definite on \(c^\perp \), \(A+\tfrac 12cc^T\) is positive semidefinite with kernel exactly \(\mathbb RA^{-1}c\) (the hypothesis is the Haynsworth form of “exactly one negative eigenvalue”); for positive definite \(A\) with \(s^TA^{-1}s=2\), \(A-\tfrac 12ss^T\) is positive semidefinite and singular; the interval DtN matrix equals \(2\kappa [[C+\tfrac 12,-A],[-A,C+\tfrac 12]]\); \((a_L-ra_R^\dagger )\Omega _r=0\) and a nonzero vector cannot satisfy this for two radii; and the shifted-radius whitening \((1-rau)(1-ra^{-1}u)=1-2r\cosh (\theta \log p)u+r^2u^2\). Finite algebra. No RH claim.

Proved (12 declarations):

• pole_threshold_neg

• pole_threshold_pos

• dtn_tfd_identity

• dtn_tfd_prime

• aL

• aRdag

• omega

• midpoint_annihilation

• aRdag_injective

• unique_radius

• theta_whitening

• weights_cosh

25.26 Riemann Hypothesis — Zero Quartet and the Two Spectral Half-Flips

From Codex’s \(q,t\) half-flip note: in the centered coordinate \(z=s-\tfrac 12\) the flips \(z\mapsto -z\) and \(z\mapsto \bar z\) generate the zero quartet \(\{ \pm \delta \pm i\gamma \} \); their product \(z\mapsto -\bar z\) fixes exactly \(\Re z=0\); they agree exactly on the critical line; the odd part \(P_-z=\Re z\) is the off-line displacement; and Mathlib’s RiemannHypothesis is equivalent to \(P_-(\rho -\tfrac 12)=0\) for every nontrivial zero. Statement-level; the physical-quotient target is open. No RH claim.

Proved (16 declarations):

• Rsh

• Rc

• Dspec

• Pplus

• Pminus

• Rsh_Rc_comm

• Rsh_invol

• Rc_invol

• D_spec_apply

• quartet_orbit

• D_fixed_iff

• halfflip_agree_iff

• one_sub_eq_conj_iff

• split_apply

• P_minus_eq_zero_iff

• riemannHypothesis_iff_P_minus

25.27 Riemann Hypothesis — Tomita Modular Flow on Ratio States

From Codex’s Tomita ratio note: on a basis vector with ratio \(n/m\), \((n/m)^{it}=(m/n)^{-it}\) is the principal-series exponent \(r^{1/2-s}\) at \(s=\tfrac 12+it\), has unit modulus, and the swap reverses the ratio. Pointwise identities; the state and its thermodynamic limit are not formalized. No RH claim.

Proved (4 declarations):

• modular_flow_inv

• principal_exponent

• tomita_reverses_ratio

• unit_modulus

25.28 Riemann Hypothesis — Stieltjes–Mellin Dispersion Kernel

The Mellin transform of the Stieltjes kernel: for \(0{\lt}\Re \sigma {\lt}1\), \(\int _0^\infty x^{\sigma -1}/(1+x)\, dx=\pi /\sin (\pi \sigma )\), proved by the substitution \(x=t/(1-t)\) onto the Beta integral, and the combined dispersion factor \(8\pi ^2/\sin (\pi \sigma )\) with the Cutkosky normalization. No RH claim.

Proved (3 declarations):

• beta_one_sub

• stieltjes_mellin

• dispersion_factor

25.29 Riemann Hypothesis — Finite Bost–Connes Divisibility Projections: Two No-Go Results

From Codex’s two Bost–Connes no-go notes: on \(\mathbb {Z}/N\mathbb {Z}\) in the additive-character index basis the range projections \(P_d\chi _k=\mathbf1_{d\mid k}\chi _k\) give a diagonal operator \(\sum _d w_dP_d\) that kills every index coprime to \(N\) (eigenvalue \(\log \gcd (k,N)\) for the von Mangoldt weights), and for \(N=p^K\) the vector \(\delta _1-\delta _{1+p^{K-1}}\) is annihilated by every \(\sum _j w_j(P_{p^j}+F^{-1}P_{p^j}F)\), for every choice of weights. Scope: static projections only; this does not invalidate the Bost–Connes architecture, and no RH claim is made.

Proved (19 declarations):

• Pproj

• H

• H_apply

• eigenvalue_eq_zero_of_coprime

• H_apply_eq_zero_of_coprime

• vonMangoldt_eigenvalue

• expectation_weighted_kernel

• bpt

• nullVec

• lt_pow_of_hyp

• not_dvd_bpt

• val_one

• val_bpt

• one_ne_bpt

• nullVec_ne_zero

• Pproj_nullVec

• dft_nullVec

• Pproj_dft_nullVec

• selfDual_frame_annihilates

25.30 Riemann Hypothesis — Bost–Connes Midpoint Algebra: Torsion Average, Two-Point Function, Jump Energy

From Codex’s Bost–Connes \(ax+b\) midpoint note: the range projection acts on the additive character of index \(k\) as \(\mathbf1_{n\mid k}\) (a torsion average); abstractly, if \(\omega (\mu _m^*\mu _n)=\delta _{mn}\) then the prime current \(J_N=\sum \sqrt{\Lambda (n)}\mu _n\) has midpoint two-point function \(\sum \Lambda (n)n^{-1/2}e^{iu\log n}\); and for norm-preserving \(T_n\), \(\sum c_n\| f-T_nf\| ^2=2\sum c_n(\| f\| ^2-\operatorname {Re}\langle f,T_nf\rangle )\). Scope: the Bost–Connes \(C^*\)-algebra and its KMS states are not formalized, and the orthonormality is a stated hypothesis. No RH claim.

Proved (5 declarations):

• torsion_average

• modFactor

• half_shift

• midpoint_two_point

• jump_energy

25.31 Riemann Hypothesis — No-Go: Prime Inner Channels Have a Non-Globalizable Zero Divisor

From Codex’s zero-accumulation note: the prime channel \(\Theta _p(z)=B_{p^{-1/2}}(e^{iz\log p})\) has the exact zero lattice \(z=2\pi k/\log p+i/2\) in the upper half-plane; every prime shares the zero \(i/2\); the \(k=1\) zeros are pairwise distinct and accumulate at \(i/2\), so by the identity theorem no nonzero analytic function vanishes at all of them; and the Blaschke terms at the common zero are \(2/5\) for every prime, so the Blaschke sum over primes diverges. Scope: the infinite-product statement itself is not formalized. No RH claim.

Proved (19 declarations):

• B

• theta

• zpk

• zpk_re

• exp_neg_half_log

• exp_eq_iff

• denom_ne_zero_aux

• denom_ne_zero

• theta_eq_zero_iff

• theta_zero_at_half_I

• prod_theta_zero

• zk_dist_half_I

• zk_ne_half_I

• zk_injOn

• tendsto_zk

• no_analytic_with_prime_zeros

• blaschkeTerm

• blaschke_term_half_I

• not_summable_blaschke

25.32 Riemann Hypothesis — Critical Zeta Gibbs Ensemble: The Escaping Energy is Exponential

From Codex’s critical Gibbs-escape note: the Laplace transform of the scaled energy \(\epsilon \log N\) under the zeta Gibbs law is exactly \(\zeta (1+\epsilon (1+s))/\zeta (1+\epsilon )\), and it converges to \(1/(1+s)\) as \(\epsilon \downarrow 0\), the transform of an \(\mathrm{Exp}(1)\) law; the only analytic input is the residue of \(\zeta \) at \(1\). Scope: convergence of transforms is proved pointwise in \(s\); the passage to convergence in distribution and the joint limit with prime occupations are not formalized. No RH claim.

Proved (5 declarations):

• laplace_term

• laplace_tsum

• tendsto_path

• tendsto_residue_path

• tendsto_laplace

25.33 Riemann Hypothesis — Self-Dual Divisor Geometry: Subgroup Gram Matrix and Mobius Parity

From Codex’s finite self-dual divisor note: the normalized subgroup states \(v_d\) on \(\mathbb {Z}/N\mathbb {Z}\) have Gram matrix \(\langle v_d,v_e\rangle =\gcd (d,e)/\sqrt{de}\) (so \(\langle v_d,v_{dp}\rangle =p^{-1/2}\)), and on the squarefree divisor cube the kernel is \(\prod _{p\in T\triangle S}p^{-1/2}\) with the Mobius parity vector an eigenvector of eigenvalue \(\prod _{p\in P}(1-p^{-1/2})\) for arbitrary weights. Scope: the unitary Fourier duality \(v_d\mapsto v_{N/d}\), the Hodge/Koszul reading, and the limit of the eigenvalue are not formalized. No RH claim.

Proved (15 declarations):

• Hset

• card_Hset

• Hset_inter

• vstate

• gram

• gram_eq_card

• gram_eq

• overlap_prime

• kern

• symmDiff_insert_left

• symmDiff_insert_right

• symmDiff_insert_both

• q_notMem_symmDiff

• mobius_eigen_weighted

• mobius_eigen

25.34 Riemann Hypothesis — Dual Mobius Obstruction in the Finite Zeta-Graph Metric

From Codex’s dual-Mobius note: the inverse-transpose of the half-density zeta matrix sends the raw character \(n^{-z}\) to the truncated reciprocal-zeta sum, \(b_{N,z}(d)=d^{-z}\sum _{m\le N/d}\mu (m)m^{-1/2-z}\), and the \(d=1\) coordinate bounds the dual norm below by the weighted Mobius partial sum. Scope: the partial-summation equivalence with the Mertens bound is not formalized. No RH claim.

Proved (4 declarations):

• dualCoord

• dual_coord_eq

• dualNormSq

• dual_norm_ge

25.35 Riemann Hypothesis — Half-Line Resolvent Commutator: Rank-One Kernel

From Codex’s rank-one resolvent note: the commutator of the Dirichlet half-line resolvent kernel with unilateral translation is exactly \(u_{a,\kappa }(x)e^{-\kappa y}\), rank one with the same right vector \(e^{-\kappa y}\) for every \(a\), and \(\| e_\kappa \| ^2=1/(2\kappa )\). Scope: pointwise kernels only; the operator-level statements, the trace, the contact limit, and the AFT Feshbach collapse are not formalized. No RH claim.

Proved (5 declarations):

• G

• u

• commKernel

• commutator_kernel

• norm_sq_expVec

25.36 Riemann Hypothesis — Local Odd-Transfer Contraction and the Cross-Mode Krein Obstruction

From Codex’s odd-transfer note: for the SU(1,1) coherent state \(\Omega _r\) and occupation parity \(J\), \(\langle \Omega _r,J\Omega _s\rangle =\sqrt{(1-r^2)(1-s^2)}/(1+rs)\), the parity components satisfy \(\| P_+\Omega _r\| ^2=1/(1+r^2)\) and \(\| P_-\Omega _r\| ^2=r^2/(1+r^2)\) so \(\| P_-\Omega _r\| /\| P_+\Omega _r\| =|r|\) (a strict contraction for every single prime mode), but for two distinct parameters the reflection Gram determinant is \(-(1-r^2)(1-s^2)(r-s)^2/((1+r^2)(1+s^2)(1+rs)^2){\lt}0\), so the raw reflection form is indefinite. Scope: the Archimedean Jacobi-transform picture and the sharpened positive-frame target are not formalized. No RH claim.

Proved (9 declarations):

• reflected_overlap

• reflected_purity

• plus_sq_hasSum

• minus_sq_hasSum

• odd_even_ratio

• krein

• krein_symm

• krein_diag

• krein_det_neg

25.37 Riemann Hypothesis — Two-Logistic Density as a Ward Operator on the Bose Trace

From Codex’s logistic/Mellin note: with the Bose trace \(h(y)=1/(e^y-1)\), the closed form \((y\coth (y/2)-2)/(4\sinh ^2(y/2))\) of the two-logistic density equals \(yh''(y)+2h'(y)\) for \(y\ne 0\), with \(h'\) and \(h''\) computed explicitly. Scope: that the convolution of two logistic densities is this closed form, the logistic characteristic function, and the Mellin identity \(\int y^sg=s(s-1)\Gamma (s)\zeta (s)\) are not formalized. No RH claim.

Proved (8 declarations):

• bose

• bose1

• bose2

• twoLogistic

• exp_sub_one_ne

• hasDerivAt_bose

• hasDerivAt_bose’

• logistic_conv_eq_ward

25.38 Riemann Hypothesis — Prime-Power Current as Excess Group Delay

From Codex’s group-delay note: the Fourier series of the Poisson kernel gives \(\sum _{m\ge 1}(\log p)p^{-m/2}\cos (mt\log p)=\tfrac 12(\tau _p(t)-\log p)\) with \(\tau _p(t)=\log p\cdot P_{p^{-1/2}}(t\log p)\), so the von Mangoldt half-density current is the excess of the local Wigner–Smith delay above the free baseline; phase derivatives add over a finite prime set; the raw delay is strictly positive while the vacuum-subtracted excess is positive at \(\theta =0\) and negative at \(\theta =\pi \). Scope: the global statements (divergent baseline, Archimedean background, zero density) are not formalized. No RH claim.

Proved (7 declarations):

• poisson_series

• vonMangoldt_current

• vonMangoldt_current_prime

• vonMangoldt_current_finite

• delay_pos

• excess_pos_at_zero

• excess_neg_at_pi

25.39 Riemann Hypothesis — Primitive Renormalization and Finite Half-Derivative Energy

From Codex’s half-derivative energy note: the prime-power frequencies \(m\log p\) are pairwise distinct; the local energy series is \(-\log (1-1/p)\); after removing the primitive harmonic the tail is at most \(p^{-2}\), so \(\sum _p(\log p)(-\log (1-p^{-1})-p^{-1}){\lt}\infty \), whereas the raw primitive sum \(\sum _p(\log p)/p\) diverges. Scope: the identification of the phase with this Fourier series and the Bohr setting are not formalized. No RH claim.

Proved (7 declarations):

• freq_injective

• local_energy

• tail_energy

• tail_le

• tail_nonneg

• summable_tail

• not_summable_primitive

25.40 Riemann Hypothesis — SU(1,1) Transfer Discriminant as the Finite-Place Mass Coordinate

From Codex’s mass-discriminant note: the hyperbolic transfer matrix \(G(\kappa )\) has \(\det G=1\) and \(G(\kappa )G(\kappa ')=G(\kappa +\kappa ')\); \((\operatorname {Tr}G)^2-4=4\sinh ^2\kappa \), equal to \(4/(p-1)\) for \(a=p^{-1/2}\); the TFD covariance is \(\tfrac 12G^{-2}\) with determinant \(\tfrac 14\); the Cayley coordinate is the squeezed eigenvalue ratio; orientation reversal preserves the discriminant while the sewn two-sheet holonomy has discriminant exactly \(0\); and at \(p=5\) the discriminant is \(1\) with \(e^\kappa =\varphi \). Scope: the conditional horizon interpretation and the global renormalized boost are not formalized, and nothing is claimed about observed masses. No RH claim.

Proved (15 declarations):

• Gk

• Gk_det

• Gk_trace

• Gk_mul

• Gk_zero

• Gk_neg_mul

• disc_eq

• disc_prime

• Cov

• cov_eq

• cov_det

• cayley_ratio

• inversion_disc

• pair_disc_zero

• golden_prime

25.41 Riemann Hypothesis — Regularized Prime Scattering and the Schatten Strip Hierarchy

From Codex’s strip-hierarchy note: with \(|\sin w|\le e^{|\operatorname {Im}w|}\), the \(m\)-th term of the regularized local log-phase is bounded by \(p^{-m(1/2-|y|)}\); if \(k(1/2-|y|){\gt}1\) the prime majorant converges (normal convergence), the leading term is summable over primes iff \(k\sigma {\gt}1\), and \(k\sigma {\gt}1\iff |y|{\lt}\tfrac 12-\tfrac 1k\), which for \(k=3\) is \(|\operatorname {Im}T|{\lt}\tfrac 16\). Scope: the identification with the analytic product and the real-axis phase derivative are not formalized. No RH claim.

Proved (6 declarations):

• norm_sin_le

• weight_eq

• prime_tail_summable

• leading_summable_iff

• strip_iff

• strip_three

25.42 Riemann Hypothesis — TFD Boundary Cayley Transform, Parity Determinants, Schur Complement

From Codex’s Cayley/parity note: \(I-Q=(xS)(I+Q)\) with \(x=e^{-u}\), so the Cayley transform of the normalized TFD precision is the attenuated sheet exchange; the parity eigenvalues, the determinants \((1-x)(1+x)=1-x^2\), trace parity of powers of \(xS\), the parity covariances \(x/(1-x)\) and \(-x/(1+x)\) with normal and anomalous sectors, the Schur complement \(\tanh (u)/(2q)\), and the even/odd split \(-\log (1-x)=-\tfrac 12\log (1-x^2)+\operatorname {artanh}x\). Scope: the interval DtN matrix, the positive spectral expansion, and the determinant Euler products are not formalized. No RH claim.

Proved (17 declarations):

• Qmat

• Smat

• cayley_Q

• det_one_add_Q_ne

• parity_eigen_plus

• parity_eigen_minus

• det_full

• prod_parity

• trace_pow

• cov_plus

• cov_minus

• cov_plus_exp

• cov_minus_exp

• normal_sector

• anomalous_sector

• schur_complement

• neglog_decomp

25.43 Riemann Hypothesis — Centered Divisor Coordinate and Hodge Reflection

From Codex’s centered-divisor note: the centered logarithmic divisor coordinate \(\ell _N(d)=\log d-\tfrac 12\log N\) equals \(\sum _{p\mid N}(v_p(d)-K_p/2)\log p\), divisor complementation \(d\mapsto N/d\) acts by \(\ell \mapsto -\ell \), and the centered scaling character satisfies \(\chi _t(N/d)=\chi _{-t}(d)=\overline{\chi _t(d)}\), the unitary reflection law of the principal series. Scope: spectral quantization is the note’s open target and is not formalized. No RH claim.

Proved (5 declarations):

• centered

• centered_complement

• centered_eq_sum

• chi

• character_complement

25.44 Riemann Hypothesis — Finite Fourier Duality Exchanges Subgroup States

From Codex’s self-dual divisor note: on \(\mathbb {Z}/dM\mathbb {Z}\) the discrete Fourier transform of the indicator of the multiples of \(d\) is \(M\) times the indicator of the multiples of \(M\), and for the normalized states \(N^{-1/2}\mathcal{F}v_d=v_{N/d}\), which forces the half-density normalization. Scope: the Hodge/Koszul reading is not formalized. No RH claim.

Proved (3 declarations):

• ind

• dft_indicator

• fourier_subgroup_state

25.45 Riemann Hypothesis — Pullback Metric from an Ambient Self-Adjoint Intertwiner

From Codex’s pullback-metric note: for an injective \(B\) and a Hermitian \(\tilde A\) with \(BA=\tilde AB\), the metric \(G=B^*B\) is positive definite and satisfies \(GA=A^*G\) automatically, and if the displacement vector is \(\eta =B^*(Be_0)\) then \(\eta =Ge_0\). Scope: the concrete arithmetic embedding is left open by the note. No RH claim.

Proved (3 declarations):

• pullback_symmetrizes

• pullback_posDef

• pullback_displacement

25.46 Riemann Hypothesis — No Diagonal Reweighting of the Prime Hilbert Space

From Codex’s scalarization note: no positive weights \(w_p\) on the primes can make both \(\sum w_p(\log p)^2/p{\lt}\infty \) (the primitive current is a vector) and \(\sum 1/w_p{\lt}\infty \) (all-ones evaluation is bounded), by AM–GM and Euler’s divergence of \(\sum 1/p\). Scope: temperedness of the vector-valued current is not formalized. No RH claim.

Proved (1 declarations):

• no_diagonal_fix

25.47 Riemann Hypothesis — Prime TFD Phase: Caratheodory Function, Local Variance, Fisher Distance

From Codex’s phase-geometry note: \(\operatorname {Re}\frac{1+z}{1-z}\) at \(z=re^{i\theta }\) is the Poisson kernel (so \(H\) is Caratheodory), \(L\, z/(1-z)=\tfrac L2H-\tfrac L2\), each prime contributes \(L^2/(2(p-1))\) to the variance of the centered current, the radial Fisher distance is \(\int _0^r\sqrt2/(1-u^2)\, du=\sqrt2\operatorname {artanh}r\), and the logarithmic negativity is \(\sqrt2\) times it. Scope: the Fisher information integrals, torus equidistribution and the ergodic averages are not formalized. No RH claim.

Proved (6 declarations):

• caratheodory_re

• caratheodory_pos

• euler_log_deriv

• local_variance

• fisher_radial_distance

• negativity_eq

25.48 Riemann Hypothesis — Prime-Power Valuation Chains: Gram Matrix and Euler Green Function

From Codex’s valuation-chain note: on \(\mathbb {Z}/p^K\mathbb {Z}\) the normalized subgroup states \(v_a\) have Gram matrix \(\langle v_a,v_b\rangle =p^{-|a-b|/2}\), so the prime-power tower is a one-dimensional Markov covariance chain in the valuation coordinate, and the one-sided Green function of the chain is the Euler factor \(\sum _{k\ge 0}p^{-k/2}e^{-ikt\log p}=1/(1-p^{-1/2-it})\). Scope: the tridiagonal precision matrix, CRT tensor factorization, and the product-formula sewing are not formalized. No RH claim.

Proved (2 declarations):

• valuation_gram

• euler_green

25.49 Riemann Hypothesis — Haar Valuation Law and the Mean Mass Series

From Codex’s profinite mass-law note: the geometric valuation law \(\Pr (N_p=a)=(1-p^{-1})p^{-a}\) is normalized, has mean \(1/(p-1)\) and single-prime Laplace transform \((1-q)/(1-qe^{-s})\), and the mean total mass \(\sum _p 2/(p-1)^{3/2}\) of the Casimir-weighted sum converges. Scope: Haar measure on \(\widehat{\mathbb Z}\), independence, Borel–Cantelli, the variance and the dark-matter reading are not formalized. No RH claim.

Proved (5 declarations):

• geometric_normalization

• geometric_mean

• mean_prime

• geometric_laplace

• mean_mass_summable

25.50 Riemann Hypothesis — The totient Volterra kernel: exact zero mean and divisor regrouping

The totient density \(\varphi (n)/n=\sum _{d\mid n}\mu (d)/d\), the smoothing kernel \(G(y)=4y\arccos y-2\sqrt{1-y^2}\) with \(\int _0^1G=0\), its ODE form \(g'=a-g/2\), and the exact regrouping \(K(x)=\sum _{d\le x}\mu (d)/d\, A_G(x/d)\). Finite and exact; the Volterra/Mertens asymptotic analysis is not formalized. No RH claim.

Proved (19 declarations):

• totient_div

• G

• G_zero

• G_one

• continuous_G

• hasDerivAt_G

• F

• continuous_F

• hasDerivAt_F

• integral_y_arccos

• integral_sqrt_quarter

• integral_G

• a

• g

• hasDerivAt_g

• tendsto_g_zero

• AG

• K

• sum_regroup

25.51 Riemann Hypothesis — The logistic density, the \(\tanh (x/2)\) substitution and Möbius boosts

The logistic density \(p(x)=1/(4\cosh ^2(x/2))=e^x/(1+e^x)^2\), \(d\tanh (x/2)/dx=2p(x)\), and the boost \(x\mapsto x-t\) acting on \(r=\tanh (x/2)\) by the Möbius map \((r-a)/(1-ar)\) with derivative \((1-a^2)/(1-ar)^2\). Calculus identities only. No RH claim.

Proved (6 declarations):

• p

• logistic_density_eq

• p_pos

• hasDerivAt_tanh_half

• tanh_half_sub

• hasDerivAt_mobius

25.52 Number Theory — Arithmetic Layer

25.52.1 BSDPointCounts

Source: On the Nature of Nature monograph, BSD chapter, worked example "BSD for E: y² = x³ - x"

Proved (47 declarations):

• affinePoints

• pointCount

• tracePairing

• pointCount_three

• tracePairing_three

• pointCount_five

• tracePairing_five

• pointCount_seven

• tracePairing_seven

• pointCount_eleven

• …and 37 further results in this module.

25.52.2 WeylCasimir

Source: zitterbewegung_T_boundary_FINAL.tex, Theorem thm:weyl-casimir-value

Proved (30 declarations):

• rhoA3

• rhoA3_dot_self

• weyl_vector_sq_numerator

• weyl_vector_casimir_times_four

• weyl_casimir_u4

• muPlusRhoA3

• muPlusRhoA3_dot_self

• gr24_lambda1

• rhoD4

• casimirD4

• …and 20 further results in this module.

25.52.3 EulerSumCapstone

From ‘haar_qg_paper_v2151.tex‘ base case ‘L = 2‘: the physics paper reconstructs the

Proved (26 declarations):

• term_swap

• nonneg_inv_sq

• summable_prod_inv_sq

• summable_term

• hasSum_term

• tsum_term_eq

• Dg

• Lt

• Gt

• diagEquiv

• …and 16 further results in this module.

25.52.4 DecodingReality

Source: decoding_reality_v4322.tex

Proved (24 declarations):

• weinberg_angle_su5

• weinberg_angle_su5_int

• casimir_formula_nonneg

• casimir_1

• casimir_2

• casimir_3

• casimir_ratios_2_5_9

• casimir_nat_ratios

• georgi_jarlskog_algebra

• georgi_jarlskog_casimir

• …and 14 further results in this module.

25.52.5 ShadowEulerIdentity

Source: *The Shadow Euler Identity: A Family of Evaluations of the Completed

Proved (13 declarations):

• glueball_product_numerator

• lem_perfect_square

• coupling_numerator_sq

• denominator_pos

• coupling_numerator_nonzero

• coupling_numerator_neg

• coupling_numerator_arith_progression

• shadowCoupling

• shadow_coupling_sq_rational (restated in \(\mathbb {R}\) 2026-09-02; the \(\mathbb {Q}\)-valued form asserted nothing)

• shadow_coupling_su3

• …and 3 further results in this module.

25.52.6 ZetaProperties

This file collects provable properties of the Riemann zeta function

Proved (13 declarations):

• riemannXi_def_eq

• critical_line_unique_fixed_locus

• shadow_fixed_locus_is_critical_line

• principal_series_shadow_eq_conj

• trivial_zero_outside_critical_strip

• xi_zero_iff_zeta_zero

• xi_zeros_symmetric

• critical_strip_symmetric

• off_critical_zero_gives_pair

• RiemannHypothesis

• …and 3 further results in this module.

25.52.7 PerfectNumbersE8

Source: decoding_reality_v43221.tex, "E₈, Perfect Numbers, and Moonshine".

Proved (11 declarations):

• sigmaK

• e8_theta_coeff_one

• e8_theta_coeff_two

• e8_theta_coeff_three

• e8_theta_coeff_four

• e8_theta_coeff_five

• perfect_496

• factorization_496

• mersenne_31

• mersenne_31_prime

• …and 1 further results in this module.

25.52.8 TwinPrimeDoublets

Regard primes as vertices and join two vertices when their difference is ‘2‘. The graph

Proved (4 declarations):

• twin_triplet_center_eq_five

• prime_gt_five_not_two_sided_twin

• two_sided_twin_iff_five

• prime_gt_five_singlet_or_one_sided_doublet

25.52.9 ZagierMZVGrowth

Source: On the Nature of Nature v5.2.1.3, "Loop Transcendence from the Plastic Constant"

Proved (4 declarations):

• mzvDim

• mzvDim_matches_source

• plastic_constant_cubic_approx

25.52.10 GaussSumModulus

Source: Tate’s-thesis lecture notes (Warwick "tateweek4" notes, epsilon-factor discussion

Proved (1 declaration):

• gaussSum_norm_eq_sqrt_card

25.52.11 ZetaNegativeIntegers

Source: decoding_reality_v43221.tex asserts ‘ζ(-3) = -1/120‘ (used as an input to a

Proved (1 declaration):

• riemannZeta_neg_three

25.53 Celestial Holography — Further Results

25.53.1 HolographicChain

Source: holographic_chain_v93.tex

Proved (31 declarations):

• plucker_ambient_dim

• exterior_two_dim

• gr24_euler_char

• gr24_complex_dim

• hodgeStar_sq

• hodgeStar_trace

• sd1

• sd2

• sd3

• asd1

• …and 21 further results in this module.

25.53.2 TwistorGoogly

Source: twistor_googly_dtoupin_v81.tex

Proved (6 declarations):

• exterior_two_dim

• gr24_complex_dim

• plucker_ambient_dim

• schubert_cell_count

• schubert_dim_sum

• shadow_as_grassmannian_involution

25.53.3 GrassmannianSelfDuality

Source: On the Nature of Nature v5.2.1.3, Chapter 7 ("The Isomorphism: From Quantum Gravity to Number Theory"),

Proved (5 declarations):

• grassmannian_orthogonal_dim

• grassmannian_orthogonal_involutive

• grassmannian_self_dual_iff

• gr_two_four_self_dual

• grassmannian_gaussian_binomial_two_four

25.53.4 MellinKinematics

Thread M of ‘docs/FORMALIZATION_PLAN.md‘, from ‘mellin_kinematics.tex‘ — the elementary

Proved (5 declarations):

• power_law_classification

• scale_shadow_involutive

• scale_shadow_norm_sq

• mellin_kernel_transport

• quadratic_transport_axis

25.53.5 FubiniStudyAntipodal

Source: qg_foundations.tex, Lemma "Antipodal Symmetry" (‘lem:antipodal‘).

Proved (2 declarations):

• fs_measure_antipodal_invariant

• fs_density_not_invariant_without_jacobian

25.54 Quantum Gravity — Further Results

25.54.1 SinhZetaBridge

Thread S of ‘docs/FORMALIZATION_PLAN.md‘, from ‘kinematic_block_v11.tex‘ (Proposition

Proved (8 declarations):

• sinh_summand_eq

• integral_term

• integrable_term

• tsum_odd_inv_rpow

• sinh_mellin_zeta

• integral_id_div_sinh

• integral_cube_div_sinh

• plancherel_first_moment

25.54.2 WightmanAxioms

Source: wightman_paper.tex

Proved (7 declarations):

• dim_su4

• dim_u2

• dim_stab

• dim_gr24_real

• dim_gr24_complex

• plucker_target_dim

• dim_sun

25.54.3 ZitterbewegungShadow

Thread Z of ‘docs/FORMALIZATION_PLAN.md‘, from ‘zitterbewegung_T_boundary_FINAL.tex‘

Proved (6 declarations):

• shadow_energy_eq

• shadow_splitting

• shadow_splitting_onshell

• shadow_frequency_onshell

• beat_frequency

• mirror_dm_bound

25.54.4 PlanckIntegral

Thread P of ‘docs/FORMALIZATION_PLAN.md‘, from ‘blackbody_law_qg_v1.tex‘ (the

Proved (5 declarations):

• integral_pow_three_mul_exp

• integrable_term

• hasSum_six_div_pow_four

• planck_summand_eq

• planck_integral

25.55 Standard Model — Further Results

25.55.1 TauDifferential

Theorem 3.3(iv) of mass_orientation_coupling_v3.tex: the differential of the orientation map \(\tau (A)=A\varepsilon /\det A\) on the big cell of \(\mathrm{Gr}(2,4)\). Retires open_differential_charpoly, which had been parked on the grounds that it needed “eigenvalue/spectrum theory for a non-symmetric real matrix”. It does not: what “characteristic polynomial \(t^4-\Delta ^{-4}\)” asserts about the matrix is Cayley–Hamilton plus the two eigenvalues, and both are matrix arithmetic. The Jacobian itself is a theorem, not an asserted matrix — all sixteen partials are proved, four coordinates at a time, as genuine HasDerivAt statements about the full 4-tuple.

Proved (7 declarations):

• hasDerivAt_affine_div_affine

• hasDerivAt_tau4_a

• hasDerivAt_tau4_b

• hasDerivAt_tau4_c

• hasDerivAt_tau4_d

• tauJac_pow_four

• tauJac_mulVec_eigen_pos

Honest boundary. tauJac is the matrix of partial derivatives, which is what the four HasDerivAt results establish; Fréchet differentiability of \(\tau \) as a map \(\mathbb {R}^4\to \mathbb {R}^4\) follows from continuity of those partials by the standard \(C^1\) criterion, not formalized here and not depended on by anything above. And the result is not stated as a literal Matrix.charpoly identity, which would require a symbolic \(4\times 4\) determinant over \(\mathrm{Polynomial}\ \mathbb {R}\).

25.55.2 MassOrientationCoupling

Source: mass_orientation_coupling_v3.tex

Proved (8 declarations):

• tau_tau_eq_neg

• momentum_spinor_decomposition

• psiL_zero

• psiR_zero

• clock_locking_negate

• clock_locking_restore

• clock_locking_population

• gamma0_double_commutator

25.55.3 OrientationCliffordCore

Source: Which_Way_Is_Forward_v26.tex (22 September 2026), section “One time axis, two microscopic orientations, and the four-lift carrier” and its subsections, with the paper’s own check script verify_which_way_is_forward.py. Every statement is a finite identity over \(\mathbb Z[i]\), checked by the kernel. The physical readings are the paper’s dictionary and are not formalized.

Proved (17 declarations):

• clifford_relations

• orientation_algebra

• chi_eq_neg_volume

• rt_eq_rq_mul_c

• intertwiner_unitary

• intertwiner

• fourLift_algebra

• carrier_nodup

• closure_eq_carrier

• carrier_order_counts

• carrier_center

• D_not_central

• fixD_iff

• halfFlips_agree_on_fixD

• Rt_reverses_chi

• minkowski_clifford_relations

• minkowski_realization

Not formalized here. The coordinate-blade signature scan, the \(\mathrm{Spin}(6,2)\)/\(\mathrm{Spin}(10,2)\) charge-conjugation signs, and the determinant cover. The paper’s Lean inventory cites 34 modules on the unmerged branch codex/orientation-mass-time-formalization (draft PR #173); as of 2026-09-26 that branch does not build, and none of its modules states the intertwiner or the order-16 carrier.

25.55.4 KappaShadow3

Source: kappa_paper.tex, "Fermion Mass Hierarchy from Division Algebra

Proved (7 declarations):

• kappaFS

• kappa_shadow3_sum_rule

• kappa_d_eq

• kappa_L_eq

• kappa_u_eq

• kappa_ud_sum

• triality_complementary_angle

25.55.5 KoideRelation

Source: On the Nature of Nature v5.2.1.3, "The Koide Structure: √2 as a Theorem"

Proved (7 declarations):

• cos_two_pi_div_three

• sin_two_pi_div_three

• cos_four_pi_div_three

• sin_four_pi_div_three

• koide_phase_sum_zero

• koide_epsilon_sq_two

• koide_epsilon_eq_sqrt_two

25.55.6 MajoranaCondition

Sources:

Proved (5 declarations):

• epsilon

• epsilon_sq

• epsilon_det

• zitterbewegung_frequency

• zitterbewegung_period

25.55.7 ComplementaryPairs

Source: On the Nature of Nature v5.2.1.3, "Counting Complementary Pairs" (thm:three-partitions),

Proved (2 declarations):

• complementaryPairings

• exactly_three_complementary_pairings

25.56 General Relativity — Further Results

25.56.1 Rigidity

This file formalizes ‘thm:rigidity‘ (On the Nature of Nature v5.2, cited 10×):

Proved (2 declarations):

• graviton_shadow_dimension

25.57 Cosmology

25.57.1 DarkEnergy

Source: dark_energy_full2.tex

Proved (11 declarations):

• shadow_t_duality_involution

• shadow_self_dual_point

• shadow_reflects_scale

• shadow_log_negation

• shadow_dimension_involution

• weyl_fermion_decomp

• three_gen_conformally_coupled

• dark_energy_acceleration_threshold

• de_constant_growth

• phantom_crossing_condition

• …and 1 further results in this module.

25.57.2 UnifiedDipole

Source: unified_dipole_v115.tex

Proved (11 declarations):

• dipole_shadow_eigenvalue_complex

• dipole_eigenvalue_negative

• dipole_eigenvalue_at_unit

• dipole_eigenvalue_bounded

• dipole_eigenvalue_decreasing

• harrison_zeldovich_exponent

• slow_roll_from_tilt

• bost_connes_inflation_parameter

• shadow_deficit_positive

• shadow_enhancement_exceeds_one

• …and 1 further results in this module.

25.57.3 AbelHaloPair

Thread H of ‘docs/FORMALIZATION_PLAN.md‘, from On the Nature of Nature v5.2.1.3 Chapter "Dark Matter:

Proved (6 declarations):

• pseudo_isothermal_eq

• hasDerivAt_sq_sub

• hasDerivAt_sq_add

• abel_forward

• abel_inverse_eval

• dm_profile_boxed

25.57.4 DarkMatterGammaRatio

Source: On the Nature of Nature v5.2.1.3, "The Grassmannian Spinor Bundle: Time Reversal,

Proved (4 declarations):

• gamma_three_half_eq

• gamma_ratio_one_half_three_half

• dm_baryon_leading_term

• shadow_kernel_normalization_three_half

25.58 String Theory

25.58.1 DivisionAlgebras

Source: why_string_theory_works_v4.tex

Proved (13 declarations):

• hurwitz_algebra_count

• division_algebra_dim_sum

• division_algebra_dim_seq

• critical_brane_dimensions

• m_theory_dimension

• critical_dims_count

• three_generations_weyl_anomaly

• three_generations_exact

• gamma_functional_eq

• gamma_at_one

• …and 3 further results in this module.

25.59 Thread S — Signature and Inertia

25.59.1 SignatureInertia

Finite-dimensional, analysis-free, zero-free (no Riemann zeta zeros anywhere in this

Proved (1 declaration):

• inertia_sum

25.60 Yang–Mills

25.60.1 MassGap

Source: YM_PAPER35.tex

Proved (22 declarations):

• dualCoxeterSU

• casimirAdjointSU

• casimirFundamentalSU

• casimirFundamentalSU_su3

• casimir_adj_fund_ratio

• mass_gap_ratio

• mass_gap_ratio_su3_k1

• mass_gap_ratio_su3_k3

• mass_gap_ratio_pos

• mass_gap_ratio_le_two

• …and 12 further results in this module.

25.61 Core Theorems and Grassmannian Geometry

25.61.1 CoreTheorems

Proved (20 declarations):

• IsInvolution

• shadow_involution

• root_involution_order_2

• involution_injective

• involution_surjective

• involution_fourth_power

• SectorDecomposition

• googly_resolution

• T_squared_identity

• LeftHanded

• …and 10 further results in this module.

25.61.2 GrassmannianJacobian

‘GrassmannianMass.lean‘ proves that the chart transition map

Proved (5 declarations):

• N

• K

• N_sq_eq_D_smul_K

• K_sq_eq_D_sq_smul_one

• N_pow_four_eq_D_pow_four_smul_one

25.61.3 GrassmannianMass

On the big cell of the Grassmannian Gr(2,4), a 2-plane is represented in the

Proved (5 declarations):

• on

• that

• massParameter

• transition_det_eq

• transition_transition_eq_neg