Gravity Ilgspatial Kernel Three Channel Factorization

The kernel amplitude

The number in question is the amplitude C in a Fourier-space modification of the Newton-Poisson relation. In plain terms, the standard law of gravity gets an extra term that grows at large distances, and C sets its strength. The framework's library, a machine-checked collection of formal theorems, proves that C equals the inverse square of the golden ratio, roughly 0.382.

The proof rests on a factorization. The library defines a channel weight as the inverse of the golden ratio, about 0.618. The theorem three_channel_factorization states that C is exactly that weight multiplied by itself. The name reflects a physical picture: one longitudinal channel and one transverse-collective channel, each contributing the same weight, combine to give the total amplitude. The library proves this as an algebraic identity, not as an empirical fit.

This factorization settles a dispute between two earlier accounts. One proposed C = 0.382 from exactly this three-channel argument; another proposed a different value near 0.486 from an unspecified argument. The library proves the first value satisfies a budget identity: the cost penalty for crossing one golden-ratio rung plus C equals one half. The competing value violates that identity, so the library excludes it.

What the theorem does not claim is that this factorization is the physical mechanism. The library proves the algebra: C equals the product of two equal weights. Whether real gravity decomposes into those two channels is a separate hypothesis, not a proved theorem. The empirical check against galaxy rotation curves is a prediction, not a derivation.

/-- **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

/-- **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 _ _

/-- **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

/-- 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

What this page does not claim

The three-channel factorization is not proved to be the physical mechanism of gravity. The empirical agreement with SPARC rotation curves is a prediction, not a theorem. The library does not prove that the competing value is physically impossible, only that it violates a 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: