gap_276_bounds
plain-language theorem explainer
The lemma establishes that the Recognition residue gap(276) = log(1 + 276/φ)/log φ lies strictly between 10.689 and 10.691, assuming the supplied logarithmic bounds on φ and on log(1 + 276/φ). Mass-spectrum calculations on the phi-ladder would cite it to fix the structural residue at this rung. The proof chains monotonicity of log with explicit numerical comparisons to phi_bounds and log_phi_bounds, then applies division inequalities to the quotient.
Claim. Assuming the lower and upper bounds on log φ together with the lower and upper bounds on log(1 + 276/φ), one has $10.689 < log(1 + 276/φ) / log φ < 10.691$.
background
The module RSBridge.GapProperties verifies algebraic and analytic properties of the gap function, defined by gap(Z) = log(1 + Z/φ) / log φ. This expression is the zero-parameter Recognition-side residue f^Rec (denoted 𝓕(Z) or F(Z) in the papers) that anchors fermion masses on the phi-ladder at the anchor scale μ⋆. The local setting treats gap as a definitional closed form whose behavior can be checked directly in Lean, in contrast to Standard-Model RG residues that require external kernels.
proof idea
The proof unfolds the definition of gap, invokes phi_bounds to obtain 1 < φ < 2, and applies log_phi_bounds to the phi hypotheses to bound log φ. It constructs strict inequalities for the argument 1 + 276/φ by comparing divisions against the numerical constants 1.618033 and 1.618034. Monotonicity of log then yields bounds on log(1 + 276/φ). These are combined with the numerical log hypotheses via lt_trans. The final step applies lt_div_iff₀ and div_lt_iff₀ to convert the log inequalities into the desired bounds on the quotient.
why it matters
This lemma supplies a concrete numerical interval for the residue at Z = 276 that enters the mass formula yardstick · φ^(rung − 8 + gap(Z)). It supports verification of the phi-ladder construction within the Recognition framework (T5 J-uniqueness, T6 phi fixed point). Although currently unused downstream, it closes a verification step for gap at this rung and is consistent with the zero-parameter claim for f^Rec. It touches the open question of matching the full mass spectrum without external parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.