module module high

`IndisputableMonolith.Foundation.GaugeFromCube`

GaugeFromCube supplies the combinatorial model of the D-cube whose vertices are maps from Fin D to {0,1}. It defines edge, face, and automorphism counts together with the signed-permutation action. Workers on the Yang-Mills mass gap cite the module when they need the discrete symmetry data that follows from D = 3. The module is a collection of definitions and direct cardinality statements.

claimThe principal objects are the vertex set $V_D = (D : ℕ) → (Fin D → {0,1})$, the edge and face cardinalities of the 3-cube, and the group of signed permutations acting on $V_D$.

background

The module follows DimensionForcing, which establishes D = 3, and imports ParticleGenerations and QuarkColors. It therefore works inside the forced three-dimensional setting where three fermion generations and three quark colors have already been derived. CubeVertex is introduced as the function type Fin D → {0,1} that labels the 2^D corners of the hypercube. Additional definitions record the number of edges, faces, and the order of the cube automorphism group generated by signed axis permutations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the cube vertex and symmetry data directly into the Yang-Mills Mass Gap construction. That parent theorem derives the mass gap from the J-cost functional alone; the discrete cube supplies the finite symmetry group whose representations are used to model the gauge degrees of freedom. The definitions therefore close the geometric step that links the forced D = 3 to the continuous gauge theory appearing in the mass-gap argument.

scope and limits

Does not derive any field equations or dynamics.
Does not identify specific Lie algebras or continuous gauge groups.
Does not treat the continuum limit of the cube lattice.
Does not address interactions with the J-cost functional itself.

used by (1)

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

IndisputableMonolith.Unification.YangMillsMassGap module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.QuarkColors module_import

declarations in this module (43)

def CubeVertex L93
theorem cube_vertex_count L101
theorem cube3_vertex_count L105
def cube_edge_count L109
theorem cube3_edge_count L112
def cube_face_count L117
theorem cube3_face_count L120
structure SignedPerm L131
theorem signed_perm_card L144
theorem cube_aut_order L153
def IsAxisPermutation L162
def axis_perm_count L166
theorem axis_perm_count_D3 L168
def IsSignFlip L173
def sign_flip_count L177
theorem sign_flip_count_D3 L179
def IsEvenSignFlip L187
def sign_parity L191
def even_sign_flip_count L195
theorem even_sign_flip_count_D3 L198
def parity_quotient_order L206
theorem three_layer_factorization L216
theorem sm_factorization L223
structure GaugeLayer L238
def color_layer L244
def weak_layer L249
def hypercharge_layer L254
theorem gauge_rank_match L262
theorem dimension_sum L275
theorem dimension_sum_triangular L283
theorem s3_is_weyl_of_su3 L298
theorem color_from_axis_permutations L304
theorem even_flips_give_weak_structure L318
theorem parity_gives_hypercharge L327
theorem unique_gauge_factorization L338
theorem no_alternative_321 L362
def sm_gauge_ranks L371
def cube_gauge_ranks L374
theorem cube_matches_sm L378
theorem total_gauge_dim L383
theorem gauge_order_product L388
theorem gauge_generation_unification L406
theorem gauge_group_certificate L432