module module high

`IndisputableMonolith.Constants.AlphaHigherOrder`

The AlphaHigherOrder module supplies the geometric primitives for Q₃, including its vertices, edges, faces, active and passive edge partitions, and wallpaper group pairings. Researchers refining higher-order corrections to the fine structure constant would cite these objects. The module is entirely definitional and builds directly on the base Constants import without any theorems or proofs.

claimThe module defines the vertex set $V(Q_3)$, edge set $E(Q_3)$, face set $F(Q_3)$ of the three-dimensional cube $Q_3$, the partitions into active_edges and passive_edges, and the bijections face_wallpaper_pairs between faces and wallpaper groups.

background

Recognition Science takes the fundamental time quantum τ₀ = 1 tick from the imported Constants module as its base unit. This module extends that foundation by introducing the Q₃ structures required for three spatial dimensions. The listed sibling definitions (Q3_vertices, Q3_edges, Q3_faces, active_edges, passive_edges, wallpaper_groups, face_wallpaper_pairs and their equality lemmas) encode the combinatorial data of the 3-cube together with its symmetry assignments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These Q₃ objects supply the geometric scaffolding needed for higher-order terms in the fine structure constant α. They prepare the structural data that will enter calculations inside the alpha inverse interval (137.030, 137.039). With zero current downstream uses, the module remains an open foundation awaiting attachment to parent constant theorems.

scope and limits

Does not compute or approximate any numerical value of α or α^{-1}.
Does not relate Q₃ structures to the phi-ladder or mass formulas.
Does not invoke the J-function, RCL, or any forcing-chain step.
Does not contain theorems, only raw definitions and equality statements.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (44)

def Q3_vertices L59
theorem Q3_vertices_eq L60
def Q3_edges L63
theorem Q3_edges_eq L64
def Q3_faces L67
theorem Q3_faces_eq L68
def active_edges L71
def passive_edges L74
theorem passive_edges_eq L75
def wallpaper_groups L78
def face_wallpaper_pairs L81
theorem face_wallpaper_pairs_eq L82
def curvature_numerator L85
theorem curvature_numerator_eq L86
def measure_dimension L89
theorem measure_dimension_eq L90
def alpha_seed L95
def f_gap L98
def delta_1 L102
theorem delta_1_structure L104
theorem delta_1_numerator L108
theorem delta_1_denominator_nat L109
theorem delta_1_power L110
theorem delta_1_neg L113
def n_fold_configs L126
theorem n_fold_configs_1 L128
theorem n_fold_configs_2 L129
def Q3_aut_order L132
def reduced_configs L135
theorem reduced_configs_2 L137
def half_period_dim L142
theorem half_period_dim_eq L143
def Z2_sectors L146
theorem Z2_sectors_eq L147
def VoxelSeamCorrection L153
def delta_n L157
def partial_alpha L161
def CODATA_alpha_inv L167
structure AlphaPrecisionHypothesis L170
def additive_residual L181
def exponential_residual L185
theorem exp_minus_add_pos L189
structure AlphaFrameworkCert L200
def alphaFramework L213