pith. machine review for the scientific record. sign in
def definition def or abbrev high

cabibboFactor

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  95noncomputable def cabibboFactor : ℝ := 1 / phi^3

proof body

Definition body.

  96
  97/-- All five 1/φ instances are equal. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.