gapR_nat
plain-language theorem explainer
gapR applied to a natural number equals the integer gap function at the corresponding integer. Researchers deriving mass spectra from the phi-ladder cite this to interchange real and discrete residues seamlessly. The proof is a one-line simplification that unfolds the common logarithmic expression for both functions.
Claim. For any natural number $n$, $gapR(n) = gap(n)$, where $gapR(x) := log(1 + x/φ)/log φ$ and $gap(Z) := log(1 + Z/φ)/log φ$.
background
The structural residue gap(Z) is defined by gap(Z) = log(1 + Z/φ) / log φ for integer Z, acting as the Recognition-side residue f^{Rec} in the mass framework. gapR extends this definition to real arguments to enable analytic arguments such as strict concavity on [0, ∞). The module supplies Lean-verified properties of this residue, which is central to the zero-parameter mass formula.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definitions of gapR and gap. Since both unfold to the same expression log(1 + n/φ)/log φ after casting n to real or integer, the equality holds immediately.
why it matters
This theorem ensures consistency between discrete and continuous formulations of the gap residue, directly supporting the downstream result gap_diminishing_increments that proves strictly decreasing increments. It contributes to the properties of the phi-ladder used in deriving spatial dimensions D=3 and the fine-structure constant band. The result closes a basic interface between the integer gap in mass calculations and its real extension for concavity proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.