CoarseGrainingFlow
plain-language theorem explainer
A coarse-graining flow on a DefectBoundedSubLedger is a monotone nonincreasing nonnegative sequence of real numbers whose value at scale zero equals the sub-ledger defect. Researchers formalizing the RS version of the Hodge conjecture cite this structure when they need to express data-processing inequalities on defect-bounded collections of recognition events. The definition simply packages the four required fields with no further computation.
Claim. A coarse-graining flow on a defect-bounded sub-ledger $L$ is a function $d:ℕ→ℝ$ such that $d(0)=defect(L)$, $d(n+1)≤d(n)$ for every natural number $n$, and $d(n)≥0$ for every $n$.
background
In the module the Hodge conjecture is restated by identifying a smooth projective variety with a DefectBoundedSubLedger: a finite list of recognition events whose total J-cost (defect) is bounded by $ϕ^{44}$. The doc-comment states that a coarse-graining flow is the RS analog of the heat flow, recording how apparent defect decreases when the ledger is viewed at successively coarser scales.
proof idea
Structure definition that directly records the four fields: the defect sequence, the initial-value axiom, the monotonicity axiom, and the nonnegativity axiom.
why it matters
The structure supplies the object required by the defect-budget theorem and by the definitions of flowLimit and IsFlowStable. It therefore supports the proved direction of the RS Hodge conjecture (every JCostMinimalCycle is CoarseGrainingStableClass) while leaving the converse open. The construction mirrors the classical heat-flow picture used to isolate Hodge classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.