is
plain-language theorem explainer
The binder uniqueness half holds once the arc-complement frontier is granted: linking vanishes in dimensions 0 and 1 outright, and in dimensions 2 and ≥4 by Mayer–Vietoris reduction. Anyone assembling the public spine to the high-dimensional linking bridge cites this. The statement is an assembly interface; the body is empty in the extract, so the content is the dimensional case split itself.
Claim. Conditional on the arc-complement frontier, the binder uniqueness half holds: linking vanishes unconditionally in dimensions $0$ and $1$, and in dimensions $2$ and $\ge 4$ by the Mayer–Vietoris reduction of high-dimensional linking vanishing. Instantiating the compact-support bisection over the banked Mayer–Vietoris layer closes the bridge with no residual hypothesis.
background
Module PublicSpineLinkingAssembly glues the public spine to the high-dimensional linking-vanishing package. The local goal is to discharge the uniqueness half of the binder once an arc-complement frontier hypothesis is in place, so the spine-to-linking bridge becomes unconditional after the remaining geometric lemmas are plugged in.
Low-dimensional vanishing (dimensions $0$ and $1$) is already settled by the low-dimensional linking package. Dimensions $2$ and $\ge 4$ are reduced, via a banked Mayer–Vietoris layer with compact-support bisection, to the high-dimensional vanishing theorems. Dimension $3$ is deliberately left to the arc-acyclicity forcing siblings in the same module.
Upstream imports are the public spine interface and the high-dimensional linking-vanishing development. The assembly does not re-prove those vanishing statements; it only records which dimensional cases they cover and under which frontier hypothesis the uniqueness half is available.
proof idea
No tactic body is present in the extract (n_proof_body_lines = 0). The declaration functions as a dimensional case-split interface: cite low-dimensional linking vanishing for $D\in{0,1}$; cite the Mayer–Vietoris reduction from the high-dimensional package for $D=2$ and $D\ge 4$; keep the arc-complement frontier as the sole residual hypothesis. Closing the bridge is then pure instantiation of those named results, not a new geometric argument.
why it matters
In the Recognition foundation stack this lemma is the uniqueness half of the binder that ties the public spine to linking vanishing. Together with the sibling arc-acyclicity lemmas (forces_D3_of_arcAcyclic, target_of_arcAcyclic) it isolates dimension $3$ as the remaining geometric case, consistent with the forcing-chain landmark that spatial dimension $D=3$ is forced (T8).
No downstream uses are recorded yet (used_by_count = 0), so the declaration is presently a spine-assembly leaf: it packages the conditional uniqueness claim for later bridge closure once compact-support bisection over the banked Mayer–Vietoris layer is fully instantiated. It does not itself force $D=3$; it only organizes the uniqueness half so that the $D=3$ forcing siblings can finish the job.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.