ilg_spatial_kernel_one_statement
plain-language theorem explainer
The theorem establishes that the ILG spatial-kernel amplitude equals 2 minus phi, satisfies positivity and the half-rung budget identity with the first-rung J-cost penalty, factors as the square of the per-channel weight, lies in the numerical interval (0.380, 0.390), and excludes the competing amplitude phi to the minus three-halves. Galaxy rotation-curve modelers fitting SPARC data would cite the closed form and budget identity. The proof is a term-mode conjunction that assembles six sibling lemmas.
Claim. Let $C := ϕ^{-2}$, $J := ϕ - 3/2$, $C' := ϕ^{-3/2}$, and $w := ϕ^{-1}$. Then $C = 2 - ϕ$, $0 < C$, $J + C = 1/2$, $0.380 < C < 0.390$, $C = w · w$, and $J + C' > 1/2$.
background
The module derives the amplitude in the ILG kernel modification $w_ker(k) = 1 + C · (k_0/k)^α$ with $α ≈ 0.191$. C_kernel is defined as $ϕ^{-2}$ and Jphi_penalty as the first-rung J-cost $ϕ - 3/2$. The half-rung budget identity states that these two quantities sum to exactly 1/2, which follows from the relation $ϕ^2 = ϕ + 1$ alone. The competing amplitude C_kernel_competing is defined as $ϕ^{-3/2}$.
proof idea
The proof is a term-mode wrapper that directly constructs the six-way conjunction from the component results C_kernel_eq_two_minus_phi, C_kernel_pos, half_rung_budget, C_kernel_band, three_channel_factorization, and C_competing_violates_budget.
why it matters
This declaration consolidates the derivation of the spatial-kernel amplitude $C = ϕ^{-2}$ in the ILG framework and selects it over the competing value via the half-rung budget identity. It resolves the ambiguity between the three-channel factorization argument and the earlier unspecified three-channel claim. The result rests on the Recognition Composition Law and the self-similar fixed point for phi (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.