channel_weight_eq
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.
claimThe 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 in Recognition Science
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).
scope and limits
- Does not prove the three-channel factorization assumption.
- Does not derive the kernel exponent α.
- Does not address lattice discretization or higher-rung weights.
- Does not compare the amplitude to observational data.
formal statement (Lean)
231theorem channel_weight_eq : channel_weight = phi - 1 := by
proof body
Term-mode proof.
232 unfold channel_weight
233 rw [show (-(1 : ℝ)) = ((-1) : ℤ) from by norm_num]
234 rw [Real.rpow_intCast]
235 rw [zpow_neg, zpow_one, ← one_div]
236 have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
237 have h_sq := phi_sq_eq
238 field_simp
239 linarith
240
241/-- **THEOREM.** The three-channel factorization product
242 `C = (longitudinal weight) × (transverse-collective weight)`
243 with each weight equal to `channel_weight = φ⁻¹` reproduces
244 `C = φ⁻²`. -/