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

row_vus_eq_geometry

show as:
view Lean formalization →

The equality asserts that the predicted Cabibbo element from Recognition Science geometry equals the three-generation torsion overlap minus the cube-face radiative correction. Physicists checking quark-mixing predictions against PDG data would cite it to confirm the geometric origin of |V_us|. The proof is a one-line wrapper that invokes the upstream derivation theorem from the mixing module.

claim$V_{us}^{pred} = phi^{-3} - (3/2) alpha$, where the left side is the geometric prediction for the up-strange CKM element, the first right-hand term is the torsion overlap on the cubic ledger, and the second term is the radiative correction forced by the six cube faces.

background

The CKMElementScoreCard module collects leading CKM magnitudes predicted from cube geometry under Recognition Science. Torsion overlap is the delocalization of the first generation across three spatial dimensions and equals phi to the minus three. Cabibbo radiative correction equals (3/2) times alpha, obtained from six faces divided by four vertex-edge weight. The module documentation states the explicit form V_us_pred = phi^{-3} - (3/2)alpha together with the one-sigma falsifier against PDG values. This row rests on the upstream theorem vus_derived, which states that the Cabibbo element is derived from the golden projection minus the radiative fine-structure correction.

proof idea

The proof is a one-line wrapper that applies the theorem vus_derived. That theorem unfolds the definitions of the predicted element, torsion overlap, and radiative correction, then closes the equality by reflexivity.

why it matters in Recognition Science

This declaration supplies the V_us geometric equality required by the certification theorem ckmElementScoreCardCert_holds, which assembles the scorecard from the three row theorems and their geometric matches. It realizes the Phase 2 P2-CKM prediction stated in the module documentation, where the golden projection phi^{-3} is corrected by the small alpha term to match the observed |V_us| within one sigma. The construction uses the cubic ledger forced by D = 3 spatial dimensions in the Recognition Science forcing chain.

formal statement (Lean)

  39theorem row_vus_eq_geometry : V_us_pred = torsion_overlap - cabibbo_radiative_correction :=

proof body

One-line wrapper that applies vus_derived.

  40  vus_derived
  41

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.