phi_inv3_upper_bound
plain-language theorem explainer
The theorem asserts that the cube of the reciprocal golden ratio is strictly less than 0.2361. CKM matrix modelers cite the bound when closing the interval arithmetic for the predicted Cabibbo angle V_us = φ^{-3} - (3/2)α. The proof is a direct term projection of the upper conjunct from the upstream interval theorem phi_inv3_zpow_bounds.
Claim. $φ^{-3} < 0.2361$, where $φ$ is the golden ratio.
background
The CKMGeometry module derives the three mixing angles from cubic ledger geometry. The Cabibbo element is given by the expression V_us_pred = φ^{-3} - (3/2)α, with the experimental anchor V_us_exp = 0.22500. The upstream theorem phi_inv3_zpow_bounds supplies the tight interval 0.2360 < φ^{-3} < 0.2361 by rewriting φ^3 = 2φ + 1 and inverting.
proof idea
One-line wrapper that applies the second conjunct of phi_inv3_zpow_bounds.
why it matters
The bound supplies the missing upper limit required by V_us_match, which verifies the geometric prediction lies inside one sigma of experiment. It also feeds jarlskog_match in MixingDerivation. The result sits inside T11 of the CKM geometry derivation and rests on the phi fixed point from the forcing chain T5-T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.