C_competing_gt_C_kernel
plain-language theorem explainer
The declaration proves that the ILG spatial-kernel amplitude phi^{-2} is strictly smaller than the competing proposal phi^{-3/2}. Gravity modelers selecting between the entropy-paper and Gravity_From_Recognition derivations of the kernel constant would cite this comparison to eliminate the larger value. The proof is a direct term-mode reduction that unfolds the two power expressions and applies the real-exponent monotonicity lemma under the upstream fact 1 < phi.
Claim. The spatial-kernel amplitude satisfies $C = ϕ^{-2} < C' = ϕ^{-3/2}$, where $C'$ denotes the competing amplitude.
background
The ILG module formalizes the Fourier-space kernel modification w_ker(k) = 1 + C (k_0/k)^α with amplitude C derived from the half-rung budget identity J(ϕ) + ϕ^{-2} = 1/2. This identity follows from ϕ² = ϕ + 1 alone and selects C = ϕ^{-2} over the alternative C' = ϕ^{-3/2} proposed in Gravity_From_Recognition. The module imports the definition of ϕ together with the lemma one_lt_phi establishing ϕ > 1, and defines both C_kernel := ϕ^{-2} and C_kernel_competing := ϕ^{-3/2}.
proof idea
The term proof unfolds the definitions of C_kernel and C_kernel_competing, invokes the upstream lemma one_lt_phi to obtain 1 < ϕ, and applies Real.rpow_lt_rpow_of_exponent_lt to the exponent comparison -(2 : ℝ) < -(3/2 : ℝ).
why it matters
This result is invoked directly by the downstream theorem C_competing_violates_budget, which combines it with the half-rung identity to show that Jphi_penalty + C_kernel_competing exceeds 1/2. It thereby resolves the ambiguity between the two prior accounts of C cited in the module documentation. Within the Recognition Science framework it reinforces selection of the structurally forced amplitude at the phi fixed-point step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.