pith. sign in
module module high

IndisputableMonolith.Physics.MixingGeometry

show as:
view Lean formalization →

MixingGeometry defines vertex-edge incidence counts and dual ratios on the 3-cube that supply geometric inputs for mixing derivations. Researchers on CKM and PMNS matrices cite it to replace free parameters with ledger topology. The module consists entirely of definitions and direct equalities.

claimThe total vertex-edge incidence slots in the 3-cube equal 24. The edge-dual ratio, fine-structure leakage, solar weight, and atmospheric weight are defined from the same cubic structure.

background

The module sits inside the cubic ledger of Recognition Science, where D=3 follows from the eight-tick octave. Vertex_edge_slots counts the 24 incidences arising from 12 edges each meeting two vertices. Upstream AlphaDerivation supplies the 4π factor via Gauss-Bonnet on vertex deficits of Q₃. Sibling definitions introduce edge_dual_ratio, torsion_overlap, solar_weight, atmospheric_weight, and the forced angles that appear in later mixing work.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds CKMGeometry (T11), MixingDerivation (Phase 7.2), Hierarchy, PMNSCorrections, ParticleSummary, and QuarkMasses. It supplies the geometric primitives that convert cubic ledger structure into mixing-angle predictions, closing the step between T8 (D=3) and the CKM/PMNS hypotheses stated in the downstream modules.

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)