log_upper_bound_phi_hypothesis
plain-language theorem explainer
The declaration defines the proposition that log(1.618034) is strictly less than 0.481213, supplying an upper bound on log phi for numerical control of the gap residue. Researchers verifying mass-ladder intervals at specific Z values would cite it when tightening bounds on gap(24) and gap(276). It is introduced as a direct definition whose truth rests on external Taylor expansion rather than an internal derivation.
Claim. The upper bound hypothesis asserts that $log(1.618034) < 0.481213$.
background
The module supplies Lean-checked properties of the structural residue gap(Z) = log(1 + Z/φ) / log φ, where φ ≈ 1.618034. This gap functions as the zero-parameter Recognition-side residue f^Rec in the mass formula, contrasting with Standard-Model RG residues that require external kernels. The local setting stresses that gap is definitional, so its algebraic and analytic behavior can be verified directly.
proof idea
This is a definition that directly encodes the numerical inequality as a Prop. No lemmas or tactics are applied; the bound is asserted from external verification.
why it matters
The hypothesis is required by gap_24_bounds and gap_276_bounds to produce the concrete intervals (5.737, 5.74) for gap(24) and (10.689, 10.691) for gap(276). It also feeds log_phi_bounds, which pins log phi inside (0.481211, 0.481213). These bounds support the phi-ladder mass assignments and the T5–T6 steps of the forcing chain that fix phi as the self-similar point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.