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

cabibbo_correction_geometric

show as:
view Lean formalization →

The declaration equates the Cabibbo radiative correction coefficient of 3/2 to the matching value in the PMNS corrections module, with the factor arising from cubic ledger topology. Researchers deriving CKM parameters from geometric models would cite it to replace numerical fits with topological constraints. The proof is a one-line term wrapper that invokes symmetry on the established matching lemma.

claimThe Cabibbo radiative correction coefficient equals the PMNS correction coefficient, both fixed at $3/2$ by the requirement of cubic topology in the ledger structure.

background

The module derives CKM and PMNS mixing elements from the cubic ledger using edge-dual coupling, where generation overlaps are set by 8-tick window alignments. Topological ratios fix values such as $|V_{cb}| = 1/24$ from single-edge versus double-vertex coverage and enforce unitarity through 8-tick closure. Upstream results on primitive distinction reduce seven axioms to four structural conditions plus definitional facts, while simplicial ledger theorems confirm algebraic tautologies without new axioms.

proof idea

The proof is a term-mode one-line wrapper. It applies the simpa tactic to the symmetric form of the cabibbo_matches lemma already proved in the PMNSCorrections module, confirming identity between the radiative correction and the geometric definition.

why it matters in Recognition Science

This result identifies the 3/2 Cabibbo factor inside the Phase 7.2 geometric derivation, tying it to the same cubic symmetry that produces $|V_{cb}| = 1/24$ and the 8-tick octave closure. It advances the claim that mixing arises from ledger topology rather than free parameters, consistent with T7 and D = 3 landmarks. No downstream uses are recorded yet.

scope and limits

formal statement (Lean)

  43theorem cabibbo_correction_geometric :
  44    cabibbo_radiative_correction = PMNSCorrections.cabibbo_correction := by

proof body

Term-mode proof.

  45  -- PMNSCorrections proves it matches the MixingGeometry definition.
  46  simpa using (PMNSCorrections.cabibbo_matches).symm
  47
  48/-- **THEOREM: V_cb from Ledger Topology**
  49    The CKM element $|V_{cb}|$ is exactly $1/24$ derived from the cubic symmetry.
  50    - 12 edges in a cube.
  51    - Each edge has 2 vertices.
  52    - Total coverage space = 24 (vertex_edge_slots).
  53    - Edge-Dual Coupling: The second generation (s, c) occupies the faces, while the
  54      third generation (b, t) occupies the vertices. The transition $|V_{cb}|$
  55      represents the dual mapping from a face-center to a vertex via a single edge. -/

depends on (14)

Lean names referenced from this declaration's body.