half_rung_components_band
The declaration establishes numerical bounds showing that the first-rung J-cost penalty lies strictly between 0.110 and 0.120 while the spatial-kernel amplitude lies between 0.380 and 0.390. Researchers modeling Information-Limited Gravity would cite these bounds to confirm that the half-rung budget identity holds numerically with positive contributions from each term. The proof is a one-line wrapper that invokes the pre-established C_kernel_band and applies linear arithmetic to the golden-ratio bounds phi > 1.61 and phi < 1.62.
claimLet $J := Jphi_penalty = phi - 3/2$ denote the first-rung J-cost penalty and let $C := C_kernel = phi^{-2}$ denote the spatial-kernel amplitude. Then $0.110 < J < 0.120$ and $0.380 < C < 0.390$.
background
In the ILG framework the spatial kernel takes the form $w_{ker}(k) = 1 + C · (k_0/k)^α$ with amplitude $C = phi^{-2}$. The module defines Jphi_penalty := phi - 3/2 as the cost penalty for crossing one φ-rung and C_kernel := phi^{-2} as the complementary saving from finite-latency closure. These two quantities satisfy the half-rung budget identity J(φ) + C = 1/2, which follows directly from the defining equation φ² = φ + 1. Upstream results supply the tight bounds 1.61 < φ < 1.62.
proof idea
The proof applies the already-proved band theorem C_kernel_band to obtain the two inequalities on C_kernel. For the Jphi_penalty bounds it unfolds the definition Jphi_penalty := phi - 3/2 and invokes the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo, then closes each goal with linarith.
why it matters in Recognition Science
This numerical band theorem supports the structural claim that C equals φ^{-2} rather than the competing value φ^{-3/2} ≈ 0.486, thereby resolving the ambiguity noted in the module documentation between the Entropy paper and Gravity_From_Recognition. It supplies concrete verification of the half-rung budget identity that underpins the derivation of the kernel amplitude from first principles in the ILG framework. The result sits inside the broader Recognition Science forcing chain that fixes φ as the self-similar fixed point.
scope and limits
- Does not establish the exact algebraic identity J(φ) + C = 1/2.
- Does not derive the value of the golden ratio φ itself.
- Does not address the kernel exponent α.
- Does not connect to observational data or downstream applications.
formal statement (Lean)
176theorem half_rung_components_band :
177 (0.110 : ℝ) < Jphi_penalty ∧ Jphi_penalty < (0.120 : ℝ) ∧
178 (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by
proof body
Term-mode proof.
179 refine ⟨?_, ?_, C_kernel_band.1, C_kernel_band.2⟩
180 · unfold Jphi_penalty
181 have h := phi_gt_onePointSixOne
182 linarith
183 · unfold Jphi_penalty
184 have h := phi_lt_onePointSixTwo
185 linarith
186
187/-! ## §5. Discrimination from the competing hypothesis `C = φ⁻³ᐟ²`
188
189The competing value `C' = φ⁻³ᐟ² ≈ 0.486` from
190`Gravity_From_Recognition` does NOT satisfy the half-rung budget
191identity. We show this discrepancy formally.
192-/
193
194/-- The competing amplitude `C' = φ⁻³ᐟ²`. -/