canonicalDecomposition
plain-language theorem explainer
The canonical decomposition specifies the five-dimensional configuration space that produces the π^5 factor in the curvature correction to the fine-structure constant. Researchers deriving the explicit form of α^{-1} cite it to justify the denominator 102π^5 rather than a different power. The definition supplies the default structure instance whose dimension sum is settled by native decision.
Claim. The canonical decomposition is the structure with spatial dimension 3, temporal dimension 1 from the eight-tick cycle, and balance dimension 1 from the conservation constraint, satisfying $3 + 1 + 1 = 5$.
background
The module derives the curvature correction δ_κ = -103/(102π^5) by integrating the mismatch between spherical and cubic geometries over the ledger phase space. That space is five-dimensional: three spatial coordinates on the cubic lattice, one temporal coordinate from the eight-tick cycle, and one balance coordinate enforcing the conserved quantity σ. The structure ConfigSpaceDecomposition records these counts together with the equality to the total configuration-space dimension.
proof idea
The definition is a one-line wrapper that instantiates the ConfigSpaceDecomposition structure with the fixed values spatial_dims=3, temporal_dim=1, balance_dim=1 and the equality proved by native_decide.
why it matters
This definition supplies the dimension counts required by the curvature-space derivation to explain the π^5 in the fine-structure formula. It rests on the forced D=3 from the unified forcing chain and the eight-tick temporal structure. No downstream uses are recorded, so the declaration functions as a module-level constant that closes the accounting for the five-dimensional integration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.