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

DefectBoundedSubLedger

show as:
view Lean formalization →

A DefectBoundedSubLedger is a finite list of recognition events equipped with a real-valued total J-cost that is strictly less than phi to the 44 and nonnegative. Researchers formalizing the Hodge conjecture inside Recognition Science cite this structure as the direct analog of a smooth projective variety. The declaration is a plain structure definition that encodes the bounded-defect and nonnegativity conditions with no lemmas or tactics.

claimA DefectBoundedSubLedger consists of a finite list of recognition events together with a real number $d$ satisfying $d < phi^{44}$ and $d >= 0$.

background

In the Recognition Science translation of the Hodge conjecture, a smooth projective algebraic variety becomes a DefectBoundedSubLedger: a finite collection of recognition events whose aggregate J-cost (defect) remains finite. The J-cost functional originates in the LedgerFactorization upstream result, which calibrates the multiplicative structure on positive reals and ensures nonnegativity. Coarse-graining flows and stable cohomology classes are subsequently defined on top of such ledgers.

proof idea

This is a structure definition that directly packages a list of recognition events with a real defect value and the two inequalities defect < phi^44 and 0 <= defect. No lemmas are invoked; the definition itself supplies the non-singularity condition required by the module's RS dictionary.

why it matters in Recognition Science

The structure supplies the ambient space for every downstream object in the module, including CoarseGrainingFlow, CoarseGrainingStableClass, CohomologyClass, defect_budget_theorem, and HodgeCert. It fills the base case of the RS Hodge dictionary (variety = DefectBoundedSubLedger) and enables the one-direction theorem that every JCostMinimalCycle is a CoarseGrainingStableClass. The bounded-defect hypothesis directly supports the defect-budget argument that stable classes must carry zero charge.

scope and limits

formal statement (Lean)

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

used by (33)

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

… and 3 more

depends on (30)

Lean names referenced from this declaration's body.