Paper Specification Layer

This file keeps only the genuinely useful paper-notation bridge facts that are not already transparent from the main theorem file.

For the literal paper quantities

• paperCount n s = N_{n,s},

start in RequestProject.HadamardCn3ShortMain.

For the weak comparison surface, inspect

• quadraticForm_lindeberg_comparison_C3
• psi_sub_gaussianPsi_le_threeHalfInfluenceSum

in RequestProject.HadamardCn3WeakInvariance.

This file retains only the nontrivial normalization lemma comparing the project statistic threeHalfInfluenceSum with the paper's kernel-influence notation.

theorem paper_threeHalfInfluenceSum_eq_eight_kernelInfluence_sum (n : ℕ) (lam : Fin n → Fin n → ℝ) : threeHalfInfluenceSum n lam = 8 * ∑ k : Fin n, kernelInfluence n (mooKernel n lam) k * √(kernelInfluence n (mooKernel n lam) k)

The project statistic threeHalfInfluenceSum is exactly eight times the paper kernel-influence sum \sum_k \operatorname{Inf}_k(f)^{3/2} for f = mooKernel.