IndisputableMonolith.Foundation

   1import IndisputableMonolith.Foundation.NothingToDistinction
   2import IndisputableMonolith.Foundation.TMinus1ToT8Bridge
   3import IndisputableMonolith.Foundation.LinkingNecessity
   4import IndisputableMonolith.Foundation.LinkingFromHierarchy
   5import IndisputableMonolith.Foundation.RecognitionToLinkingSeam
   6import IndisputableMonolith.Foundation.RecognitionLinkingPositiveID
   7import IndisputableMonolith.Foundation.RecognitionProducedEmbedding
   8import IndisputableMonolith.Foundation.LinkingNumbers
   9
  10/-!
  11# Shape of Logic Core Foundation
  12
  13This public aggregator is intentionally narrow.  It exposes the T-2 through T8
  14core theory, the Mathlib circle-H1 T8 closure, and the Recognition-to-detector
  15seam (`LinkingNecessity`, `RecognitionToLinkingSeam`,
  16`RecognitionProducedEmbedding`). It does not re-export later physics or
  17private application layers.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Foundation
  22
  23open NothingToDistinction
  24open TMinus1ToT8Bridge
  25
  26/-! ## Public Core Exports -/
  27
  28/-- T-2 to T-1: the Lean encoding of absolute nothing forces distinction. -/
  29abbrev tminus2_to_tminus1_certificate :=
  30  NothingToDistinction.nothingToDistinctionCert
  31
  32/-- Public T-2 through T8 certificate. -/
  33abbrev complete_tminus2_to_t8 :=
  34  TMinus1ToT8Bridge.complete_forcing_chain_tminus2_to_t8
  35
  36/-! The carrier-threaded T0 through T8 spine from one object-level distinction. -/
  37
  38/-- T8's Mathlib circle-H1 nonvanishing replacement is closed unconditionally. -/
  39theorem circle_h1_nonzero : MathlibCohomologyBridge.circleH1ZNonzero :=
  40  TMinus1ToT8Bridge.complete_forcing_chain_tminus2_to_t8.{0,0,0,0,0,0,0}.circle_h1_nonzero
  41
  42/-- The stronger `H_1(S^1; Z) ≅ Z` target is also closed unconditionally. -/
  43theorem circle_h1_iso_int : MathlibCohomologyBridge.circleH1ZIsoInt :=
  44  TMinus1ToT8Bridge.complete_forcing_chain_tminus2_to_t8.{0,0,0,0,0,0,0}.circle_h1_iso_int
  45
  46end Foundation
  47end IndisputableMonolith
  48