apsidalAngle
plain-language theorem explainer
The apsidalAngle definition supplies the closed-form expression Δθ(D) = 2π / √(4 - D) that appears after Green-kernel substitution in the Draft_v1.tex orbital analysis. Orbital mechanicians or Recognition Science modelers cite it when reducing the Bertrand problem to a dimension-selection condition. The definition is a direct one-line substitution of the power-law exponent into the classical apsidal-angle formula.
Claim. $Δθ(D) = 2π / √(4 - D)$ for natural number $D$, with $D$ cast to a real parameter in the denominator.
background
This definition sits in the Papers.DraftV1 module, whose module doc states it mirrors theorem statements from Draft_v1.tex and supplies explicit Lean surfaces for paper claims that rely on external mathematics such as Alexander duality. The formula substitutes the Green-kernel power law into the classical apsidal-angle expression. Upstream dependencies include the J-cost structure from PhiForcingDerived.of, the active edge count A from IntegrationGap.A, and the nuclear-density tiers from NucleosynthesisTiers.of, all of which calibrate the exponent that produces the 4 - D denominator.
proof idea
The definition is a direct one-line expression that substitutes the dimension parameter D into the closed-form apsidal angle obtained from the Green-kernel power-law substitution.
why it matters
This definition supplies the algebraic step required by the downstream kepler_selection_principle theorem, which proves Δθ = 2π if and only if D = 3, and by ConstraintK, which reduces the paper's (K) constraint to the same equality. It thereby closes the dimension-selection argument that links the eight-tick octave and the forced D = 3 spatial dimensions to observed Keplerian orbits. The module doc notes that such surfaces keep the certified claims honest by exposing any external hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.