IndisputableMonolith.Foundation.PublicSpine

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Strength
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced
   3import IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator
   4import IndisputableMonolith.Foundation.AlexanderDuality
   5import IndisputableMonolith.Foundation.DimensionForcing
   6import IndisputableMonolith.Foundation.CircleWindingChain
   7import IndisputableMonolith.Foundation.MathlibCohomologyBridge
   8import IndisputableMonolith.Foundation.UnknotComplementRetract
   9import IndisputableMonolith.Foundation.LinkingVanishingLowDim
  10import IndisputableMonolith.Cost.FunctionalEquation
  11import IndisputableMonolith.Verification.T6T8SpineAudit
  12
  13/-!
  14# PublicSpine — dual forcing surface (δ stratification)
  15
  16This module is the **public dual** of `UnifiedForcingChain`. It does **not** delete
  17or replace UFC. The Boolean / certificate spine stays for loop compatibility and
  18pedagogy. This surface is the honest δ-stratified map:
  19
  20* δ-only tower: ℕ / ℤ / ℚ (`forced_tower_holds`); continuum cut is
  21  `classicalExtension` (panel K2: do not put ¬ℝ under `deltaOnly`)
  22* cost form vs unit calibration (purchases / gauges, not free THEOREMs)
  23* φ from the reciprocal involution (`ReciprocalGenerator`)
  24* H₁(S¹;ℤ) ≅ ℤ kept as THEOREM; the D=3 / 8-tick bridge target is **CLOSED**
  25  (campaign P-d3link, 2026-07-18): `AlexanderLinkingBridge` is fully inhabited
  26  in `Foundation.PublicSpineLinkingClosure` (0 sorry, axioms exactly
  27  `[propext, Classical.choice, Quot.sound]`, no appeal to
  28  `DimensionForcing.linking_requires_D3`, no arithmetic encoding). The pieces:
  29  `d3_detects` (unknot complement retract), `CubePeriodEight` (pigeonhole),
  30  vanishing at D=0,1, and `forces_D3` for D=2 and D≥4 via the excision spine
  31  and arc-complement acyclicity (Hatcher 2B.1, arc case). The content-typed
  32  binder below is unchanged (panel K1: kills encoding cheat); only its
  33  inhabitation status moved from OPEN to THEOREM.
  34
  35Contract (dual-surface rules):
  361. Papers / loops that mean "what is forced" should cite **this** module.
  372. UFC names remain valid as `CERTIFICATE` / floor witnesses, not as the
  38   architecture claim.
  393. No encoding predicates: T8/T7 require `AlexanderLinkingBridge`, never
  40   `SphereAdmitsCircleLinking` as currently defined.
  414. FOP / unique-cost paper is untouched; this is Lean-map honesty only.
  42
  43Plan: `δ/Delta_Spine_Retype_Map_20260708.html`.
  44-/
  45
  46namespace IndisputableMonolith
  47namespace Foundation
  48namespace PublicSpine
  49
  50open PrimitiveRecognitionCalculus
  51open PrimitiveRecognitionCalculus.Forced
  52open UniversalForcing.ReciprocalGenerator
  53open Cost.FunctionalEquation
  54open Verification.T6T8SpineAudit
  55open AlexanderDuality
  56open DimensionForcing
  57
  58/-- Strength-tagged claim: the public surface refuses untagged THEOREM badges. -/
  59structure Tagged (tag : StrengthTag) (P : Prop) : Prop where
  60  holds : P
  61
  62/-- **δ-only tower:** ℕ / ℤ / ℚ are physically real (choice-free certificates).
  63Panel K2: do NOT conjoin the classical `¬ℝ` half under `deltaOnly`. -/
  64def ForcedTower : Prop :=
  65  PhysicallyReal ℕ ∧ PhysicallyReal ℤ ∧ PhysicallyReal ℚ
  66
  67theorem forced_tower_holds : Tagged StrengthTag.deltaOnly ForcedTower where
  68  holds := forcedTower
  69
  70/-- Continuum cut: ℝ is not δ-forced. Classical uncountability lives here, so the
  71tag is `classicalExtension`, not `deltaOnly` (panel K2). -/
  72theorem continuum_is_purchase :
  73    Tagged StrengthTag.classicalExtension (¬ DeltaForced ℝ) where
  74  holds := not_deltaForced_real
  75
  76/-- Full demarcation package (tower + continuum cut). Classical tag: the ℝ half
  77uses uncountability. Prefer `forced_tower_holds` + `continuum_is_purchase` when
  78citing δ-only vs purchase separately. -/
  79def Floor_Demarcation : Prop :=
  80  PhysicallyReal ℕ ∧ PhysicallyReal ℤ ∧ PhysicallyReal ℚ ∧ ¬ PhysicallyReal ℝ
  81
  82theorem floor_demarcation_holds :
  83    Tagged StrengthTag.classicalExtension Floor_Demarcation where
  84  holds := demarcation
  85
  86/-- **Cost form vs selection.** The continuous uniqueness theorem selects `J`
  87under reciprocity, normalization, RCL, calibration, continuity, and the Aczél
  88package. Honest tag is at least `traceClosure` (continuum carrier) plus the
  89calibration gauge; never `deltaOnly`. -/
  90structure CostSelectionPackage : Prop where
  91  /-- J is unique among reciprocal continuous calibrated RCL costs. -/
  92  j_unique :
  93    ∀ (F : ℝ → ℝ) [AczelSmoothnessPackage],
  94      IsReciprocalCost F → IsNormalized F → SatisfiesCompositionLaw F →
  95      IsCalibrated F → ContinuousOn F (Set.Ioi 0) →
  96      ∀ {x : ℝ}, 0 < x → F x = Cost.Jcost x
  97
  98theorem cost_selection_holds : Tagged StrengthTag.traceClosure CostSelectionPackage where
  99  holds := {
 100    j_unique := fun F _ hRecip hNorm hComp hCalib hCont {_x} hx =>
 101      law_of_logic_forces_jcost F hRecip hNorm hComp hCalib hCont _ hx
 102  }
 103
 104/-- **φ from the reciprocal involution** (consumes reciprocity of J, not a
 105standalone quadratic). Tier: THEOREM (algebra of `ι` / `1+ι`). Hierarchy /
 106`MinimalHierarchy` routes remain FORCED-CONDITIONAL elsewhere. -/
 107structure PhiFromIota : Prop where
 108  cost_and_scale : ReciprocalGeneratorCert
 109
 110theorem phi_from_iota_holds :
 111    Tagged StrengthTag.traceClosure PhiFromIota where
 112  holds := { cost_and_scale := reciprocalGeneratorCert_holds }
 113
 114/-- **H₁(S¹;ℤ) ≅ ℤ** is proved; it is **not** yet a premise of a non-encoding
 115D=3 theorem (`T6T8SpineAudit`). -/
 116theorem circle_H1_holds :
 117    Tagged StrengthTag.classicalExtension MathlibCohomologyBridge.circleH1ZIsoInt where
 118  holds := CircleWindingChain.circleH1ZIsoInt_holds
 119
 120/-- Audit: linking predicate still unfolds to arithmetic encoding. -/
 121theorem linking_still_encoding (D : ℕ) :
 122    SphereAdmitsCircleLinking D ↔ (D : ℤ) - 2 = 1 :=
 123  t8_linking_predicate_unfolds_to_arithmetic D
 124
 125/-- **Content-typed linking object.** First singular homology (ℤ coefficients,
 126genuine Mathlib `singularHomologyFunctor`) of the complement of a continuous
 127map from S¹ into S^D. This is the object Alexander duality computes. Statements
 128about it cannot be discharged by arithmetic encodings: they require actual
 129homology computations of complements. -/
 130noncomputable def linkingComplementH1 (D : ℕ)
 131    (f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D)) : ModuleCat ℤ :=
 132  ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
 133    (ModuleCat.of ℤ ℤ)).obj
 134    (TopCat.of {x : TopCat.sphere.{0} D // x ∉ Set.range f})
 135
 136/-- **Non-encoding detector (panel K1, corrected 2026-07-08).** Some embedded
 137circle in S^D has homologically nontrivial complement: the real linking
 138obstruction, stated on the Mathlib object itself.
 139
 140History: the first binder used an abstract `detects : ℕ → Prop` field plus a
 141`not_encoding` name-firewall. That was broken both ways: the empty detector
 142`fun _ => False` inhabited it trivially (verified: the probe built), and by
 143`funext`+`propext` any honest detector is *equal* to the encoding predicate,
 144so the firewall excluded exactly the real bridge. Content-typing is the only
 145non-gameable form. -/
 146def DetectsNontrivialLinking (D : ℕ) : Prop :=
 147  ∃ f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D),
 148    Topology.IsEmbedding f ∧
 149      ¬ CategoryTheory.Limits.IsZero (linkingComplementH1 D f)
 150
 151/-- **The detection half is proved** (R2 of campaign P-d3link, 2026-07-17):
 152the flat unknot `z ↦ (z,0,0)` embeds S¹ in S³, and its complement retracts
 153onto the core circle `(0,0,w)`, so `H₁(S¹;ℤ) ≅ ℤ` (proved,
 154`circleH1ZIsoInt_holds`) is a retract of the complement's first homology,
 155which therefore is not zero. Real Mathlib singular homology throughout; no
 156arithmetic encoding anywhere in the proof
 157(`Foundation/UnknotComplementRetract.lean`). -/
 158theorem detectsNontrivialLinking_three : DetectsNontrivialLinking 3 :=
 159  ⟨UnknotComplementRetract.unknot, UnknotComplementRetract.unknot_isEmbedding,
 160    UnknotComplementRetract.unknotComplementH1_ne_zero
 161      CircleWindingChain.circleH1ZIsoInt_holds⟩
 162
 163/-- **The purchase binder, content-typed.** All three fields are PROVED
 164(campaign P-d3link, 2026-07-18): `d3_detects` by the unknot complement
 165retract, and `forces_D3` unconditionally by the circle-complement dichotomy
 166(excision spine + arc-complement acyclicity), for arbitrary (possibly wild)
 167topological embeddings. None of it can be produced from
 168`SphereAdmitsCircleLinking`'s arithmetic. The full inhabitation lives in
 169`Foundation.PublicSpineLinkingClosure`. -/
 170structure AlexanderLinkingBridge : Prop where
 171  /-- H₁(S¹;ℤ) ≅ ℤ is available to the bridge (already proved). -/
 172  h1 : MathlibCohomologyBridge.circleH1ZIsoInt
 173  /-- Some embedded circle in S³ has nontrivial complement homology.
 174  PROVED: `detectsNontrivialLinking_three` (unknot complement retract). -/
 175  d3_detects : DetectsNontrivialLinking 3
 176  /-- Only D = 3 admits the obstruction. PROVED:
 177  `PublicSpineLinkingClosure.forces_D3` (unconditional). -/
 178  forces_D3 : ∀ D, DetectsNontrivialLinking D → D = 3
 179
 180theorem D3_of_bridge (B : AlexanderLinkingBridge) :
 181    ∀ D, DetectsNontrivialLinking D → D = 3 :=
 182  B.forces_D3
 183
 184/-- **Target: D=3 from non-encoding linking — now THEOREM** (campaign
 185P-d3link, 2026-07-18; proof: `PublicSpineLinkingClosure.target_D3`). Kept as
 186a `def` (gate requirement): the statement stays content-typed so no free-Prop
 187cheat could ever have discharged it; it was closed by real topology. -/
 188def target_D3_from_nonencoding_linking : Prop :=
 189  Nonempty AlexanderLinkingBridge
 190
 191/-- **Vanishing at D = 0** (R3a of campaign P-d3link): every subspace of the
 192two-point S⁰ is totally disconnected, so complement H₁ vanishes for any map. -/
 193theorem not_detectsNontrivialLinking_zero : ¬ DetectsNontrivialLinking 0 :=
 194  LinkingVanishingLowDim.not_detects_zero
 195
 196/-- **Vanishing at D = 1** (R3a of campaign P-d3link): an embedded circle in
 197S¹ is surjective (stereographic projection + connectedness), so the complement
 198is empty and its H₁ vanishes. -/
 199theorem not_detectsNontrivialLinking_one : ¬ DetectsNontrivialLinking 1 :=
 200  LinkingVanishingLowDim.not_detects_one
 201
 202/-- Reduction lemma (historical shape of the campaign): given `forces_D3`,
 203the target follows because `h1` and `d3_detects` are proved. The premise is
 204now discharged unconditionally in `PublicSpineLinkingClosure`. -/
 205theorem bridge_of_forces_D3
 206    (h : ∀ D, DetectsNontrivialLinking D → D = 3) :
 207    target_D3_from_nonencoding_linking :=
 208  ⟨⟨CircleWindingChain.circleH1ZIsoInt_holds, detectsNontrivialLinking_three, h⟩⟩
 209
 210/-- Real (non-`rfl`) eight-tick consequent: any periodic walk covering all
 2112³ = 8 corners of the 3-cube has period at least 8. Stated this way because
 212the literal `eight_tick = 2 ^ 3` is `rfl`-true (`eight_tick := 8`), which made
 213the previous eight-tick target vacuous. -/
 214def CubePeriodEight : Prop :=
 215  ∀ (walk : ℕ → (Fin 3 → Bool)) (p : ℕ), 0 < p →
 216    (∀ n, walk (n + p) = walk n) →
 217    Function.Surjective walk → 8 ≤ p
 218
 219/-- **The eight-tick period bound holds** (R0 of campaign P-d3link,
 2202026-07-17). Periodicity confines the walk's range to its first `p` values,
 221so surjectivity onto the `2³ = 8` cube corners forces `8 ≤ p` by counting.
 222Honest pigeonhole content; nothing here touches the D=3 bridge. -/
 223theorem cubePeriodEight_holds : CubePeriodEight := by
 224  classical
 225  intro walk p hp hper hsurj
 226  have hshift : ∀ k n, walk (n + k * p) = walk n := by
 227    intro k
 228    induction k with
 229    | zero => intro n; simp
 230    | succ k ih =>
 231      intro n
 232      have hsplit : n + (k + 1) * p = (n + k * p) + p := by ring
 233      rw [hsplit, hper, ih]
 234  have hmod : ∀ n, walk n = walk (n % p) := by
 235    intro n
 236    have h := hshift (n / p) (n % p)
 237    rwa [Nat.mod_add_div'] at h
 238  let f : (Fin 3 → Bool) → Fin p := fun x =>
 239    ⟨(hsurj x).choose % p, Nat.mod_lt _ hp⟩
 240  have hf : ∀ x, walk ((f x : Fin p) : ℕ) = x := by
 241    intro x
 242    exact ((hmod (hsurj x).choose).symm.trans (hsurj x).choose_spec)
 243  have hinj : Function.Injective f := by
 244    intro x y hxy
 245    have hx := hf x
 246    rw [hxy, hf y] at hx
 247    exact hx.symm
 248  have hcard := Fintype.card_le_of_injective f hinj
 249  simpa using hcard
 250
 251/-- **Target: eight-tick downstream of a non-encoding D=3 — now THEOREM.**
 252Both conjuncts are proved: the bridge (`PublicSpineLinkingClosure.target_D3`)
 253and the period half (`cubePeriodEight_holds`). See
 254`Skeleton.guidepost_public_eight_tick` for the assembled proof. -/
 255def target_eight_tick_from_D3 : Prop :=
 256  target_D3_from_nonencoding_linking ∧ CubePeriodEight
 257
 258/-- The eight-tick target reduces to the D=3 bridge alone: the period half is
 259proved. -/
 260theorem target_eight_tick_of_bridge
 261    (h : target_D3_from_nonencoding_linking) : target_eight_tick_from_D3 :=
 262  ⟨h, cubePeriodEight_holds⟩
 263
 264/-- Dual-surface certificate: inhabited pieces of the public spine. -/
 265structure PublicSpineCert : Prop where
 266  forced_tower : Tagged StrengthTag.deltaOnly ForcedTower
 267  continuum_purchase : Tagged StrengthTag.classicalExtension (¬ DeltaForced ℝ)
 268  cost_selection : Tagged StrengthTag.traceClosure CostSelectionPackage
 269  phi_from_iota : Tagged StrengthTag.traceClosure PhiFromIota
 270  circle_H1 : Tagged StrengthTag.classicalExtension MathlibCohomologyBridge.circleH1ZIsoInt
 271  linking_encoding_named : ∀ D, SphereAdmitsCircleLinking D ↔ (D : ℤ) - 2 = 1
 272
 273theorem publicSpineCert_holds : PublicSpineCert where
 274  forced_tower := forced_tower_holds
 275  continuum_purchase := continuum_is_purchase
 276  cost_selection := cost_selection_holds
 277  phi_from_iota := phi_from_iota_holds
 278  circle_H1 := circle_H1_holds
 279  linking_encoding_named := linking_still_encoding
 280
 281/-! ## Channel-B citation surface (2026-07-08; retiered 2026-07-18)
 282
 283Downstream modules that previously bundled `UnifiedForcingChain.t0_holds`…`t8_holds`
 284as a closed architecture spine should cite these instead. Inhabited content is
 285`PublicSpineCert`. D=3 / eight-tick are now closed:
 286`PublicSpineLinkingClosure.target_D3` and
 287`Skeleton.guidepost_public_eight_tick`. -/
 288
 289/-- Preferred name for the inhabited public substrate (Channel B retarget). -/
 290abbrev SubstrateCert : Prop := PublicSpineCert
 291
 292theorem substrateCert_holds : SubstrateCert := publicSpineCert_holds
 293
 294/-- Disclosure: the D=3 / eight-tick public targets are exactly the content-typed
 295binders above (both now proved; see `PublicSpineLinkingClosure`). Citing this is
 296the honest replacement for `Nonempty T7_EightTick_Forced` /
 297`Nonempty T8_Dimension_Forced`. -/
 298structure DimensionEightTickOpen : Prop where
 299  d3_is_bridge :
 300    target_D3_from_nonencoding_linking = Nonempty AlexanderLinkingBridge
 301  eight_is_bridge_and_period :
 302    target_eight_tick_from_D3 =
 303      (target_D3_from_nonencoding_linking ∧ CubePeriodEight)
 304
 305theorem dimensionEightTickOpen_holds : DimensionEightTickOpen where
 306  d3_is_bridge := rfl
 307  eight_is_bridge_and_period := rfl
 308
 309end PublicSpine
 310end Foundation
 311end IndisputableMonolith
 312