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 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.17 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.18 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.19 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.20 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.21 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.22 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.23 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.24 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.25 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.26 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.27 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.28 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.29 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.30 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.31 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.32 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.33 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.34 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.35 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.36 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.37 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.38 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.39 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.40 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.41 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.42 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.43 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.44 IdeleGroup

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

Proved (4 declarations):

• resolution

• RationalIdeleGroup

• diagonalEmbedding_injective

• adicCompletionIntegers_toSubring_eq_integer

25.1.45 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.46 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.47 ScaleShadowHalfDensity

For

Proved (4 declarations):

• shadow_centered_exponent

• dilationCharacter_shadow_eq_inv

• dilationCharacter_shadow_involution

• critical_line_iff_unitary_with_shadow

25.1.48 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.49 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.50 MomentumGeneratorNoPointSpectrum

Source: ‘ONON5213.tex‘ (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.51 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.52 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.53 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.54 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.55 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.56 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.57 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.58 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.59 CasimirIdentity

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

Proved (2 declarations):

• casimir_eq_neg_riemann_form

• casimir_value

25.1.60 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.61 FiniteMomentFactorization

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

Proved (2 declarations):

• rawMoment

• triple_monomial_factorization

25.1.62 PadicFieldHaarMeasure

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

Proved (2 declarations):

• to

• fieldHaarMeasure_closedBall

25.1.63 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.64 PadicMultiplicativeMeasure

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

Proved (2 declarations):

• in

• measurable_multiplicativeDensity

25.1.65 PadicScalingHaar

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

Proved (2 declarations):

• isAddHaarMeasure_map_scaleAddEquiv

• map_scaleAddEquiv_apply

25.1.66 PadicShellMeasure

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

Proved (2 declarations):

• measurableSet_span_pow

• haarMeasure_shell

25.1.67 PrimeHankelFisherSpecialization

This file instantiates the abstract infinite weighted-polynomial positivity theorem

Proved (2 declarations):

• fisherWeight_nonneg

• fisher_polynomial_tsum_pos

25.1.68 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.69 SpectralWeil

This file formalizes ‘thm:spectral-weil‘ (ONON52, 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.70 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.71 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.72 FiniteVandermondeExpansionKernel

Pointwise polynomial expansion underlying the arbitrary finite-support

Proved (1 declaration):

• vandermonde_sq_expansion

25.1.73 GramPositivityBoundary

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

Proved (1 declaration):

• gram_posSemidef

25.1.74 PadicHaarMeasure

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

Proved (1 declaration):

• haarMeasure_univ

25.1.75 PadicOriginMeasure

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

Proved (1 declaration):

• haarMeasure_singleton_zero

25.1.76 PadicShellNorm

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

Proved (1 declaration):

• norm_eq_of_mem_shell

25.1.77 PadicZetaIntegral

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

Proved (1 declaration):

• haarMeasure_span_pow

25.1.78 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.79 PrimeGasPartition

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

Proved (1 declaration):

• partition_eq_riemannZeta

25.1.80 PrimeHankelFiniteGramStrict

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

Proved (1 declaration):

• weighted_eval_sq_sum_pos

25.2 Thread Weil-Parity

25.2.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.2.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.2.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.3 Number Theory — Arithmetic Layer

25.3.1 BSDPointCounts

Source: ONON 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.3.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.3.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.3.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.3.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.3.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.3.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.3.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.3.9 ZagierMZVGrowth

Source: ONON5213.tex, "Loop Transcendence from the Plastic Constant"

Proved (4 declarations):

• mzvDim

• mzvDim_matches_source

• plastic_constant_cubic_approx

25.3.10 GaussSumModulus

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

Proved (1 declaration):

• gaussSum_norm_eq_sqrt_card

25.3.11 ZetaNegativeIntegers

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

Proved (1 declaration):

• riemannZeta_neg_three

25.4 Celestial Holography — Further Results

25.4.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.4.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.4.3 GrassmannianSelfDuality

Source: ONON5213.tex, 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.4.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.4.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.5 Quantum Gravity — Further Results

25.5.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.5.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.5.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.5.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.6 Standard Model — Further Results

25.6.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.6.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.6.3 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.6.4 KoideRelation

Source: ONON5213.tex, "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.6.5 MajoranaCondition

Sources:

Proved (5 declarations):

• epsilon

• epsilon_sq

• epsilon_det

• zitterbewegung_frequency

• zitterbewegung_period

25.6.6 ComplementaryPairs

Source: ONON5213.tex, "Counting Complementary Pairs" (thm:three-partitions),

Proved (2 declarations):

• complementaryPairings

• exactly_three_complementary_pairings

25.7 General Relativity — Further Results

25.7.1 Rigidity

This file formalizes ‘thm:rigidity‘ (ONON52, cited 10×):

Proved (2 declarations):

• graviton_shadow_dimension

25.8 Cosmology

25.8.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.8.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.8.3 AbelHaloPair

Thread H of ‘docs/FORMALIZATION_PLAN.md‘, from ONON5213.tex Chapter "Dark Matter:

Proved (6 declarations):

• pseudo_isothermal_eq

• hasDerivAt_sq_sub

• hasDerivAt_sq_add

• abel_forward

• abel_inverse_eval

• dm_profile_boxed

25.8.4 DarkMatterGammaRatio

Source: ONON5213.tex, "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.9 String Theory

25.9.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.10 Thread S — Signature and Inertia

25.10.1 SignatureInertia

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

Proved (1 declaration):

• inertia_sum

25.11 Yang–Mills

25.11.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.12 Core Theorems and Grassmannian Geometry

25.12.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.12.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.12.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