module module moderate

`IndisputableMonolith.StandardModel.CKMExact`

Exact CKM structure from the 3-cube Gray code on the eight-tick clock: vertices, edges, and which axis flips at each step of 000→001→011→010→110→111→101→100. Quark-mixing workers cite it for discrete angle and phase bookkeeping tied to three generations. The module packages combinatorial counts and flip-axis lemmas rather than a single closed-form matrix theorem.

claimOn the unit 3-cube with Gray-code cycle $000\to001\to011\to010\to110\to111\to101\to100\to000$, record the flipped axis at step $k$, the vertex and edge sets, flip counts per axis, and the resulting Gray-code asymmetry used to pin exact CKM mixing data in the Recognition Science discrete clock.

background

Recognition Science runs physics on a discrete eight-tick octave (period $2^3$), with phases at multiples of $\pi/4$. The three spatial bits label the vertices of the unit 3-cube; a reflected binary (Gray) path visits each vertex once and returns, flipping exactly one coordinate per step.

Upstream, EightTick fixes that clock, ParticleGenerations forces exactly three fermion generations (P-001), and CKMMatrix targets the $3\times3$ Cabibbo-Kobayashi-Maskawa matrix from $\varphi$-angles: three mixing angles plus one CP phase. Constants supply the RS-native tick $\tau_0$.

This module makes the cube combinatorics explicit: $Q_3$ vertices and edges, the axis flipped at step $k$ along the standard Gray cycle, per-axis flip counts, and symmetry statements (e.g. axes 1 and 2 symmetric) that feed exact CKM bookkeeping rather than numerical fits.

proof idea

Definition-heavy module with short combinatorial lemmas. Vertices and edges of the 3-cube are enumerated; grayFlipAxis (and the flip lemmas for axes 0,1,2) read off which bit changes at each step of the fixed Gray cycle 000→…→000. Flip counts and total flips are pure counting; asymmetry and axis-1/2 symmetry are direct comparisons of those counts. No analytic continuum argument: finite case analysis on eight steps and three axes.

why it matters in Recognition Science

Feeds the Standard Model side of the unified forcing story: UnifiedForcingChain imports this module while claiming T0–T8 (including the eight-tick octave T7 and $D=3$ as T8) as inevitabilities from the cost foundation and Recognition Composition Law. Exact Gray-code flip structure supplies the discrete skeleton for SM-012 CKM elements from $\varphi$-angles, aligning three generations with the three cube axes and the CP-sensitive asymmetry with the oriented eight-tick loop. Without these counts, CKM remains angle phenomenology; with them, mixing data sit on the same $2^3$ clock as the rest of the forcing chain.

scope and limits

Does not derive numerical CKM entries or prove unitarity of a concrete matrix.
Does not replace SM-012 φ-angle formulas; only supplies Gray-code combinatorics.
Does not address PMNS lepton mixing or charged-lepton masses.
Does not prove three generations here; that is assumed from ParticleGenerations.
Does not treat continuum CKM parametrizations beyond the discrete 3-cube path.

used by (1)

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

IndisputableMonolith.Foundation.UnifiedForcingChain module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.EightTick module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.StandardModel.CKMMatrix module_import

declarations in this module (56)

inductive Q3Vertex L45
inductive Q3Edge L50
theorem q3_vertex_count L56
theorem q3_edge_count L57
def grayFlipAxis L62
def flipCount L72
theorem flip_axis0 L77
theorem flip_axis1 L78
theorem flip_axis2 L79
theorem total_flips L81
theorem gray_asymmetry L85
theorem gray_axis12_symmetric L88
def tau L93
def deltaTau12 L98
def deltaTau23 L99
theorem deltaTau12_eq L101
theorem deltaTau23_eq L102
theorem forty_four_connection L104
def A_structural L109
theorem A_structural_eq L111
theorem A_structural_pos L114
def faceFlux L125
theorem faceFlux_12 L129
theorem faceFlux_23 L133
theorem faceFlux_13 L137
def berryCorrection L144
theorem berry_correction_eq L148
theorem berry_correction_pos L151
theorem berry_sq_eq L154
def A_corrected L160
theorem A_corrected_exact L163
theorem A_corrected_pos L167
theorem A_corrected_tight L172
theorem A_in_pdg_1sigma L176
theorem A_distance_from_pdg L180
theorem gap_nearly_closed L185
def lambda_RS L191
theorem lambda_RS_pos L193
theorem lambda_RS_interval L195
def lambda_PDG L221
theorem lambda_PDG_in_window L223
theorem lambda_structural_discrepancy L228
theorem lambda_correction_target L246
def jarlskog_rs L252
theorem jarlskog_pos L254
theorem forty_four_governs_three_constants L262
theorem nine_from_color_squared L269
theorem eleven_is_torsion_gap L272
theorem A_from_color_and_torsion L275
theorem four_from_chirality L281
theorem eleven_from_torsion L284
theorem six_from_torsion L287
theorem three_halves_from_asymmetry L291
theorem nine_elevenths_forced L295
structure CKMExactCert L301
def ckmExactCert L316