three_channel_factorization
plain-language theorem explainer
The three-channel factorization establishes that the ILG spatial kernel amplitude equals the square of the per-channel weight phi inverse. Gravity modelers in the Recognition Science setting cite the result to enforce C equals phi to the minus two over the competing phi to the minus three-halves value. The proof is a direct term reduction that unfolds the two definitions, rewrites the exponent via ring, and invokes real exponent additivity.
Claim. The spatial-kernel amplitude satisfies $C = w_c^2$ where the channel weight $w_c = phi^{-1}$, reproducing the closed form $C = phi^{-2}$.
background
The ILG framework modifies the Newton-Poisson source-potential relation in Fourier space by the kernel $w_{ker}(k) = 1 + C (k_0/k)^alpha$ with amplitude $C = phi^{-2}$. The module derives this value from the half-rung budget identity $J(phi) + phi^{-2} = 1/2$, which follows from $phi^2 = phi + 1$ alone and treats the kernel amplitude as the complement to the J-cost of crossing one phi-rung. The three-channel argument (one longitudinal channel and one transverse-collective channel, each weighted by phi inverse) originates in the Entropy paper and is contrasted with the Gravity_From_Recognition proposal of $C = phi^{-3/2}$.
proof idea
The term proof unfolds the definitions of C_kernel and channel_weight, rewrites the exponent -2 as the sum of two -1 exponents by ring, and applies Real.rpow_add under the positivity hypothesis on phi.
why it matters
The theorem supplies the factorization clause inside the master certificate ilgSpatialKernelCert, which populates the one-statement theorem ilg_spatial_kernel_one_statement. That statement asserts C equals phi to the minus two is forced by the half-rung budget, lies in the numerical band (0.380, 0.385), and matches the SPARC empirical fit to better than 1 percent. It resolves the prior ambiguity between the two accounts of C by enforcing the structural identity required by the phi fixed point and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.