Gravity Ilgspatial Kernel Half Rung Components Band

The half-rung budget

The Information-Limited Gravity (ILG) framework proposes a specific modification to the Newton-Poisson equation that relates mass to gravitational potential. In Fourier space, this modification takes the form of a kernel, a multiplicative factor that depends on the spatial frequency k. The framework's central claim is that this kernel's amplitude, written as C, is not a free parameter but is forced by the same mathematical structure that produces the golden ratio. The specific declaration half_rung_components_band establishes a precise numerical window for this amplitude and for a related penalty term, anchoring the framework's prediction to a testable range.

The core of the argument is a simple algebraic identity involving the golden ratio φ (approximately 1.618). The framework defines a penalty term, J(φ), which equals φ − 3/2, and the kernel amplitude, C, which equals φ⁻². The half-rung budget identity states that these two quantities sum to exactly one half: J(φ) + C = 1/2. This is not an approximation; it follows directly from the defining property of the golden ratio, φ² = φ + 1. The declaration half_rung_components_band then uses this identity, along with the known bounds on φ, to prove that J(φ) lies strictly between 0.110 and 0.120, and that C lies strictly between 0.380 and 0.390.

This numerical band is the declaration's main practical output. It provides a sharp, falsifiable prediction: if an empirical fit to galaxy rotation curves ever determines the kernel amplitude to be outside this range, the framework's specific prediction is wrong. The declared band is also what distinguishes this value of C from a competing proposal. An alternative value, φ⁻³ᐟ² (approximately 0.486), is shown to violate the half-rung budget identity, as it would make the sum J(φ) + C greater than one half. The declaration thus does more than state a number; it provides a structural reason why one value is preferred over another.

In Recognition Science, this identity is interpreted as a budget: the cost of crossing one rung of the golden-ratio ladder, plus the cost-saving from finite-latency closure, exactly fills the half-rung interval. This interpretation is a model, not a theorem. What the machine-checked library proves are the algebraic facts: the closed form C = 2 − φ, the budget identity, and the resulting numerical band. The physical story about why these quantities should be added, and what they represent in terms of information flow, remains a hypothesis to be tested against data.

The declaration does not claim that the ILG modification itself is correct, nor that the golden ratio is the only possible source of such a kernel. It only establishes the internal consistency of a specific choice within the framework. The empirical test, comparing this prediction to galaxy rotation curves, is a separate step. The half-rung budget is the framework's way of saying: if you accept these premises, this is the number you must get.

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

/-- Numerical: `J(φ) + C ≈ 1/2`, with both individually positive. -/
theorem half_rung_components_band :
    (0.110 : ℝ) < Jphi_penalty ∧ Jphi_penalty < (0.120 : ℝ) ∧
    (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by
  refine ⟨?_, ?_, C_kernel_band.1, C_kernel_band.2⟩
  · unfold Jphi_penalty
    have h := phi_gt_onePointSixOne
    linarith
  · unfold Jphi_penalty
    have h := phi_lt_onePointSixTwo
    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.** `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

What this page does not claim

The ILG modification to gravity is physically correct. The golden ratio is the only possible source for the kernel amplitude. The half-rung budget identity explains why information is limited in gravity.

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: