angular_contribution_per_dim
plain-language theorem explainer
angular_contribution_per_dim supplies the per-dimension angular integral factor π that accumulates to π^5 over the five-dimensional ledger configuration space. A researcher deriving the curvature correction δ_κ = -103/(102π^5) inside the fine-structure formula would cite it to account for the half-sphere measures arising from antipodal, time-reversal, and sign symmetries. The definition is a direct assignment to Real.pi, with no further computation or lemma application required.
Claim. In the five-dimensional configuration space the angular integral over each dimension equals $π$, so that the total angular factor is $π^5$.
background
The module derives the π^5 factor in the curvature correction term of the fine-structure constant: α^{-1} = 4π·11 - f_gap - 103/(102π^5). The ledger state is described by a 5-dimensional phase space consisting of three spatial coordinates on the cubic lattice, one temporal coordinate from the 8-tick cycle, and one balance coordinate enforcing the conservation constraint σ. Each coordinate contributes an angular integral ∫_0^π dθ = π because of antipodal identification in space, time-reversal symmetry in the cycle, and the absolute-value convention on the balance normal.
proof idea
One-line definition that directly assigns the real number π, encoding the half-period angular measure in each of the five dimensions.
why it matters
This definition supplies the elementary building block for the total angular factor π^5 that appears in the denominator of the curvature correction inside the Recognition Science expression for α^{-1}. It rests on the forced values D = 3 (T8), the eight-tick temporal octave (T7), and the single balance dimension required by ledger conservation. The sibling declaration total_angular_factor is the immediate consumer that raises the per-dimension factor to the fifth power.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.