`IndisputableMonolith.Gravity.SevenGaps.Gap2ExactClassCarrierAttack`

IndisputableMonolith/Gravity/SevenGaps/Gap2ExactClassCarrierAttack.lean · 27 lines · 1 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase
   2
   3/-!
   4# Gap2ExactClassCarrierAttack (superseded stub)
   5
   6Binary-carrier draft from session qg-full-completion-continue-20260722 was
   7superseded by `Gap2EnrichedCarrierPhase` (Fin-8 enriched labeled tick +
   8sharper R5 residual). This module re-exports the live attack surface so
   9stale Elmo target names stay green.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Gravity
  14namespace SevenGaps
  15namespace Gap2ExactClassCarrierAttack
  16
  17open Gap2EnrichedCarrierPhase
  18
  19theorem superseded_by_enriched_carrier :
  20    Nonempty EnrichedCarrierPhaseSubstrate :=
  21  enrichedCarrierPhaseSubstrate_nonempty
  22
  23end Gap2ExactClassCarrierAttack
  24end SevenGaps
  25end Gravity
  26end IndisputableMonolith
  27

source mirrored from github.com/jonwashburn/shape-of-logic