channel_weight
plain-language theorem explainer
Defines the per-channel ladder weight as φ^{-1}. Researchers deriving the ILG spatial kernel amplitude C would cite this when assembling the three-channel factorization. It is introduced as a direct definition with no computational steps or lemmas.
Claim. The per-channel ladder weight is defined by $w = ϕ^{-1}$.
background
In the ILG Spatial-Kernel module the Fourier modification of the Newton-Poisson relation is written w_ker(k) = 1 + C · (k_0/k)^α with α already fixed by GravityParameters. The module documentation states that C = φ^{-2} follows from the half-rung budget identity J(φ) + C = 1/2, which is an algebraic consequence of φ² = φ + 1 alone. This definition supplies the common weight φ^{-1} for the longitudinal and transverse-collective channels in the three-channel factorization argument.
proof idea
This is a direct definition that assigns channel_weight to phi raised to the power of negative one. No lemmas are applied and no tactics are used; the declaration is the base assignment that later theorems unfold.
why it matters
The definition supplies the per-channel weight that enables the three_channel_factorization theorem (C_kernel = channel_weight * channel_weight) and the ILGSpatialKernelCert structure (closed_form, budget, and factorization clauses). It feeds the one-statement theorem ilg_spatial_kernel_one_statement that certifies C = 2 - φ and the numerical band (0.380, 0.385). It resolves the prior discrepancy between the entropy-paper value φ^{-2} and the earlier φ^{-3/2} proposal by anchoring the factorization to the Recognition Science phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.