ConstraintK
plain-language theorem explainer
ConstraintK defines the (K) constraint as the requirement that the apsidal angle equals 2π for dimension D. Researchers assembling the dimensional rigidity argument in Recognition Science cite it when combining the (T), (K), and (S) conditions to force three spatial dimensions. The definition is a direct equating of the closed-form apsidal angle to 2π with no additional steps.
Claim. The (K) constraint holds for dimension $D$ when the apsidal angle satisfies $Δθ(D) = 2π$, where $Δθ(D) = 2π / √(4 - D)$ is the closed-form expression obtained after substituting the Green-kernel power law.
background
In the Draft_v1.tex formalization surface, the (K) constraint is one of three conditions whose conjunction forces D = 3. The apsidal angle is introduced via the upstream definition that sets Δθ(D) = 2π / √(4 - D) for integer D treated as a real parameter. This module mirrors paper theorem statements while recording external mathematics (such as Alexander duality) only as explicit hypothesis interfaces rather than new axioms.
proof idea
The definition is a direct one-line equating of the apsidal angle expression to 2π, serving as the arithmetic reduction of the paper-style (K) constraint.
why it matters
ConstraintK supplies the (K) constraint to dimensional_rigidity_main, which concludes D = 3 from the three constraints, and to no_higher_dimensional_alternative, which rules out D > 3. It fills the paper proposition on dimensional rigidity and connects to the Recognition framework landmark that forces D = 3 spatial dimensions (T8). The downstream corollaries quote the forward direction as proved while noting the converse depends on further geometric infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.