module module moderate

`IndisputableMonolith.Constants.AlphaHigherOrder`

The module AlphaHigherOrder defines the vertices, edges, faces and wallpaper pairings of the graph Q₃ together with active and passive edge partitions. Researchers deriving higher-order corrections to the fine-structure constant in Recognition Science would reference these objects. The module is purely definitional; it contains no theorems or proofs.

claimThe module supplies the vertex set $V(Q_3)$, edge set $E(Q_3)$, face set $F(Q_3)$, active-edge and passive-edge subsets, and the set of face-wallpaper pairs for the 3-cube graph $Q_3$.

background

The module imports the base Recognition Science constants, whose sole documented object is the fundamental time quantum τ₀ = 1 tick. It introduces a collection of graph-theoretic definitions (Q3_vertices, Q3_edges, wallpaper_groups, face_wallpaper_pairs) that appear to supply combinatorial scaffolding for higher-order terms in α. No further theoretical setting is stated in the supplied module documentation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the graph Q₃ and its wallpaper structure that later constant derivations are expected to use when refining the alpha band (137.030, 137.039). No parent theorems are listed among the used_by edges.

scope and limits

Does not prove any equality or incidence property of the listed objects.
Does not relate Q₃ to the phi-ladder or to the eight-tick octave.
Does not compute or bound any numerical value of α.
Does not import or reference the Recognition Composition Law.

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