Pith. sign in
module module high

IndisputableMonolith.Physics.MixingGeometry

show as:
view Lean formalization →

MixingGeometry supplies the cubic ledger primitives for fermion mixing derivations, defining 24 vertex-edge incidence slots in the 3-cube along with dual ratios and leakage terms. CKMGeometry, MixingDerivation, and PMNSCorrections cite it to ground mixing angles in Recognition Science geometry. The module consists of definitions and equalities that follow directly from the 3-cube topology and the vertex-deficit structure imported from AlphaDerivation.

claimThe total number of vertex-edge incidence slots in the 3-cube $Q_3$ equals 24, since each of the 12 edges connects two vertices. Additional objects include the edge-dual ratio, fine-structure leakage, torsion overlap, and forced weights for solar, atmospheric, and reactor angles.

background

The module sits inside the Recognition Science cubic ledger $Q_3$, whose vertex deficits yield $4\pi$ via Gauss-Bonnet as shown in AlphaDerivation. Constants supplies the base time quantum $\tau_0 = 1$ tick. The module introduces vertex_edge_slots (total incidences), edge_dual_ratio, fine_structure_leakage, torsion_overlap, and the solar/atmospheric/reactor weight and angle terms that appear in downstream mixing calculations.

These definitions translate the 3-cube topology into the geometric quantities needed for generation coupling. AlphaDerivation already extracts $\alpha^{-1}$ from the same ledger; MixingGeometry extends that ledger geometry to the mixing sector.

proof idea

This is a definition module, no proofs. It consists of direct definitions of incidence counts and ratios together with the equality vertex_edge_slots_eq_24 that follows immediately from the 3-cube edge count.

why it matters in Recognition Science

The module supplies the geometric layer required by T11 (CKMGeometry) and Phase 7.2 (MixingDerivation) for deriving CKM and PMNS elements from ledger structure. It is imported by Hierarchy for ladder positions, by PMNSCorrections for the integer coefficients in angle predictions, and by QuarkMasses for the quarter-ladder hypothesis. It therefore bridges the cubic ledger of AlphaDerivation to the mixing and mass sectors of the Recognition framework.

scope and limits

used by (6)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)