linking_forces_d3_cert
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.
papers checked against this theorem (showing 12 of 12)
-
TetraSphere adds O(3) invariance to point clouds with under 0.0002% extra parameters
"steerable 3D spherical neurons... B(S) = [ (R_O^T R_Ti R_O S)^T ]_{i=0..3} ... equivariant under 3D rotations: V_R B(S) X = B(S) R X"
-
Mañé value sets blow-up threshold for magnetic Hunter-Saxton system
"the magnetic system on S^3 is fully understood by [4]... Proposition 3.1. The Ma~n'e's critical value of the system is c(S^3, g, d alpha) = 1/2 ||alpha||^2_infty = 1/8"
-
Trunk forms one component in S^3 restricted flip graph
"For S^3, we define the trunk to be the set of triangulations reachable from ∂Δ^4 using 1–4, 2–3, and 3–2 moves, but no 4–1 moves."
-
Circle-RoPE creates cone geometry to remove cross-modal RoPE bias
"PTD = 0 is a sufficient condition to eliminate the geometric attention bias induced by RoPE... yielding a cone-like geometry where each text token is equidistant to all image tokens while preserving intra-image spatial structure"
-
Color routing builds 4D and 5D layer codes that saturate bounds
"the output code C is embedded in D dimensions with n(C)=O(w²q²)LD for D=4 and O(w⁶q⁴)LD for D=5"
-
Nearly Kähler manifolds obey Kähler Hodge rules in all dimensions
"We generalize to nearly Kähler manifolds of arbitrary dimensions most of the Hodge-theoretic results for nearly Kähler 6-manifolds"
-
Cusped hyperbolic 4-manifold built without spin structure
"the only unbounded, right-angled, hyperbolic 4-polytope of finite volume with a compact 2-face ... P4 has 22 facets and octahedral symmetry"
-
Brain Turns Complex Search into Fast Navigation via Topology
"Closure induces Euler-Poincaré balance. ... ∂² = 0 ... even-dimensional and odd-dimensional homology contribute with opposite sign"
-
Interleaving contractions and inclusions enriches graph topology features
"FB-persistence is strictly more expressive than forward and backward persistence combined... Hourglass persistence is more expressive than FB-persistence"
-
Punctured surface code turns many couplings into one logical signal
"B⊤w=0... simple closed dual 1-cochain... endpoint graph Γend is bipartite"
-
VLMs hide a 3D scene map that math extraction can shape
"the k-th principal component ... exactly recovers z(k+1) ... converges uniformly to ... Cartesian coordinates x, y, z"
-
Combinatorial test decides generic rigidity in any dimension
"Theorem 1. ... G is infinitesimally flexible in E^d if and only if there exists a balanced source-stream-sink orientation Γ on a subgraph H of G ..."