C_kernel_eq_two_minus_phi
The spatial-kernel amplitude C in the ILG gravity model equals 2 minus the golden ratio. Gravity modelers cite this to fix the prefactor in the Fourier-space kernel w_ker(k) = 1 + C (k0/k)^alpha. The proof unfolds the power definition, substitutes the quadratic relation phi squared equals phi plus one, and applies the product identity (phi plus one) times (2 minus phi) equals one to recover the inverse.
claim$C = 2 - ϕ$ where $C := ϕ^{-2}$ is the amplitude in the spatial kernel $w_{ker}(k) = 1 + C · (k_0/k)^α$.
background
The module formalizes the amplitude C in the ILG spatial kernel w_ker(k) = 1 + C (k0/k)^alpha, with alpha already fixed near 0.191. C is defined as phi to the power negative two. This choice satisfies the half-rung budget identity J(phi) + C = 1/2, which complements the first-rung cost penalty J(phi) = phi minus 3/2 and selects phi^{-2} over the prior alternative phi^{-3/2}.
proof idea
Unfolds the definition of C_kernel. Applies the upstream lemma phi_sq_eq to replace phi squared with phi plus one. Rewrites the negative real power via rpow_neg and rpow_natCast. Establishes the product identity (phi + 1)(2 - phi) = 1 by nlinarith. Concludes with inv_eq_of_mul_eq_one_right.
why it matters in Recognition Science
This theorem supplies the closed form required by half_rung_budget and the master certificate ilgSpatialKernelCert. It enforces the structural forcing of C = phi^{-2} consistent with J-uniqueness and the phi fixed point. The result feeds the one-statement theorem ilg_spatial_kernel_one_statement that collects positivity, numerical band, and factorization for the ILG kernel.
scope and limits
- Does not derive the kernel exponent alpha.
- Does not establish the three-channel factorization.
- Does not perform the SPARC empirical fit.
- Does not generalize to higher rungs or other kernels.
Lean usage
rw [C_kernel_eq_two_minus_phi]formal statement (Lean)
98theorem C_kernel_eq_two_minus_phi : C_kernel = 2 - phi := by
proof body
Tactic-mode proof.
99 unfold C_kernel
100 have h_phi_pos := phi_pos
101 have h_sq : phi ^ 2 = phi + 1 := phi_sq_eq
102 have h_phi_p1_pos : 0 < phi + 1 := by linarith
103 -- Step 1: phi^(-2 : ℝ) = (phi^2)⁻¹ via rpow_neg and rpow_natCast
104 have hpow : phi ^ (-(2 : ℝ)) = (phi ^ (2 : ℕ))⁻¹ := by
105 rw [Real.rpow_neg h_phi_pos.le]
106 congr 1
107 rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) from by norm_num, Real.rpow_natCast]
108 -- Step 2: (phi^2)⁻¹ = (phi+1)⁻¹ via phi^2 = phi + 1
109 rw [hpow, h_sq]
110 -- Step 3: (phi+1)⁻¹ = 2 - phi via the product identity (phi+1)(2-phi) = 1
111 have key : (phi + 1) * (2 - phi) = 1 := by nlinarith [h_sq]
112 exact inv_eq_of_mul_eq_one_right key
113
114/-- `C` is positive. -/