cabibboFactor
plain-language theorem explainer
Recognition Science sets the Cabibbo mixing angle factor to one divided by the cube of the golden ratio phi. Particle physicists studying mixing angles and Recognition Science modelers tracking cross-domain invariants would cite the assignment. The definition is introduced as a direct real-number constant requiring no lemmas or reduction steps.
Claim. The Cabibbo mixing angle factor is defined to be $1/phi^3$, where $phi$ is the golden ratio.
background
Module C22 collects one-over-phi invariants as the attractor for negative-rung quantities such as decay rates, dampings, target ratios, and mixing angles. The Cabibbo angle appears explicitly as the instance approximated by one over phi cubed. Companion facts established in the same module are that one over phi is positive, less than one, and equals phi minus one.
proof idea
The declaration is a direct definition that assigns the real number one over phi cubed. No lemmas are applied and no tactics are used; the value is set explicitly to serve as input for subsequent bounds.
why it matters
The definition supplies the explicit value for the Cabibbo factor inside the one-over-phi family. It is used by the theorem proving the factor lies in (0,1) and is smaller than one over phi, and by the certificate structure that gathers all one-over-phi identities. The assignment realizes the module claim that the Cabibbo angle belongs to the phi-ladder and the self-similar fixed point of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.