gap_24_lt_gap_276
plain-language theorem explainer
The theorem establishes gap(24) < gap(276) for the Recognition residue gap(Z) = ln(1 + Z/φ)/ln φ. Mass-spectrum calculations cite the ordering when placing rungs 24 and 276 on the phi-ladder. The short tactic proof obtains the strict monotonicity of gap on nonnegative integers, decides the natural-number comparison 24 < 276, and applies simpa.
Claim. $gap(24) < gap(276)$ where $gap(Z) := ln(1 + Z/φ)/ln φ$ for integer $Z$.
background
The module records Lean-verified properties of the structural residue gap(Z) = ln(1 + Z/φ)/ln φ, presented as the zero-parameter Recognition-side residue f^{Rec} that equals the integrated mass anomalous dimension at the anchor scale. The definition appears in RSBridge.Anchor as the closed-form display function F(Z) and is reused across AnchorPolicy and Gap45.Derivation. Strict monotonicity of gap on nonnegative integers is established upstream by positivity of φ and of ln φ together with the increasing character of the logarithm.
proof idea
One-line wrapper that applies the upstream theorem gap_strictMono_on_nonneg. It decides the comparison (24 : ℕ) < (276 : ℕ) and uses simpa to transfer the inequality to the real-valued gap function.
why it matters
The result supplies a concrete ordering check inside the GapProperties module that supports rung placement in the mass formula yardstick · φ^(rung - 8 + gap(Z)). It is consistent with the phi-ladder and eight-tick octave of the forcing chain (T5-T8) but has no downstream dependents yet. It closes a direct verification that gap remains strictly increasing between the cited integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.