gap_lepton_pos
plain-language theorem explainer
The theorem establishes that the gap correction for leptons at the integer parameter 1332 is strictly positive. Researchers reconciling the structural rung mass formula with the gap-corrected anchor mass in the Recognition Science framework would cite this to confirm the sign of the lepton anomalous-dimension correction. The proof is a short tactic sequence that unfolds the gap definition and applies real-logarithm positivity to both the numerator argument exceeding 1 and the denominator using the known inequality 1 < phi.
Claim. The gap correction for leptons at the specified rung parameter satisfies $0 < g(1332)$, where $g$ denotes the gap function arising as the ratio of logarithms that encodes the integrated mass anomalous dimension.
background
The module compares two mass expressions: the structural rung formula (no gap) given by phi raised to a power divided by normalization factors, and the anchor mass formula that multiplies by an exponential of gap(ZOf f) times log phi. The gap term is precisely the integrated running-mass anomalous dimension from the anchor scale to the physical scale. For leptons the effective integer parameter is 1332. Upstream, the positivity of phi is supplied by the lemma one_lt_phi, while the gap definition itself traces to the product of closure and Fibonacci factors in Gap45.Derivation.
proof idea
The proof unfolds the gap definition to expose a ratio of real logarithms. It applies the positivity of division, then constructs a subproof that 1 + 1332/phi exceeds 1 by invoking positivity of phi and division, and finally applies the positivity of the logarithm to the denominator via the upstream fact 1 < phi.
why it matters
This result is assembled into the scheme reconciliation certificate theorem, which collects the positive-gap statements for neutrinos, up-type quarks, down-type quarks, and leptons together with a hypothesis-satisfiability condition. It thereby confirms that the gap correction for leptons aligns with the leading-log part of the two-loop RGE engine, consistent with the phi-ladder and the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.