module module moderate

`IndisputableMonolith.Constants.AlphaHigherOrder`

Defines combinatorial data on the 3-cube Q₃: vertices, edges, faces, active versus passive edges, wallpaper groups, and face-wallpaper pairs. Constants work on higher-order fine-structure corrections cites these counts and equalities. The module is definitional, with short equality lemmas pinning the cardinalities.

claimCombinatorial data on the 3-cube $Q_3$: vertex, edge, and face sets; partitions into active and passive edges; wallpaper groups and face-wallpaper pairs, as input to higher-order corrections of the fine-structure constant $\alpha$.

background

In Recognition Science the spatial dimension $D=3$ and the eight-tick octave (period $2^3$) force the 3-cube $Q_3$ as the natural discrete geometry for one recognition cycle. Its $8$ vertices, $12$ edges, and $6$ faces supply the counting data that enter higher-order corrections to $\alpha^{-1}$ (the RS band $(137.030, 137.039)$).

The parent Constants module supplies the RS-native time quantum $\tau_0=1$ tick and the base constants. This file layers the $Q_3$ combinatorics: named sets for vertices, edges, faces; a split of edges into active and passive; wallpaper groups; and pairings of faces with wallpaper data. Equality lemmas record the expected cardinalities so downstream alpha expansions can quote them by name.

proof idea

Definition module. Each object is introduced as a concrete finite set or natural-number count; companion _eq lemmas are one-line cardinality or set-equality checks against the standard $Q_3$ numbers (8 vertices, 12 edges, 6 faces, and the derived active/passive and wallpaper counts). No deep proof content.

why it matters in Recognition Science

Higher-order $\alpha$ work needs a fixed, named source for $Q_3$ incidence data rather than ad-hoc numerals. The module sits in the Constants domain beside the base RS units ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) and feeds any expansion that weights edges, faces, or wallpaper symmetries on the eight-tick cube. No downstream theorems are wired yet in the graph; the intended consumers are alpha-correction assemblies that quote these counts. Ties directly to forcing landmarks T7 (eight-tick octave) and T8 ($D=3$).

scope and limits

Does not compute or bound the numerical value of $\alpha$ or $\alpha^{-1}$.
Does not derive $Q_3$ from the forcing chain; it assumes the cube geometry.
Does not prove completeness of the active/passive or wallpaper partitions beyond stated equalities.
Does not connect these counts to mass-ladder or Berry-threshold formulae.

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