gap_24_bounds
plain-language theorem explainer
The lemma establishes that the Recognition residue gap(24) = log(1 + 24/φ)/log φ lies strictly between 5.737 and 5.74 under standard numerical bounds on log φ and on log(1 + 24/φ). Researchers verifying zero-parameter mass ladders or anchor residues in Recognition Science would cite it to confirm the fit at the 24-rung sector. The proof chains monotonicity of the logarithm with explicit interval comparisons on φ and scaling by the denominator via linarith and div_lt_iff.
Claim. Under the hypotheses that $0.481211 < log φ < 0.481212$ and $2.7613 < log(1 + 24/φ) < 2.7615$, the inequality $5.737 < log(1 + 24/φ)/log φ < 5.74$ holds.
background
The module establishes analytic properties of the structural residue gap(Z) := log(1 + Z/φ)/log φ, the proposed zero-parameter Recognition-side function f^Rec used in the mass framework. This definition appears in the RSBridge.Anchor import as the closed-form display function F(Z) at the anchor scale μ⋆. Upstream, phi_bounds states that φ is strictly between 1 and 2, while log_phi_bounds supplies the tight interval 0.481211 < log φ < 0.481212. The gap function itself is introduced as the integrated residue claimed to equal the mass anomalous dimension at the anchor.
proof idea
The tactic proof begins with simp only [gap] to unfold the definition, then obtains hphi := phi_bounds and hlogphi := log_phi_bounds h_low_phi h_high_phi. It constructs strict bounds on the argument 1 + 24/φ by comparing divisions against the constants 1.618033 and 1.618034 using div_lt_div_of_pos_left, transfers them to the logarithm via Real.log_lt_log, and combines with the supplied numerical bounds on log(1 + 24/φ) using lt_trans. The final scaling steps apply nlinarith and div_lt_iff₀ (or lt_div_iff₀) to produce the target inequalities for gap 24.
why it matters
This lemma supplies concrete numerical control on gap at Z = 24, a checkpoint inside the GapProperties module that supports the phi-ladder mass formula yardstick * φ^(rung - 8 + gap(Z)). It aligns with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain by confirming the residue behavior required for the eight-tick octave and D = 3 spatial dimensions. With zero recorded downstream uses, the result functions as an internal verification step rather than a direct parent for further theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.