`DefectBoundedSubLedger`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.HodgeConjecture
domain: Mathematics
line: 56 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.HodgeConjecture on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  53/-- A DefectBoundedSubLedger is a finite set of recognition events
  54    (the RS analog of a smooth projective algebraic variety).
  55    It has bounded total J-cost: the "defect" of the sub-ledger is finite. -/
  56structure DefectBoundedSubLedger where
  57  /-- Recognition events in the sub-ledger -/
  58  events : List RecognitionEvent
  59  /-- Defect = total J-cost of all recognition events -/
  60  defect : ℝ
  61  /-- Defect is bounded (the variety is non-singular) -/
  62  defect_bounded : defect < phi ^ 44
  63  /-- Defect is nonneg (J-cost is always nonneg) -/
  64  defect_nonneg : 0 ≤ defect
  65
  66/-- A cohomology class on a DefectBoundedSubLedger is a real number
  67    (encoding the "charge" of the class in the Z-complexity sense). -/
  68structure CohomologyClass (L : DefectBoundedSubLedger) where
  69  /-- The characteristic value of the class (Z-charge) -/
  70  z_charge : ℝ
  71  /-- The type (p,p) condition in RS: charge is symmetric about 0 -/
  72  symmetric : z_charge ≥ 0
  73
  74/-- A CoarseGrainingStableClass is a cohomology class that survives
  75    "zooming out" — the Data Processing Inequality (DPI).
  76    A class survives coarse-graining iff its z_charge is anchored to
  77    the actual J-cost structure (not just a statistical artifact). -/
  78structure CoarseGrainingStableClass (L : DefectBoundedSubLedger) extends CohomologyClass L where
  79  /-- Stability condition: z_charge is a fixed point under DPI -/
  80  dpi_stable : z_charge ≤ L.defect
  81
  82/-- A JCostMinimalCycle is a recognition-closed subgraph with zero net defect:
  83    the RS analog of an algebraic cycle. Every boundary node is balanced. -/
  84structure JCostMinimalCycle (L : DefectBoundedSubLedger) where
  85  /-- The events in the cycle -/
  86  cycle_events : List RecognitionEvent

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.