IndisputableMonolith.Foundation

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