log_171p6_upper_hypothesis
plain-language theorem explainer
This definition encodes the numerical hypothesis that log(1 + 276/φ) < 5.1444 with φ approximated as 1.618033. Researchers bounding the structural residue gap(276) cite it to close the interval (10.689, 10.691) in the mass framework. The declaration is a direct one-line definition of the inequality as a proposition with no further computation.
Claim. The hypothesis states that $log(1 + 276 / φ) < 5.1444$, where $φ ≈ 1.618033$ and $log$ denotes the natural logarithm.
background
The gap function is defined as $gap(Z) = log(1 + Z/φ) / log φ$, serving as the zero-parameter Recognition-side residue $f^{Rec}$ (also denoted $𝓕(Z)$) in the mass framework. This module supplies Lean-verified algebraic and analytic properties of gap(Z), contrasting with Standard-Model RG residues that require external kernels. Upstream definitions establish gap as the product of closure and Fibonacci factors or the closed-form display function at the anchor scale μ⋆, with the claim that the integrated mass anomalous dimension equals gap(ZOf i).
proof idea
This is a direct definition of the proposition. No lemmas or tactics are applied; the declaration simply states the concrete inequality using Real.log and the supplied decimal constants.
why it matters
The hypothesis is required by the downstream lemma gap_276_bounds to establish the tight numerical interval 10.689 < gap(276) < 10.691. It supports the Recognition mass formula (yardstick · φ^(rung - 8 + gap(Z))) and the phi-ladder structure within the T0-T8 forcing chain. It touches the open verification of numerical bounds for the structural residue at key Z values such as 276.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.