pith. machine review for the scientific record. sign in
theorem proved term proof high

cabibbo_scaling_forced

show as:
view Lean formalization →

The torsion overlap on the cubic ledger minus the Cabibbo radiative correction equals phi to the minus three minus three-halves times the fine-structure constant. Researchers deriving CKM parameters in Recognition Science cite this result to anchor the geometric origin of the scaling factor. The proof is a one-line term wrapper that unfolds the two definitions and applies ring normalization.

claimLet $T$ be the 3-generation torsion overlap on the cubic ledger and $C$ the Cabibbo radiative correction. Then $T - C = phi^{-3} - (3/2) alpha$, where $alpha$ is the fine-structure constant.

background

The MixingGeometry module formalizes cubic voxel topology constraints that force CKM and PMNS mixing parameters. Torsion_overlap is defined as $phi^{-3}$, the delocalization of the first generation across three spatial dimensions. Cabibbo_radiative_correction is defined as $(3/2) alpha$, arising from six faces divided by four vertex-edge weights. The fine-structure constant $alpha$ is imported from Constants.Alpha as the reciprocal of its inverse, while the abstract Constants bundle from LawOfExistence supplies the overall constant structure.

proof idea

The proof is a term-mode wrapper. It unfolds torsion_overlap and cabibbo_radiative_correction, then applies the ring tactic to confirm the algebraic identity holds by direct substitution.

why it matters in Recognition Science

This theorem establishes that the Cabibbo scaling factor is forced by the torsion overlap and face-mediated radiative corrections within the cubic geometry. It fills a required step in the mixing-matrix chain of the Recognition Science framework, connecting to the phi-ladder (T5-T8) and the alpha band. No downstream theorems are listed, leaving its use in full CKM derivations as an open extension.

scope and limits

formal statement (Lean)

  92theorem cabibbo_scaling_forced :
  93    torsion_overlap - cabibbo_radiative_correction = phi ^ (-3 : ℤ) - (3/2) * Constants.alpha := by

proof body

Term-mode proof.

  94  unfold torsion_overlap cabibbo_radiative_correction
  95  ring
  96
  97end MixingGeometry
  98end Physics
  99end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.