config_space_complete
plain-language theorem explainer
The configuration space dimension of the Recognition ledger equals five, obtained by adding three spatial dimensions forced by linking, one temporal dimension from the eight-tick cycle, and one dual-balance dimension from conservation. Researchers deriving the curvature correction in the fine-structure constant would cite this decomposition to fix the π^5 factor. The proof is a direct unfolding of the dimension definitions followed by numerical decision.
Claim. The configuration space dimension of the Recognition ledger equals the sum of the three forced spatial dimensions, the forced temporal dimension from the eight-tick cycle, and the forced dual-balance dimension from conservation: $5 = 3 + 1 + 1$.
background
The module shows that the curvature correction δ_κ = -103/(102π^5) arises because the ledger phase space is five-dimensional. This space consists of three spatial dimensions (from D=3 forced by T9), one temporal dimension (from the eight-tick cycle evolution), and one dual-balance dimension (the codimension-one surface of the conservation constraint σ = 0). Each angular integration over [0, π] contributes a factor of π, producing the fifth power in the denominator of the curvature term.
proof idea
The proof is a one-line wrapper that unfolds configSpaceDim, spatial_dims_forced, temporal_dim_forced, and balance_dim_forced, then applies native_decide to verify the numerical equality.
why it matters
This result supplies the exact dimensional count required to derive the π^5 volume factor in the curvature correction that appears in the fine-structure constant formula α^{-1} = 4π·11 - f_gap - 103/(102π^5). It closes the accounting for the ledger configuration space by combining the forcings T9 (spatial), T6 (temporal), and T3 (balance) from the unified chain. The theorem therefore fixes a derived quantity rather than a free parameter in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.