log_171p6_lower_hypothesis
plain-language theorem explainer
This definition encodes the numerical hypothesis that log(1 + 276/φ) exceeds 5.1442 with φ set to 1.618034. Mass-ladder calculations in Recognition Science cite it to pin the structural residue gap(276) inside a narrow interval. The declaration is a direct Prop definition of the inequality with no additional reduction steps.
Claim. Define the proposition $5.1442 < log(1 + 276/φ)$ where $φ = 1.618034$.
background
The module RSBridge.GapProperties supplies Lean-checked algebraic and analytic properties of the gap function, written gap(Z) = log(1 + Z/φ) / log φ. This quantity is the proposed zero-parameter Recognition-side residue f^{Rec} used in the mass framework, in contrast to Standard-Model RG residues that require external kernels. The present definition supplies one concrete numerical lower bound on the logarithm term that appears inside gap(276). Upstream structures from ClassicalBridge.Fluids.CPM2D.Hypothesis and Foundation.UniversalForcingSelfReference supply the broader context of projection-defect and meta-realization axioms, but the local content is the isolated inequality.
proof idea
The declaration is a one-line definition that directly states the inequality (5.1442 : ℝ) < Real.log (1 + 276 / (1.618034 : ℝ)) as a Prop.
why it matters
The definition is invoked inside gap_276_bounds to conclude 10.689 < gap(276) < 10.691. That interval fixes the 276 rung on the phi-ladder and thereby determines the corresponding mass value via the yardstick · φ^(rung - 8 + gap(Z)) formula. It therefore contributes to the T6 self-similar fixed point and T7 eight-tick octave structure of the forcing chain while remaining inside the alpha band verification. No open scaffolding is closed by this definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.