cabibbo_in_unit
plain-language theorem explainer
The theorem shows that the Cabibbo factor 1/phi cubed lies strictly between zero and 1/phi. Recognition Science researchers working on cross-domain 1/phi attractors cite it to confirm the mixing-angle instance fits the pattern. The proof is a short term-mode argument that unfolds the two definitions then applies division-positivity and an ordering reduction via nlinarith on the golden-ratio identities.
Claim. Let $phi > 1$ be the golden ratio. Then $0 < 1/phi^3 < 1/phi$.
background
The CrossDomain.PhiInverseInvariants module treats 1/phi as the canonical attractor for negative-rung quantities such as decay rates and mixing factors. cabibboFactor is defined as 1/phi cubed to capture the Cabibbo angle; phiInv is defined as 1/phi. The module lists parallel instances including the Gini ceiling and senolytic target ratio, all asserted to equal 1/phi. Upstream lemmas one_lt_phi and phi_sq_eq supply the facts phi > 1 and phi squared equals phi plus one.
proof idea
Unfold cabibboFactor and phiInv. The lower bound follows from div_pos applied to one_pos and pow_pos phi_pos 3. The upper bound rewrites via div_lt_div_iff0 to the comparison phi < phi cubed, then closes with nlinarith using one_lt_phi, phi_pos, and the identity from phi_sq_eq.
why it matters
The result is invoked by phiInverseInvariantsCert to certify the full set of 1/phi invariants. It supplies the Cabibbo instance for the C22 cross-domain claim that independent domains converge on the same attractor. The placement links particle-physics mixing to the phi-ladder structure while remaining silent on the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.