phi_inv3_zpow_bounds
plain-language theorem explainer
This theorem pins down the numerical interval containing φ^{-3} to four decimal places. Researchers deriving CKM matrix elements or phi-ladder mass spectra cite it to control truncation error in predictions. The proof rewrites the power as the reciprocal of 2φ + 1, applies the known tight bounds on φ, and inverts the inequalities using the monotonicity of reciprocal on positives.
Claim. $0.2360 < φ^{-3} < 0.2361$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous bounds on the golden ratio φ using its algebraic properties and the relation φ² = φ + 1. Upstream, phi_cubed_eq states that φ³ = 2φ + 1, which follows directly from the Fibonacci recurrence. This zpow form is needed because some physics modules apply the exponent directly rather than composing the inverse power. Local setting: bounds are derived from sqrt(5) approximations leading to 1.618 < φ < 1.6185, then tightened further for the required precision.
proof idea
The proof first invokes phi_cubed_eq to obtain φ³ = 2φ + 1, rewrites the negative zpow as its reciprocal, then uses phi_tight_bounds to bound 2φ + 1 between 4.2360679 and 4.2360680. It inverts these inequalities via one_div_lt_one_div_of_lt and finally compares the resulting bounds to the target decimals 0.2360 and 0.2361 by transitivity.
why it matters
This declaration supplies the concrete numerical envelope required by the CKMGeometry module for its phi_inv3_lower_bound and phi_inv3_upper_bound theorems, which in turn support the V_us prediction within one sigma. It closes the legacy replacement noted in the module doc for direct zpow usage in physics derivations. Within the framework it anchors the phi-ladder rung at exponent -3, consistent with the self-similar fixed point property of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.