half_rung_components_band
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.