pith. machine review for the scientific record. sign in
structure definition def or abbrev high

CoarseGrainingStableClass

show as:
view Lean formalization →

Coarse-graining stable classes are cohomology classes on defect-bounded subledgers whose charge satisfies z_charge ≤ defect(L). Researchers formalizing the Recognition Science version of the Hodge conjecture cite this when separating Hodge classes from algebraic cycles. The declaration is a structure definition that extends CohomologyClass by a single inequality field.

claimLet $L$ be a defect-bounded subledger. A coarse-graining stable class on $L$ is a cohomology class $z$ (satisfying $z ≥ 0$) such that $z ≤ defect(L)$.

background

In the module's RS dictionary a DefectBoundedSubLedger is a finite list of recognition events whose total J-cost (defect) is bounded by φ^44 and nonnegative. A CohomologyClass on such an L is a nonnegative real z_charge that encodes topological charge of type (p,p). The module translates the classical Hodge conjecture by identifying Hodge classes with classes that survive coarse-graining and algebraic cycles with JCostMinimalCycles (recognition-closed subgraphs whose boundary nodes are balanced). Upstream the defect functional equals J(x) and every ledger is balanced by construction.

proof idea

The declaration is a structure definition extending CohomologyClass with the single field dpi_stable that records the inequality z_charge ≤ L.defect.

why it matters in Recognition Science

It supplies the Hodge-class side of the RS Hodge conjecture stated in the module. Downstream it is used by defect_budget_theorem (any class stable under all flows has z_charge = 0) and by HodgeCert (which records that every JCostMinimalCycle yields a stable class). The open converse direction of the conjecture remains that every stable class is generated by minimal cycles.

scope and limits

formal statement (Lean)

  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. -/

used by (24)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (23)

Lean names referenced from this declaration's body.