IndisputableMonolith.Foundation.PublicSpineLinkingAssembly

   1/-
   2Conditional assembly of the Alexander linking bridge (campaign P-d3link).
   3
   4This leaf file glues the Mayer-Vietoris reduction of
   5`LinkingVanishingHighDim` to the binder `PublicSpine`, exhibiting the exact
   6remaining distance to the unconditional bridge:
   7
   8* `forces_D3_of_arcAcyclic`: granting the single frontier
   9  `ArcComplementsAcyclic D` (embedded arcs in `S^D` have `H₁`-acyclic
  10  complements — Hatcher 2B.1, arc case) for every `D ≥ 2`, `D ≠ 3`, the
  11  binder's uniqueness half `∀ D, DetectsNontrivialLinking D → D = 3` holds.
  12* `target_of_arcAcyclic`: under the same hypothesis, the campaign target
  13  `target_D3_from_nonencoding_linking` (a fully inhabited
  14  `AlexanderLinkingBridge`) holds, with no appeal to
  15  `DimensionForcing.linking_requires_D3` or any other axiom.
  16
  17The hypothesis is a parameter, not an axiom and not a sorry.  When the arc
  18lemma is proved (compact-support bisection over the banked Mayer-Vietoris
  19layer), instantiating these theorems closes the bridge unconditionally.
  20-/
  21import IndisputableMonolith.Foundation.PublicSpine
  22import IndisputableMonolith.Foundation.LinkingVanishingHighDim
  23
  24namespace IndisputableMonolith
  25namespace Foundation
  26namespace PublicSpineLinkingAssembly
  27
  28/-- The binder's uniqueness half, conditional on the arc-complement
  29frontier.  Dimensions `0`, `1` are unconditional (`LinkingVanishingLowDim`);
  30dimensions `2` and `≥ 4` are the Mayer-Vietoris reduction of
  31`LinkingVanishingHighDim`. -/
  32theorem forces_D3_of_arcAcyclic
  33    (harc : ∀ D, 2 ≤ D → D ≠ 3 →
  34      LinkingVanishingHighDim.ArcComplementsAcyclic D) :
  35    ∀ D, PublicSpine.DetectsNontrivialLinking D → D = 3 :=
  36  fun D hdet => LinkingVanishingHighDim.forces_D3_of_arcAcyclic harc D hdet
  37
  38/-- The campaign target, conditional on the arc-complement frontier: a
  39fully inhabited `AlexanderLinkingBridge`, bypassing the
  40`DimensionForcing.linking_requires_D3` axiom on the public spine. -/
  41theorem target_of_arcAcyclic
  42    (harc : ∀ D, 2 ≤ D → D ≠ 3 →
  43      LinkingVanishingHighDim.ArcComplementsAcyclic D) :
  44    PublicSpine.target_D3_from_nonencoding_linking :=
  45  PublicSpine.bridge_of_forces_D3 (forces_D3_of_arcAcyclic harc)
  46
  47end PublicSpineLinkingAssembly
  48end Foundation
  49end IndisputableMonolith
  50