module module high

`IndisputableMonolith.Foundation.GaugeFromCube`

GaugeFromCube defines the D-cube vertices as maps Fin D to {0,1} together with edge, face, and signed-permutation counts to supply discrete geometry for gauge groups. Researchers working on the Yang-Mills mass gap or discrete origins of color would cite it. The module consists entirely of definitions and cardinality statements with no proof obligations.

claimA vertex of the $D$-cube is a function $\{0,1\}^D$, i.e., an element of the set of maps from $\{1,\dots,D\}$ to $\{0,1\}$.

background

The module follows DimensionForcing, which proves D=3 is forced by the RS framework through topological, self-similar, and other arguments. It also imports ParticleGenerations (P-001: three fermion generations) and QuarkColors (P-007: N_c=3).

CubeVertex is introduced as the set of functions Fin D → {0,1}. Companion definitions give the cardinalities 2^D for vertices, D·2^{D-1} for edges, and the order of the hyperoctahedral group for signed permutations of the axes.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the cube geometry imported by YangMillsMassGap (QG-005), the module that resolves one of the seven Millennium problems from the J-cost functional alone. The vertex and symmetry counts connect the D=3 forcing and the three-color/three-generation results to the discrete substrate of non-Abelian gauge structure.

scope and limits

Does not derive an explicit gauge group from the cube symmetries.
Does not compute masses, couplings, or the J-cost on these objects.
Does not address non-cubic lattices or dimensions other than the forced D=3.
Does not contain any theorem linking the cube directly to the recognition functional.

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