configSpaceDim
plain-language theorem explainer
configSpaceDim fixes the effective dimension of the Recognition ledger configuration space at 5 for curvature integration. Derivations of the fine structure constant correction term cite it to explain the origin of the π^5 volume factor. The definition is a direct constant assignment with no further computation.
Claim. The effective dimension of the configuration space for curvature integration in the Recognition ledger is $5$.
background
The Curvature Space Derivation module establishes that the configuration space for the Recognition ledger combines three spatial dimensions (forced by D=3), one temporal dimension from the 8-tick cycle, and one dual-balance dimension from the conservation constraint. This decomposition produces the total dimension 5, which supplies the π^5 factor when integrating the curvature mismatch between spherical and cubic geometries over phase space. The local theoretical setting is the fine structure constant formula α^{-1} = 4π·11 - f_gap - 103/(102π^5), where the correction δ_κ arises from integration over this 5-dimensional space.
proof idea
The definition is a direct constant assignment configSpaceDim := 5. Dependent results such as config_space_is_5D recover the equality by reflexivity after unfolding.
why it matters
This definition supplies the dimension count that justifies the π^5 in curvature_correction_derived and curvature_correction_eq_formula, which produce δ_κ = -103/(102π^5). It is used by config_space_complete, ConfigSpaceDecomposition, and curvature_tuple_uniqueness_bundle_vs_derived. The value ties directly to framework landmarks T8 (D=3 spatial), T7 (eight-tick temporal), and the conservation constraint, closing the explanation for why the denominator involves π^5 rather than other powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.