pith. sign in
theorem

linking_forces_d3_cert

proved
show as:
module
IndisputableMonolith.Foundation.AlexanderDualityProof
domain
Foundation
line
84 · github
papers citing
12 papers (below)

plain-language theorem explainer

Certification that circle linking occurs precisely in three dimensions is delivered by constructing an instance of the LinkingForcesD3 structure. Researchers deriving spatial dimension from topological constraints in the Recognition Science forcing chain would cite this when closing the T8 step. The proof is a direct record construction that assigns the linking equality from circle_links_in_three and dispatches the exclusion of lower dimensions via arithmetic.

Claim. The linking dimension of a circle equals three: for a one-dimensional linker $p=1$ one has linking dimension $2p+1=3$, no nontrivial linking of such objects exists in ambient dimension $D≤2$, and linking holds exactly in $D=3$.

background

The module replaces three Alexander duality axioms used in T8 (D=3 forcing) with explicit calculations. The key definition is linking_dimension(p) := 2p+1, which gives the ambient dimension in which a p-dimensional object links nontrivially. Upstream, circle_links_in_three proves linking_dimension(1)=3 by norm_num, while the structure LinkingForcesD3 packages the smallest linker (the circle), the required equality, the prohibition on linking in D≤2, and the confirmation in D=3.

proof idea

The proof constructs the LinkingForcesD3 instance by setting linking_requires to circle_links_in_three. The no_linking_in_2D field is discharged by introducing D and the linking assumption, unfolding linking_dimension, and applying omega. The linking_in_3D field reuses circle_links_in_three directly.

why it matters

This supplies the concrete certificate for the linking constraint that forces D=3 in the T8 step of the unified forcing chain. It closes the structural requirement inside LinkingForcesD3, supporting the module's goal of replacing Alexander duality axioms with explicit results. The construction connects to the Recognition Science derivation of three spatial dimensions from the self-similar fixed point phi and the eight-tick octave.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.