IndisputableMonolith.Foundation.PublicSpineLinkingClosure

   1/-
   2UNCONDITIONAL closure of the Alexander linking bridge (campaign P-d3link).
   3
   4`ArcComplementAcyclic.arcComplementsAcyclic` discharges the last remaining
   5hypothesis parameter of the campaign (embedded arcs in `S^D` have
   6`H₁`-acyclic complements, every `D`; Hatcher 2B.1, arc case, proved by
   7compact-support bisection over the banked Mayer-Vietoris layer).  This leaf
   8file instantiates the conditional assembly with it:
   9
  10* `forces_D3`: the binder's uniqueness half,
  11  `∀ D, DetectsNontrivialLinking D → D = 3`, unconditionally.
  12* `target_D3`: the campaign target `target_D3_from_nonencoding_linking`
  13  (a fully inhabited `AlexanderLinkingBridge`), unconditionally, with no
  14  appeal to `DimensionForcing.linking_requires_D3` or any other axiom
  15  beyond the three standard Lean foundations.
  16-/
  17import IndisputableMonolith.Foundation.ArcComplementAcyclic
  18import IndisputableMonolith.Foundation.PublicSpineLinkingAssembly
  19
  20namespace IndisputableMonolith
  21namespace Foundation
  22namespace PublicSpineLinkingClosure
  23
  24/-- **Unconditional**: nontrivial linking detection forces dimension `3`.
  25Dimensions `0`, `1` are `LinkingVanishingLowDim`; dimensions `2` and `≥ 4`
  26are the Mayer-Vietoris reduction of `LinkingVanishingHighDim` instantiated
  27with the arc-complement acyclicity theorem. -/
  28theorem forces_D3 :
  29    ∀ D, PublicSpine.DetectsNontrivialLinking D → D = 3 :=
  30  PublicSpineLinkingAssembly.forces_D3_of_arcAcyclic
  31    (fun D _ _ => ArcComplementAcyclic.arcComplementsAcyclic D)
  32
  33/-- **Unconditional campaign target**: a fully inhabited
  34`AlexanderLinkingBridge`, bypassing the `DimensionForcing.linking_requires_D3`
  35axiom on the public spine. -/
  36theorem target_D3 : PublicSpine.target_D3_from_nonencoding_linking :=
  37  PublicSpineLinkingAssembly.target_of_arcAcyclic
  38    (fun D _ _ => ArcComplementAcyclic.arcComplementsAcyclic D)
  39
  40end PublicSpineLinkingClosure
  41end Foundation
  42end IndisputableMonolith
  43