pith. sign in
module module high

IndisputableMonolith.Physics.MixingGeometry

show as:
view Lean formalization →

MixingGeometry supplies the 3-cube incidence counts and dual ratios that feed CKM and PMNS derivations. Physicists constructing mixing angles from the cubic ledger cite its vertex-edge slots and angle weights. The module consists entirely of definitions and equalities extracted from the 3-cube structure.

claimThe 3-cube $Q_3$ possesses 24 vertex-edge incidence slots. Edge dual ratios, fine-structure leakage, and sector weights (solar, atmospheric, reactor) are defined from these incidences.

background

Recognition Science places particle mixing on the cubic ledger $Q_3$. The upstream AlphaDerivation module states: 'This module provides a complete, constructive derivation of the fine-structure constant α⁻¹ from the geometry of the cubic ledger' and obtains 4π via Gauss-Bonnet on vertex deficits of $Q_3$. Constants supplies the base time quantum τ₀ = 1 tick. The present module introduces the incidence primitives used by all downstream mixing work.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions supply the geometric substrate for CKMGeometry (T11: CKM matrix elements from ledger geometry), MixingDerivation (Phase 7.2), PMNSCorrections (integer coefficients from 8-tick octave), Hierarchy (unified generation ladder), QuarkMasses (quarter-ladder steps), and ParticleSummary. The module therefore closes the geometric layer required by the mixing and mass derivations.

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)