Gravity Ilgspatial Kernel C Kernel Eq Two Minus Phi

The kernel amplitude

The golden ratio φ ≈ 1.618 is best known from geometry and number theory: it solves φ² = φ + 1, appears in the pentagon, and is the limit of ratios of consecutive Fibonacci numbers. In the Recognition Science framework, the same constant appears in a proposed modification to Newton's law of gravity. The modification writes the source-potential relation in Fourier space as w_ker(k) = 1 + C·(k₀/k)^α, where α ≈ 0.191 is a derived exponent. The quantity C is the spatial-kernel amplitude, and the declaration C_kernel_eq_two_minus_phi proves the identity C = 2 − φ ≈ 0.382.

The proof is algebraic and short. It relies only on the defining property φ² = φ + 1, from which φ⁻² = 2 − φ follows directly. The machine-checked library of formal theorems confirms this closed form, along with the positivity of C, its numerical band between 0.380 and 0.390, and a structural identity: the cost penalty J(φ) = φ − 3/2 plus C equals exactly 1/2. That half-rung budget identity gives C a complementary role: it is the cost-saving available from finite-latency closure, balancing the penalty for crossing one φ-rung.

In the framework's account, this identity resolves a prior ambiguity. An earlier account proposed C = φ^(−3/2) ≈ 0.486 from an unspecified three-channel argument. The new result singles out C = φ⁻² because it has the closed form 2 − φ, satisfies the budget identity, and matches the SPARC empirical fit A_fit = 0.38 to better than 1% on 147 galaxies. The competing value violates the budget identity and disagrees with SPARC by 28%.

What the declaration does not claim is as important as what it proves. The algebraic identities are theorems, but the structural three-channel factorization that picks C = φ⁻² as the theoretical prediction rather than an empirical fit is a hypothesis. The empirical fit is what discriminates. A future SPARC-class rotation-curve fit that determines the kernel amplitude and finds it inconsistent with 0.382 at better than 5% would falsify the prediction. The declaration also does not claim that the modified gravity law itself is established physics; it establishes the internal consistency of one parameter within that proposed law.

/-- **THEOREM.** `C = φ⁻² = 2 - φ`. Proof: `φ⁻² = 1/φ² = 1/(φ+1)`, and
    `(φ+1)(2-φ) = 2φ+2-φ²-φ = φ+2-(φ+1) = 1`, so `(φ+1)⁻¹ = 2-φ`. -/
theorem C_kernel_eq_two_minus_phi : C_kernel = 2 - phi := by
  unfold C_kernel
  have h_phi_pos := phi_pos
  have h_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  have h_phi_p1_pos : 0 < phi + 1 := by linarith
  -- Step 1: phi^(-2 : ℝ) = (phi^2)⁻¹ via rpow_neg and rpow_natCast
  have hpow : phi ^ (-(2 : ℝ)) = (phi ^ (2 : ℕ))⁻¹ := by
    rw [Real.rpow_neg h_phi_pos.le]
    congr 1
    rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) from by norm_num, Real.rpow_natCast]
  -- Step 2: (phi^2)⁻¹ = (phi+1)⁻¹ via phi^2 = phi + 1
  rw [hpow, h_sq]
  -- Step 3: (phi+1)⁻¹ = 2 - phi via the product identity (phi+1)(2-phi) = 1
  have key : (phi + 1) * (2 - phi) = 1 := by nlinarith [h_sq]
  exact inv_eq_of_mul_eq_one_right key

/-- **THE HALF-RUNG BUDGET IDENTITY.** `J(φ) + C = 1/2`, the structural
    forcing of `C = φ⁻²` as the unique spatial-kernel amplitude
    consistent with the first-rung cost penalty. -/
theorem half_rung_budget : Jphi_penalty + C_kernel = 1 / 2 := by
  rw [Jphi_penalty_eq_phi_minus_three_halves, C_kernel_eq_two_minus_phi]
  ring

/-- **THEOREM.** Numerical band: `0.380 < C < 0.390` from
    `1.61 < φ < 1.62` via the `2 - φ` closed form. -/
theorem C_kernel_band :
    (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by
  rw [C_kernel_eq_two_minus_phi]
  have h_lo : 1.61 < phi := phi_gt_onePointSixOne
  have h_hi : phi < 1.62 := phi_lt_onePointSixTwo
  refine ⟨?_, ?_⟩ <;> linarith

/-- The competing amplitude `C'` PLUS `J(φ)` exceeds the half-rung
    budget, violating the structural identity `J(φ) + C = 1/2`. -/
theorem C_competing_violates_budget :
    Jphi_penalty + C_kernel_competing > 1 / 2 := by
  have h1 : Jphi_penalty + C_kernel = 1 / 2 := half_rung_budget
  have h2 : C_kernel < C_kernel_competing := C_competing_gt_C_kernel
  linarith

/-- **THEOREM.** The three-channel factorization product
    `C = (longitudinal weight) × (transverse-collective weight)`
    with each weight equal to `channel_weight = φ⁻¹` reproduces
    `C = φ⁻²`. -/
theorem three_channel_factorization :
    C_kernel = channel_weight * channel_weight := by
  unfold C_kernel channel_weight
  rw [show ((-2 : ℝ)) = ((-1 : ℝ)) + ((-1 : ℝ)) from by ring]
  exact Real.rpow_add phi_pos _ _

What this page does not claim

The declaration does not prove that the modified gravity law is physically correct. The declaration does not derive the kernel amplitude from first principles; the three-channel factorization is a hypothesis. The declaration does not claim the competing value C = φ^(−3/2) is impossible, only that it violates the budget identity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/ILGSpatialKernel.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: