module module high

`IndisputableMonolith.Physics.MixingGeometry`

The MixingGeometry module supplies cubic ledger geometry for deriving fermion mixing weights and ratios in Recognition Science. It establishes vertex-edge incidence counts and angle-specific weights used by CKM and PMNS derivations. Researchers formalizing mixing matrices from the 3-cube structure cite these primitives. Content consists of definitions and equalities that count incidences and extract dual ratios from the cubic lattice.

claimThe module defines the total vertex-edge incidence slots in the 3-cube $Q_3$ by $12$ edges each incident to $2$ vertices, together with the edge-dual ratio, fine-structure leakage, and solar/atmospheric weights derived from the same incidence structure.

background

This module sits inside the Recognition Science cubic ledger where spatial structure is the 3-cube $Q_3$. Upstream AlphaDerivation derives $4π$ from Gauss-Bonnet via vertex deficits of $Q_3$. Key definitions include vertex_edge_slots (total incidences), edge_dual_ratio, and radiative weights for solar and atmospheric angles that later enter the eight-tick octave closure.

proof idea

This is a definition module. vertex_edge_slots_eq_24 follows by direct counting: twelve edges each contribute two incidences. Remaining declarations (edge_dual_ratio, fine_structure_leakage, solar_weight, atmospheric_weight) are introduced as abbreviations or equalities extracted from the same 3-cube incidence graph without further tactics.

why it matters in Recognition Science

The module supplies the geometric primitives required by CKMGeometry (T11) and MixingDerivation (Phase 7.2) for CKM and PMNS matrix elements. It also feeds Hierarchy for generation unification and QuarkMasses for quarter-ladder mass steps. These definitions close the structural link between the cubic ledger and observable mixing parameters while supporting the alpha derivation.

scope and limits

Does not derive explicit numerical values for mixing angles.
Does not contain full radiative correction proofs.
Does not extend beyond the 3-cube incidence structure.
Does not incorporate experimental PDG fits or bounds.

used by (6)

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

IndisputableMonolith.Physics.CKMGeometry module_import
IndisputableMonolith.Physics.Hierarchy module_import
IndisputableMonolith.Physics.MixingDerivation module_import
IndisputableMonolith.Physics.ParticleSummary module_import
IndisputableMonolith.Physics.PMNSCorrections module_import
IndisputableMonolith.Physics.QuarkMasses module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (17)

def vertex_edge_slots L20
theorem vertex_edge_slots_eq_24 L22
def edge_dual_ratio L29
def fine_structure_leakage L34
def torsion_overlap L39
def solar_weight L42
def solar_radiative_correction L46
theorem solar_angle_forced L51
def atmospheric_weight L57
def atmospheric_radiative_correction L61
theorem atmospheric_angle_forced L66
def reactor_weight L72
def step_top_bottom L77
def step_bottom_charm L80
def step_charm_strange L83
def cabibbo_radiative_correction L87
theorem cabibbo_scaling_forced L92