Gravity Ilgspatial Kernel Jphi Penalty Eq Phi Minus Three Halves

The half-rung penalty

The declaration Jphi_penalty_eq_phi_minus_three_halves is a theorem in the machine-checked library of formal theorems. It states that a quantity called the cost penalty, written J(φ), equals φ − 3/2, where φ is the golden ratio (1.618...). The cost penalty is a number that measures the price, in the framework's accounting, of crossing one rung of a discrete scale ladder. The theorem is a definitional identity: it unfolds the definition of J(φ) and shows it is exactly φ − 3/2, which is about 0.118.

The identity matters because it completes a budget. The framework also defines a kernel amplitude C = φ⁻² ≈ 0.382, which appears in a proposed modification of the Newton-Poisson relation in Fourier space. The theorem half_rung_budget proves that J(φ) + C = 1/2. That is, the penalty for crossing a rung plus the amplitude of the kernel exactly fills a half-rung interval. The two quantities are complementary: one is the cost, the other the saving, and together they account for the budget.

The budget identity does real work. A competing value for the amplitude, C = φ⁻³ᐟ² ≈ 0.486, was proposed in an earlier account. The theorem C_competing_violates_budget proves that this competing value would make J(φ) + C exceed 1/2, breaking the budget. The framework therefore singles out C = φ⁻² as the structurally forced value. It has the closed form 2 − φ, it satisfies the budget, and it sits in a numerical band between 0.380 and 0.390. The competing value fails all three checks.

What the theorem does not claim is important. The algebraic identity J(φ) = φ − 3/2 is proved. But the choice of C = φ⁻² as the theoretical prediction, rather than an empirical fit, rests on a three-channel factorization argument that is a hypothesis, not a theorem. The empirical check against SPARC rotation-curve data is a measurement, not a proof. The theorem itself says nothing about whether the modified gravity law is true; it only fixes the amplitude if the framework is assumed.

/-- The first-rung J-cost penalty has closed form `φ - 3/2`. -/
theorem Jphi_penalty_eq_phi_minus_three_halves :
    Jphi_penalty = phi - 3 / 2 := rfl

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

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

What this page does not claim

The theorem does not prove that the modified gravity law is correct. The theorem does not derive the three-channel factorization from first principles; that argument is a hypothesis. The theorem does not establish the empirical fit to SPARC data; that is a measurement, not a proof.

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: