C_kernel_eq_two_minus_phi
plain-language theorem explainer
The spatial-kernel amplitude C in the ILG model equals 2 minus φ. Gravity researchers cite this closed form when substituting the kernel into the modified Poisson relation. The proof is an algebraic reduction that invokes the golden-ratio identity φ² = φ + 1 and the product (φ + 1)(2 - φ) = 1.
Claim. The spatial-kernel amplitude defined by $C = ϕ^{-2}$ satisfies $C = 2 - ϕ$.
background
The Information-Limited Gravity framework writes the Fourier-space modification of the Newton-Poisson source-potential relation as w_ker(k) = 1 + C · (k_0 / k)^α. The module derives the spatial-kernel amplitude C from first principles as φ^{-2} ≈ 0.382. C_kernel is defined as phi raised to the power negative two.
proof idea
The tactic proof unfolds the definition of C_kernel. It obtains phi_sq_eq to replace φ² with φ + 1, rewrites the negative power via rpow_neg and rpow_natCast, establishes the product identity (φ + 1)(2 - φ) = 1 by nlinarith, and concludes with inv_eq_of_mul_eq_one_right.
why it matters
This supplies the closed form to C_kernel_band, C_kernel_pos, C_kernel_lt_half, half_rung_budget, and ilgSpatialKernelCert. It resolves the prior ambiguity between the entropy paper value φ^{-2} and the Gravity_From_Recognition value φ^{-3/2} by enforcing consistency with the half-rung budget identity. The result is collected in the one-statement theorem ilg_spatial_kernel_one_statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.