DefectBoundedSubLedger
plain-language theorem explainer
DefectBoundedSubLedger models a smooth projective algebraic variety in Recognition Science as a finite list of recognition events whose total J-cost satisfies a strict upper bound. Researchers formalizing the Hodge conjecture in this framework cite the structure when defining the domain for cohomology classes and algebraic cycles. The declaration is a plain structure definition that directly encodes the boundedness and non-negativity conditions on the defect.
Claim. A structure consisting of a finite list of recognition events together with a real number $defect$ satisfying $0 ≤ defect < φ^{44}$.
background
The module translates the classical Hodge conjecture into Recognition Science terms: a smooth projective complex algebraic variety becomes a DefectBoundedSubLedger (finite voxel set with bounded J-cost), a Hodge class becomes a CoarseGrainingStableClass that survives the data processing inequality, and an algebraic cycle becomes a JCostMinimalCycle with zero net defect. The local setting is the one-direction theorem that every JCostMinimalCycle is a CoarseGrainingStableClass, while the converse remains open. Upstream results supply the underlying J-cost functional via LedgerFactorization and the defect notion via LawOfExistence.
proof idea
This is a structure definition with four fields: the list of events, the real-valued defect, and the two inequalities defect < phi^44 and 0 ≤ defect. No lemmas or tactics are applied.
why it matters
The structure is the base type for CoarseGrainingStableClass, CoarseGrainingFlow, defect_budget_theorem, and HodgeCert in the same module. It implements the 'variety' slot in the RS dictionary given in the module documentation and supplies the domain for the defect budget bridge that would prove the open direction of the conjecture. It touches the T5 J-uniqueness and T6 phi fixed-point landmarks through the J-cost bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.