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

row_V_us

show as:
view Lean formalization →

The theorem certifies that the Recognition Science geometric prediction for the CKM element V_us lies inside the one-sigma experimental band. A physicist constructing CKM fits or testing mixing-angle derivations from the golden ratio would invoke this check. The entire proof consists of a direct reference to the matching result already proved in the geometry submodule.

claimThe inequality holds: $|V_{us}^{pred} - 0.22500| < 0.00067$, where $V_{us}^{pred} = φ^{-3} - (3/2)α$.

background

The CKMElementScoreCard module collects row theorems that verify the three leading CKM magnitudes against PDG data. V_us_pred is defined in the imported CKMGeometry module as the difference between the torsion overlap and the Cabibbo radiative correction, which simplifies to φ^{-3} - (3/2)α. The constants V_us_exp = 0.22500 and V_us_err = 0.00067 are hard-coded numerical values.

proof idea

This is a one-line wrapper that applies the theorem V_us_match from CKMGeometry. The proof term is exactly the identifier V_us_match, which discharges the goal without further reduction.

why it matters in Recognition Science

The result populates the vus component of the certificate produced by ckmElementScoreCardCert_holds. It thereby contributes to the partial theorem status for the CKM predictions listed in the module documentation. The construction relies on the Recognition Science constants phi and alpha lying in their certified intervals, consistent with the eight-tick octave and D=3 spatial dimensions of the underlying forcing chain. The module notes that Wolfenstein packings remain separate.

scope and limits

formal statement (Lean)

  33theorem row_V_us : abs (V_us_pred - V_us_exp) < V_us_err := V_us_match

proof body

  34

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.