log_15p83_upper_hypothesis
plain-language theorem explainer
This definition introduces a numerical hypothesis asserting that the natural log of (1 + 24/1.618033) is strictly less than 2.7615. Researchers bounding the structural residue gap(24) in the Recognition mass ladder would cite it to close the interval 5.737 < gap(24) < 5.74. The declaration is a direct definition of the inequality using concrete real constants for the golden-ratio approximation and the target bound.
Claim. Let $a = 1.618033$. The proposition asserts that $log(1 + 24/a) < 2.7615$.
background
The module supplies Lean-verified properties of the gap function, defined as gap(Z) = log(1 + Z/φ) / log φ, which functions as the zero-parameter Recognition-side residue f^Rec throughout the mass framework. This residue supplies the adjustment term in the phi-ladder mass formula yardstick * φ^(rung - 8 + gap(Z)). The present definition supplies one of the concrete numerical bounds needed to locate gap(24) inside a narrow interval.
proof idea
This is a direct definition of the Prop consisting of the stated inequality. No lemmas or tactics are invoked; the body simply records the comparison between the logarithm evaluated at the supplied constants and the target real number.
why it matters
The hypothesis is consumed by gap_24_bounds to prove the tight interval 5.737 < gap(24) < 5.74. It supports verification of the structural residue that enters the Recognition mass formula at every rung adjustment. In the broader framework the same gap function is tied to the phi fixed point (T6) and the eight-tick octave (T7), and the numerical bounds help confirm consistency with the J-uniqueness relation (T5) without external kernels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.