config_space_is_5D
plain-language theorem explainer
The Recognition ledger configuration space has effective dimension five, combining three spatial dimensions forced by non-trivial curve linking, one temporal dimension from the eight-tick cycle, and one balance dimension from conservation. Derivations of the curvature correction term in α^{-1} cite this to fix the π^5 denominator in δ_κ = -103/(102π^5). The proof is a one-line reflexivity on the definition of configSpaceDim.
Claim. The effective dimension of the ledger configuration space for curvature integration equals five.
background
The module derives the curvature correction δ_κ = -103/(102π^5) by integrating the mismatch between spherical and cubic geometries over the ledger phase space. This space decomposes into three spatial dimensions (D=3, forced by linking topology), one temporal dimension (the eight-tick cycle), and one dual-balance dimension (the conserved quantity σ). Each angular contribution supplies a factor of π, producing the observed π^5. The upstream definition sets configSpaceDim : ℕ := 5 with an explicit decomposition note. Related structures include the Dimension record tracking length, time, and mass exponents.
proof idea
The proof is a term-mode reflexivity that matches configSpaceDim directly to the numeral 5 by appeal to its defining equation.
why it matters
This supplies the exponent five required by the downstream theorem curvature_tuple_uniqueness_bundle_vs_derived, which equates the curvature correction expression to its derived form precisely when the dimension is five. The result closes the account of why the fine structure constant involves π^5, consistent with the eight-tick octave and the forcing of D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.