IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CubicalChainComplex

   1/-
   2  PrimitiveRecognitionCalculus/CubicalChainComplex.lean
   3
   4  A stronger multi-distinction geometry packaging.
   5
   6  `MultiDistinctionGeometry.lean` proves the local 2-face cancellation used by
   7  cubical homology. This module packages the same content as a finite chain
   8  complex interface: a boundary pair is a pair of maps whose composite vanishes.
   9  This is intentionally lightweight, but it gives the internal paper a stable
  10  "chain complex" theorem without overclaiming a full homology library.
  11
  12  No project-local axioms. No sorry.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21namespace CubicalChainComplex
  22
  23/-- A two-step chain complex over types `C₂`, `C₁`, `C₀`: boundary after boundary
  24is zero. -/
  25structure BoundaryPair (C₂ C₁ C₀ : Type*) [Zero C₀] where
  26  d₂ : C₂ → C₁
  27  d₁ : C₁ → C₀
  28  square_zero : ∀ c : C₂, d₁ (d₂ c) = 0
  29
  30/-- The explicit Delta square as a two-step chain complex. -/
  31def squareBoundaryPair : BoundaryPair ℤ MultiDistinctionGeometry.C1 MultiDistinctionGeometry.C0 where
  32  d₂ := MultiDistinctionGeometry.d2
  33  d₁ := MultiDistinctionGeometry.d1
  34  square_zero := by
  35    intro c
  36    exact MultiDistinctionGeometry.boundary_squared_zero c
  37
  38/-- Any ambient 2-face in an `n`-channel cube has square-zero boundary. -/
  39theorem ambient_two_face_square_zero {n : ℕ}
  40    (base : MultiDistinctionGeometry.Config n) (i j : Fin n) (c : ℤ) :
  41    MultiDistinctionGeometry.faceBoundaryBoundary base i j c = fun _ => 0 :=
  42  MultiDistinctionGeometry.face_boundary_squared_zero_general base i j c
  43
  44/-- **Cubical chain packaging headline.** Delta's multi-distinction geometry has
  45a concrete chain-complex interface on the square and square-zero boundary on
  46every ambient 2-face. The remaining stronger target is the full all-dimensions
  47homology API, not the local `∂²=0` law. -/
  48theorem cubical_chain_complex_headline :
  49    (∀ c : ℤ, squareBoundaryPair.d₁ (squareBoundaryPair.d₂ c) = 0)
  50      ∧ (∀ (n : ℕ) (base : MultiDistinctionGeometry.Config n) (i j : Fin n) (c : ℤ),
  51          MultiDistinctionGeometry.faceBoundaryBoundary base i j c = fun _ => 0) :=
  52  ⟨squareBoundaryPair.square_zero, fun _ base i j c => ambient_two_face_square_zero base i j c⟩
  53
  54/-- A finite 2-face certificate inside an `n`-channel distinction cube. -/
  55structure TwoFaceCert (n : ℕ) where
  56  base : MultiDistinctionGeometry.Config n
  57  i : Fin n
  58  j : Fin n
  59  coeff : ℤ
  60
  61/-- The boundary-of-boundary chain carried by a two-face certificate. -/
  62def TwoFaceCert.boundaryBoundary {n : ℕ} (F : TwoFaceCert n) :
  63    MultiDistinctionGeometry.Config n → ℤ :=
  64  MultiDistinctionGeometry.faceBoundaryBoundary F.base F.i F.j F.coeff
  65
  66/-- Every finite 2-face certificate has zero boundary-of-boundary. -/
  67theorem twoFaceCert_boundary_squared_zero {n : ℕ} (F : TwoFaceCert n) :
  68    F.boundaryBoundary = fun _ => 0 :=
  69  ambient_two_face_square_zero F.base F.i F.j F.coeff
  70
  71/-- A finite list of two-face certificates has zero total boundary-of-boundary.
  72This is the additive finite-certificate version of local cubical `∂²=0`. -/
  73theorem twoFaceCert_list_boundary_squared_zero {n : ℕ} (faces : List (TwoFaceCert n)) :
  74    (fun w : MultiDistinctionGeometry.Config n =>
  75      faces.foldl (fun acc F => acc + F.boundaryBoundary w) 0) = fun _ => 0 := by
  76  induction faces with
  77  | nil =>
  78      funext w
  79      simp
  80  | cons F rest ih =>
  81      funext w
  82      have hF := congrFun (twoFaceCert_boundary_squared_zero F) w
  83      have hrest := congrFun ih w
  84      simp [List.foldl_cons, hF, hrest]
  85
  86/-- **Finite cubical certificate headline.** The local square-zero law is stable
  87under finite collections of certified 2-faces: every finite 2-face ledger has
  88zero total boundary-of-boundary. This is the all-finite-2-face strengthening
  89available from the current definitions without introducing a full homology API. -/
  90theorem finite_two_face_ledger_square_zero :
  91    ∀ (n : ℕ) (faces : List (TwoFaceCert n)),
  92      (fun w : MultiDistinctionGeometry.Config n =>
  93        faces.foldl (fun acc F => acc + F.boundaryBoundary w) 0) = fun _ => 0 :=
  94  fun n faces => twoFaceCert_list_boundary_squared_zero (n := n) faces
  95
  96end CubicalChainComplex
  97end PrimitiveRecognitionCalculus
  98end Foundation
  99end IndisputableMonolith
 100