linking_still_encoding
plain-language theorem explainer
Audit theorem: the predicate that S^D admits nontrivial circle linking is definitionally equivalent to the arithmetic identity D−2=1. PublicSpine certificate authors cite it to flag that SphereAdmitsCircleLinking remains an encoding, not a homology computation. Proof is a one-line application of the dedicated unfold lemma.
Claim. For every natural number $D$, the $D$-sphere admits nontrivial linking of disjoint embedded circles if and only if $(D:\mathbb{Z})-2=1$.
background
PublicSpine is the public dual of UnifiedForcingChain: a δ-stratified forcing surface that keeps Boolean certificates for pedagogy while refusing encoding cheats on the T7/T8 bridge. Contract rule 3 forbids citing the circle-linking predicate as the architecture claim for D=3; that role belongs to the content-typed Alexander linking bridge (closed elsewhere).
The predicate in question is defined, via Alexander duality (Hatcher 3.44), as nontriviality of the reduced cohomology of S¹ in degree D−2: linking of circles in S^D is nontrivial iff H̃₁(S^D ∖ S¹) ≠ 0, which duality identifies with H̃^{D−2}(S¹). For the circle, that group is nontrivial only in degree 1, so the predicate collapses to D−2=1.
The companion content-typed object (first singular homology of the complement of a continuous S¹→S^D map) is deliberately separate: statements about it require actual homology of complements and cannot be discharged by arithmetic encodings.
proof idea
One-line term wrapper. Applies t8_linking_predicate_unfolds_to_arithmetic at the given D, which expands the definition of the linking predicate (reduced-cohomology nontriviality at degree D−2) into the integer equation (D:ℤ)−2=1 and closes both directions of the biconditional.
why it matters
Panel K1 audit inside PublicSpine: it records, as a proved fact rather than a comment, that the named linking predicate is still an arithmetic encoding of D=3. That honesty marker is what lets the dual surface keep the binder while routing the real T8 claim through AlexanderLinkingBridge (unknot-complement retract, CubePeriodEight, low-D vanishing, excision spine), not through this predicate.
Feeds publicSpineCert_holds, the aggregate certificate for the public dual spine (forced tower, continuum purchase, cost selection, φ-from-ι, circle H₁). Framework landmark: T8 forces D=3 spatial dimensions; the eight-tick octave (T7) and the closed D=3 linking bridge sit beside this audit, not inside it. Papers that mean "what is forced" should cite PublicSpine, and this lemma is the explicit non-claim that keeps the encoding out of that citation path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.