log_lower_bound_phi_hypothesis
plain-language theorem explainer
This definition encodes the proposition 0.481211 < log(1.618033) as a reusable hypothesis for numerical bounds on the gap function. Researchers deriving mass spectra on the phi-ladder cite it to constrain gap(24) and gap(276) to sub-percent intervals. It is realized as a direct definition of the inequality, with the module comment recording external Taylor expansion verification.
Claim. $0.481211 < log(1.618033)$, where the numerical argument approximates the golden ratio used in the gap residue.
background
The RSBridge.GapProperties module supplies Lean-checked analytic properties of the structural residue gap(Z) = log(1 + Z/φ) / log φ, treated as the zero-parameter Recognition-side residue f^{Rec} in the mass framework. Unlike Standard-Model RG residues that require external kernels, gap is definitional, permitting direct algebraic and analytic verification inside Lean. The local setting is therefore the provision of concrete numerical anchors for the phi-ladder mass formula yardstick · φ^(rung - 8 + gap(Z)). Upstream results supply hypothesis bundles from fluid models and recognition-weighted derivations that frame the broader context in which these bounds are applied.
proof idea
The declaration is a direct definition of the Prop (0.481211 : ℝ) < Real.log (1.618033 : ℝ). No internal lemmas or tactics are invoked; the accompanying comment states that the inequality was verified externally via Taylor expansion. Downstream lemmas such as log_phi_bounds import the definition by name and substitute it directly into the target interval statement.
why it matters
The definition supplies the lower hypothesis for log_phi_bounds, gap_24_bounds and gap_276_bounds, which in turn tighten the numerical intervals required by the mass formula on the phi-ladder. It therefore anchors the concrete values of constants such as ħ = φ^{-5} and G = φ^5 / π that appear in the T5–T8 forcing chain. By providing a Lean-checked placeholder for the logarithm of the self-similar fixed point φ, the definition closes a numerical gap between the abstract Recognition Composition Law and the explicit bounds needed for gap(Z) at physically relevant Z values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.