Gravity Ilgspatial Kernel Jphi Penalty Eq Jcost Phi

The half-rung identity

The golden ratio φ, approximately 1.618, is the unique positive number that satisfies φ² = φ + 1. This simple algebraic property is the engine behind a surprising equivalence in the Recognition Science framework. The declaration Jphi_penalty_eq_Jcost_phi proves that a quantity called the phi-penalty, defined as φ - 3/2, is exactly equal to the framework's fundamental cost function J evaluated at φ. In plain terms, the cost of a single recognition event at the golden-ratio scale is the same number that appears as a penalty term in a modified theory of gravity.

The phi-penalty itself has a direct geometric meaning. The golden ratio satisfies φ - 3/2 ≈ 0.118. This value is precisely half of the interval between 1 and φ, a half-rung on the framework's ladder of scales. The theorem Jphi_penalty_eq_Jcost_phi establishes that this half-rung interval is not an arbitrary construction but is forced by the definition of the cost function. The cost function J, which measures the price of recognition, must take this specific value at φ because of the algebraic identity φ² = φ + 1.

This equivalence is the keystone of a larger structure. The same module proves that this phi-penalty, plus another quantity C = φ⁻² ≈ 0.382, sums to exactly 1/2. The number C is the amplitude of a spatial kernel in the Information-Limited Gravity (ILG) framework, a modification of Newton's law. The theorem therefore shows that the cost of one recognition step and the strength of a gravity modification are complementary halves of a single budget. A competing value for C, φ^(-3/2) ≈ 0.486, is shown to violate this budget identity, reinforcing the uniqueness of the φ⁻² choice.

What the declaration does not claim is just as important. The theorem proves an algebraic equality between two defined quantities. It does not, by itself, prove that this specific gravity model is correct. The choice of the three-channel factorization that leads to C = φ⁻² is a hypothesis, not a theorem. The empirical check against galaxy rotation data is a separate measurement, not a consequence of the proof. The framework's library proves the mathematics; the physics remains a prediction to be tested.

/-- The first-rung J-cost penalty equals the J-cost evaluated at φ. -/
theorem Jphi_penalty_eq_Jcost_phi :
    Jphi_penalty = Cost.Jcost phi := by
  unfold Jphi_penalty Cost.Jcost
  have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
  have h_sq := phi_sq_eq
  field_simp
  nlinarith [sq_pos_of_pos phi_pos, h_sq]

/-- **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 theorem does not prove the ILG gravity model is physically correct. The choice of the three-channel factorization is a hypothesis, not a theorem. The empirical fit to galaxy data is a measurement, not a consequence of the 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: