CoarseGrainingFlow
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prescribe any concrete coarse-graining map on the underlying events.
- Does not assert that the defect sequence converges.
- Does not tie the integer scale index to the phi-ladder or to physical length scales.
- Does not constrain the z-charge of any cohomology class.
formal statement (Lean)
188structure CoarseGrainingFlow (L : DefectBoundedSubLedger) where
189 /-- Defect at scale 2^n (coarsened n times) -/
190 coarsened_defect : ℕ → ℝ
191 /-- At scale 0, we see the full defect -/
192 at_zero : coarsened_defect 0 = L.defect
193 /-- Coarse-graining is monotone: zooming out can only decrease apparent defect -/
194 monotone_decrease : ∀ n, coarsened_defect (n + 1) ≤ coarsened_defect n
195 /-- Defect is always nonneg -/
196 nonneg : ∀ n, 0 ≤ coarsened_defect n
197
198/-- Any DefectBoundedSubLedger admits a trivial (constant) coarse-graining flow. -/