phi_inv3_lower_bound
plain-language theorem explainer
Physicists deriving CKM mixing angles from ledger geometry cite this result to bound the golden projection term in the V_us prediction formula. It asserts that the cube of the reciprocal golden ratio exceeds 0.2360. Researchers verifying the Cabibbo angle match within experimental error invoke the bound when combining it with alpha interval results. The proof is a one-line wrapper that extracts the lower component from the proven interval theorem in Numerics.Interval.PhiBounds.
Claim. $0.2360 < phi^{-3}$, where $phi$ denotes the golden ratio satisfying $phi^2 = phi + 1$.
background
The CKM Geometry module formalizes T11, deriving the CKM matrix elements as geometric couplings on the cubic ledger with explicit formulas for |V_us|, |V_cb|, and |V_ub|. The V_us prediction takes the form phi^{-3} minus (3/2) alpha, so a strict lower bound on phi^{-3} is required to close the interval arithmetic for the match theorem. The golden ratio enters via the self-similar fixed point of the Recognition forcing chain (T5 J-uniqueness and T6). Upstream, phi_inv3_zpow_bounds proves the tight interval (0.2360, 0.2361) containing phi^{-3} by rewriting the power as the reciprocal of phi cubed and invoking the identity phi cubed equals two phi plus one together with zpow_neg_coe_of_pos.
proof idea
The proof is a one-line wrapper that applies the first projection of phi_inv3_zpow_bounds. That upstream theorem rewrites phi^{-3} as the inverse of phi^3, substitutes the cubic identity phi^3 = 2 phi + 1, and uses norm_num together with zpow properties to obtain the concrete decimal bounds.
why it matters
This bound feeds V_us_match in the same module and jarlskog_match in MixingDerivation, both of which confirm the geometric CKM predictions against experiment within stated sigma. It supplies the phi interval half needed to close the T11 verification that |V_us| equals phi^{-3} minus (3/2) alpha. The result sits inside the phi-ladder structure originating from the eight-tick octave and D=3 spatial dimensions in the foundational forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.