IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCocycleCarrier

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase
   2import IndisputableMonolith.Gravity.SevenGaps.Gap2CertifiedFin8PhaseClose
   3import IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridge
   4import IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlocker
   5
   6/-!
   7# Gap2 posting-cocycle carrier: forgetful map + STOP A residual
   8
   9Implements the carrier half of `D-qg-gap2-posting-cocycle-20260723`.
  10
  11The RS eight-tick recognition-posting cocycle already exists as a period-8
  12transaction
  13(`Foundation.PairKernelGap2aPhaseBearingTransactionResidual.phaseBearingActualTransaction_cert`).
  14`CertifiedGap2Fin8PhaseClose` wants a Fin-8 tick on `ExactPathClass`.
  15Those live on different carriers: PairKernel phase is transaction state;
  16`ExactComplex` / `ExactPathClass` carry only incidence (`edgeVerts` /
  17`tetVerts`).
  18
  19## Landed this module
  20
  21* `PostingEnrichedPathClass` / `PostingEnrichedExactHistory`: product
  22  enrichment adjoining an external Fin-8 posting phase.
  23* `forgetPostingPhase` / `postingPhase` and exact-history analogs.
  24* **THEOREM** `carrier_forgets_posting_phase` /
  25  `postingPhase_not_factors_through_forget`: forgetful descent erases
  26  the posting coordinate; the coordinate itself does not descend.
  27* **CLOSED blocker residual**
  28  `TypedResidual_carrier_forgets_posting_phase` (STOP A receipt).
  29* **OPEN** `TypedResidual_posting_cocycle_bridge`: non-forgetful
  30  GE-invariant antipodal bridge still required for certified close.
  31
  32## Explicit refusal
  33
  34Do **not** invent an incidence hash, mod-2 parity, or product-section
  35`⟨c, tau c⟩` and call it the posting cocycle. Prefer this STOP A bank
  36over a fake descent. Does **not** flip `gap2_continuum_and_measure`.
  37No `sorry`, `admit`, new axiom, or `native_decide`. Does **not** touch CPL.
  38-/
  39
  40namespace IndisputableMonolith
  41namespace Gravity
  42namespace SevenGaps
  43namespace Gap2PostingCocycleCarrier
  44
  45open ExactShellGaugeUV
  46open Gap2TickPhaseTailBlocker
  47open Gap2EnrichedCarrierPhase
  48open Gap2CertifiedFin8PhaseClose
  49open Gap2AntipodalBalanceBridge
  50
  51noncomputable section
  52
  53/-! ## §1. Product enrichment and forgetful map -/
  54
  55/-- Exact path class with an adjoined Fin-8 posting-phase coordinate.
  56This is the honest product enrichment of the Gap2 shell carrier by the
  57transaction phase type from the RS eight-tick posting cocycle. -/
  58structure PostingEnrichedPathClass (n : ℕ) where
  59  underlying : ExactPathClass n
  60  postingPhase : Fin 8
  61
  62/-- Forget the posting phase; retain the exact path class. -/
  63def forgetPostingPhase {n : ℕ} (H : PostingEnrichedPathClass n) :
  64    ExactPathClass n :=
  65  H.underlying
  66
  67/-- Read the adjoined posting-phase coordinate. -/
  68def postingPhase {n : ℕ} (H : PostingEnrichedPathClass n) : Fin 8 :=
  69  H.postingPhase
  70
  71theorem forgetPostingPhase_mk {n : ℕ} (c : ExactPathClass n) (p : Fin 8) :
  72    forgetPostingPhase ⟨c, p⟩ = c :=
  73  rfl
  74
  75theorem postingPhase_mk {n : ℕ} (c : ExactPathClass n) (p : Fin 8) :
  76    postingPhase ⟨c, p⟩ = p :=
  77  rfl
  78
  79/-- A family on enriched histories factors through the forgetful map when
  80it depends only on the underlying exact path class. -/
  81def FactorsThroughPostingForget
  82    (f : ∀ n : ℕ, PostingEnrichedPathClass n → Fin 8) : Prop :=
  83  ∃ tau : ∀ n : ℕ, ExactPathClass n → Fin 8,
  84    ∀ (n : ℕ) (H : PostingEnrichedPathClass n),
  85      f n H = tau n (forgetPostingPhase H)
  86
  87/-! ## §2. Carrier forgets posting phase (STOP A) -/
  88
  89/-- **THEOREM.** Descent through `forgetPostingPhase` erases the posting
  90coordinate: any factoring family is constant in `postingPhase`. -/
  91theorem carrier_forgets_posting_phase
  92    (f : ∀ n : ℕ, PostingEnrichedPathClass n → Fin 8)
  93    (h : FactorsThroughPostingForget f)
  94    (n : ℕ) (c : ExactPathClass n) (p q : Fin 8) :
  95    f n ⟨c, p⟩ = f n ⟨c, q⟩ := by
  96  obtain ⟨tau, htau⟩ := h
  97  calc
  98    f n ⟨c, p⟩ = tau n (forgetPostingPhase ⟨c, p⟩) := htau n ⟨c, p⟩
  99    _ = tau n c := by rw [forgetPostingPhase_mk]
 100    _ = tau n (forgetPostingPhase ⟨c, q⟩) := by rw [forgetPostingPhase_mk]
 101    _ = f n ⟨c, q⟩ := (htau n ⟨c, q⟩).symm
 102
 103/-- The posting-phase coordinate does not factor through the forgetful map. -/
 104theorem postingPhase_not_factors_through_forget :
 105    ¬ FactorsThroughPostingForget fun _n H => postingPhase H := by
 106  rintro ⟨tau, htau⟩
 107  let c0 : ExactPathClass 0 := isolatedClass 0
 108  have h0 := htau 0 ⟨c0, 0⟩
 109  have h1 := htau 0 ⟨c0, 1⟩
 110  have hEq : (0 : Fin 8) = 1 := by
 111    calc
 112      (0 : Fin 8) = postingPhase (⟨c0, 0⟩ : PostingEnrichedPathClass 0) := rfl
 113      _ = tau 0 (forgetPostingPhase ⟨c0, 0⟩) := h0
 114      _ = tau 0 c0 := by rw [forgetPostingPhase_mk]
 115      _ = tau 0 (forgetPostingPhase ⟨c0, 1⟩) := by rw [forgetPostingPhase_mk]
 116      _ = postingPhase (⟨c0, 1⟩ : PostingEnrichedPathClass 0) := h1.symm
 117      _ = 1 := rfl
 118  exact (by decide : ¬ ((0 : Fin 8) = 1)) hEq
 119
 120/-- Same forgetfulness at labeled exact-complex product level. -/
 121structure PostingEnrichedExactHistory (v e t : ℕ) where
 122  K : ExactComplex v e t
 123  postingPhase : Fin 8
 124
 125def forgetExactHistory {v e t : ℕ} (H : PostingEnrichedExactHistory v e t) :
 126    ExactComplex v e t :=
 127  H.K
 128
 129def FactorsThroughExactHistoryForget
 130    (f : ∀ v e t : ℕ, PostingEnrichedExactHistory v e t → Fin 8) : Prop :=
 131  ∃ lab : LabeledTick,
 132    ∀ v e t (H : PostingEnrichedExactHistory v e t),
 133      f v e t H = lab v e t (forgetExactHistory H)
 134
 135theorem exact_carrier_forgets_posting_phase
 136    (f : ∀ v e t : ℕ, PostingEnrichedExactHistory v e t → Fin 8)
 137    (h : FactorsThroughExactHistoryForget f)
 138    (v e t : ℕ) (K : ExactComplex v e t) (p q : Fin 8) :
 139    f v e t ⟨K, p⟩ = f v e t ⟨K, q⟩ := by
 140  obtain ⟨lab, hlab⟩ := h
 141  calc
 142    f v e t ⟨K, p⟩ = lab v e t (forgetExactHistory ⟨K, p⟩) := hlab v e t ⟨K, p⟩
 143    _ = lab v e t K := rfl
 144    _ = lab v e t (forgetExactHistory ⟨K, q⟩) := rfl
 145    _ = f v e t ⟨K, q⟩ := (hlab v e t ⟨K, q⟩).symm
 146
 147theorem exact_postingPhase_not_factors_through_forget :
 148    ¬ FactorsThroughExactHistoryForget
 149        fun _v _e _t H => H.postingPhase := by
 150  rintro ⟨lab, hlab⟩
 151  let K0 : ExactComplex 0 0 0 := isolatedVertices 0
 152  have h0 := hlab 0 0 0 ⟨K0, 0⟩
 153  have h1 := hlab 0 0 0 ⟨K0, 1⟩
 154  have hEq : (0 : Fin 8) = 1 := by
 155    calc
 156      (0 : Fin 8) = (⟨K0, 0⟩ : PostingEnrichedExactHistory 0 0 0).postingPhase :=
 157        rfl
 158      _ = lab 0 0 0 (forgetExactHistory ⟨K0, 0⟩) := h0
 159      _ = lab 0 0 0 K0 := rfl
 160      _ = lab 0 0 0 (forgetExactHistory ⟨K0, 1⟩) := rfl
 161      _ = (⟨K0, 1⟩ : PostingEnrichedExactHistory 0 0 0).postingPhase := h1.symm
 162      _ = 1 := rfl
 163  exact (by decide : ¬ ((0 : Fin 8) = 1)) hEq
 164
 165/-! ## §3. Residuals: CLOSED forgetfulness + OPEN non-forgetful bridge -/
 166
 167/-- **CLOSED STOP A residual.** The posting-phase coordinate on product
 168enrichment does not descend through the forgetful map to `ExactPathClass`. -/
 169def TypedResidual_carrier_forgets_posting_phase : Prop :=
 170  ¬ FactorsThroughPostingForget fun _n H => postingPhase H
 171
 172theorem typedResidual_carrier_forgets_posting_phase :
 173    TypedResidual_carrier_forgets_posting_phase :=
 174  postingPhase_not_factors_through_forget
 175
 176/-- **OPEN package.** A GE-invariant labeled tick with antipodal mass
 177balance, i.e. a non-forgetful inhabit route toward
 178`CertifiedGap2Fin8PhaseClose`. Product enrichment cannot supply this via
 179`forgetPostingPhase` (see STOP A). A future session must derive `lab`
 180from exact incidence using period-8 posting semantics, not glue an
 181external Fin-8 coordinate. -/
 182structure PostingCocycleExactPathBridge where
 183  lab : LabeledTick
 184  invariant : GlobalEquivalentInvariant lab
 185  not_shellSig : ¬ ShellSigTick (descendedTick lab invariant)
 186  antipodalBalance :
 187    EventuallyTickFiberAntipodalMassBalanced (descendedTick lab invariant)
 188
 189/-- Descended class-level tick of a bridge (defined when inhabited). -/
 190def bridgeClassTick (B : PostingCocycleExactPathBridge) :
 191    ∀ n : ℕ, ExactPathClass n → Fin 8 :=
 192  descendedTick B.lab B.invariant
 193
 194/-- **OPEN residual.** Nonempty non-forgetful posting-cocycle bridge. -/
 195def TypedResidual_posting_cocycle_bridge : Prop :=
 196  Nonempty PostingCocycleExactPathBridge
 197
 198/-- Packaging helper: a bridge yields a certified recipe package with API
 199honesty markers. Does not inhabit the close. -/
 200def certifiedRecipe_of_bridge (B : PostingCocycleExactPathBridge) :
 201    CertifiedTickRecipe (bridgeClassTick B) where
 202  kind := CertifiedTickRecipeKind.mixedAutMassBalancer
 203  globalEquivalentProvenance := trivial
 204  notAmplitudeOracle := trivial
 205  notShellwiseClassicalAssembly := trivial
 206  tickDerived := trivial
 207
 208/-! ## §4. Status (STOP A banked; gap2 unflipped) -/
 209
 210structure Gap2PostingCocycleCarrierStatus where
 211  enrichedProductCarrierBanked : Bool
 212  forgetfulMapBanked : Bool
 213  carrierForgetsPhaseProved : Bool
 214  postingPhaseDoesNotDescend : Bool
 215  carrierForgetsPhaseResidualClosed : Bool
 216  bridgeResidualDefinedOpen : Bool
 217  certifiedCloseInhabited : Bool
 218  gap2ContinuumAndMeasure : Bool
 219
 220def gap2PostingCocycleCarrierStatus : Gap2PostingCocycleCarrierStatus where
 221  enrichedProductCarrierBanked := true
 222  forgetfulMapBanked := true
 223  carrierForgetsPhaseProved := true
 224  postingPhaseDoesNotDescend := true
 225  carrierForgetsPhaseResidualClosed := true
 226  bridgeResidualDefinedOpen := true
 227  certifiedCloseInhabited := false
 228  gap2ContinuumAndMeasure := false
 229
 230theorem gap2PostingCocycleCarrierStatus_flags :
 231    gap2PostingCocycleCarrierStatus.enrichedProductCarrierBanked = true ∧
 232      gap2PostingCocycleCarrierStatus.forgetfulMapBanked = true ∧
 233      gap2PostingCocycleCarrierStatus.carrierForgetsPhaseProved = true ∧
 234      gap2PostingCocycleCarrierStatus.postingPhaseDoesNotDescend = true ∧
 235      gap2PostingCocycleCarrierStatus.carrierForgetsPhaseResidualClosed =
 236        true ∧
 237      gap2PostingCocycleCarrierStatus.bridgeResidualDefinedOpen = true ∧
 238      gap2PostingCocycleCarrierStatus.certifiedCloseInhabited = false ∧
 239      gap2PostingCocycleCarrierStatus.gap2ContinuumAndMeasure = false := by
 240  decide
 241
 242end
 243
 244end Gap2PostingCocycleCarrier
 245end SevenGaps
 246end Gravity
 247end IndisputableMonolith
 248