three_channel_factorization
The theorem shows that the ILG spatial-kernel amplitude C factors as the square of a single channel weight equal to phi inverse, confirming C equals phi to the minus two. Modelers of information-limited gravity kernels cite this to fix the amplitude in the Fourier-space modification of the Newton-Poisson relation. The term-mode proof unfolds the two definitions, rewrites the exponent minus two as minus one plus minus one, and applies the real power-addition rule under phi positivity.
claimLet $C$ be the spatial-kernel amplitude and let $w$ be the per-channel weight. Then $C = w^2$ with $w = 1/phi$, hence $C = phi^{-2}$.
background
The module formalizes the amplitude $C$ in the ILG kernel $w_ker(k) = 1 + C (k_0/k)^alpha$ with alpha already fixed near 0.191. C_kernel is defined directly as phi raised to minus two. The half-rung budget identity J(phi) + C = 1/2 follows from the Recognition Composition Law and the fixed-point relation phi squared equals phi plus one; it treats the J-cost penalty for crossing one rung and the finite-latency saving C as complementary contributions to the rung budget.
proof idea
The proof is a one-line wrapper. It unfolds C_kernel and channel_weight, rewrites the exponent -2 as the sum of two -1 terms by ring, and applies Real.rpow_add using phi positivity to obtain the product of two identical phi^{-1} factors.
why it matters in Recognition Science
This supplies the factorization clause inside the master certificate ilgSpatialKernelCert, which is invoked by the one-statement theorem ilg_spatial_kernel_one_statement. The clause selects C = phi^{-2} over the competing phi^{-3/2} value by enforcing the half-rung budget, thereby resolving the ambiguity between the Entropy paper and Gravity_From_Recognition accounts. It sits inside the phi-ladder construction and the RCL-derived constants.
scope and limits
- Does not derive the kernel exponent alpha from the RCL.
- Does not construct the three channels from an underlying graph or forcing chain.
- Does not address empirical SPARC fitting beyond the numerical band.
- Does not extend to higher-order kernel corrections or non-power terms.
formal statement (Lean)
245theorem three_channel_factorization :
246 C_kernel = channel_weight * channel_weight := by
proof body
Term-mode proof.
247 unfold C_kernel channel_weight
248 rw [show ((-2 : ℝ)) = ((-1 : ℝ)) + ((-1 : ℝ)) from by ring]
249 exact Real.rpow_add phi_pos _ _
250
251/-! ## §7. Master certificate -/
252
253/-- **ILG SPATIAL-KERNEL AMPLITUDE MASTER CERTIFICATE.**
254
255Six clauses, all derived from the RCL and `φ² = φ + 1`:
256
2571. **closed_form**: `C = 2 - φ` (from `φ⁻¹ = φ - 1`).
2582. **positivity**: `0 < C`.
2593. **budget**: `J(φ) + C = 1/2` (the half-rung budget identity).
2604. **band**: `C ∈ (0.380, 0.385)` from `φ ∈ (1.61, 1.62)`.
2615. **factorization**: `C = (1/φ) · (1/φ)` (three-channel decomposition).
2626. **competing_excluded**: `C' = φ⁻³ᐟ²` violates the budget identity.
263-/