channel_weight_eq
plain-language theorem explainer
channel_weight_eq establishes that the per-channel ladder weight equals φ − 1. Workers on the ILG spatial kernel cite it to fix the three-channel product at φ^{-2}. The term proof unfolds the definition and reduces via the golden-ratio quadratic identity.
Claim. The per-channel ladder weight defined by $φ^{-1}$ satisfies $φ^{-1} = φ - 1$.
background
The ILG Spatial-Kernel module derives the Fourier-space amplitude C = φ^{-2} for the kernel w_ker(k) = 1 + C · (k_0 / k)^α. It rests on a three-channel factorization in which each channel carries the ladder weight φ^{-1}. The half-rung budget identity J(φ) + φ^{-2} = 1/2 then selects this value of C over the earlier alternative φ^{-3/2}.
proof idea
The term proof unfolds channel_weight to phi ^ (-1), rewrites the negative exponent via zpow_neg and one_div, invokes phi_sq_eq to obtain φ² = φ + 1, then finishes with field_simp and linarith.
why it matters
This pins the spatial-kernel amplitude to φ^{-2}, resolving the discrepancy between the entropy-paper three-channel value and the Gravity_From_Recognition alternative. It completes the structural core of the module and supplies the half-rung budget identity used by the Recognition forcing chain (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.