gap_1332_bounds
plain-language theorem explainer
The lemma proves that gap(1332) lies strictly between 13.953 and 13.954. Researchers deriving electron structural mass from the phi-ladder in Recognition Science cite it to fix the exponent contribution for Z=1332. The tactic proof invokes phi_bounds and local log bounds, then chains monotonicity of log with rational comparisons to sandwich the scaled value.
Claim. $13.953 < g(1332) < 13.954$, where $g(n) = $ log$(1 + n/φ) /$ log$φ$ is the structural gap on the phi-ladder for integer $n$ (here $n=1332$ for the electron).
background
The module establishes T9 necessity: the electron mass formula is forced from T8 ledger quantization together with geometric constants. The phi-ladder supplies mass scales via yardstick times phi to a power involving rung offset plus gap(Z). Upstream, phi_bounds states that φ satisfies 1 < φ < 2. The gap function itself appears in Gap45.Derivation and is evaluated here at the electron Z-value 1332.
proof idea
Tactic proof begins with simp on the gap definition. It pulls phi_bounds to obtain 1 < φ < 2 and positivity of log φ. Separate blocks establish log(1 + 1332/φ) bounds by comparing the argument to rational approximations of φ and applying log monotonicity via log_824_lower and log_824_upper. Final steps multiply the log bounds by log φ and divide to recover the target interval on gap(1332).
why it matters
The result anchors the electron structural mass 2^{-22} φ^{51} inside the Necessity module and supplies the lower bound used by gap_minus_shift_bounds, lepton generation checks, and RecognitionCoupling. It completes the T9 step that converts T8 quantization into a concrete mass prediction, consistent with the phi fixed point and eight-tick octave. It leaves open the question of whether tighter analytic bounds can replace the numerical log comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.