CoarseGraining
A coarse-graining map reduces resolution from a finite set of n elements to one of m elements by a surjective function. Researchers formalizing the Recognition Science version of the Hodge conjecture cite this structure when expressing stability of cohomology classes under resolution reduction via the Data Processing Inequality. The declaration is a direct structure definition consisting of the map field and its surjectivity condition.
claimA coarse-graining map from a finite set of cardinality $n$ to one of cardinality $m$ is a surjective function $Fin n → Fin m$.
background
In the Recognition Science translation, a defect-bounded sub-ledger carries a J-cost that sums recognition costs over its voxels. Coarse-graining maps reduce resolution while the Data Processing Inequality guarantees that J-cost cannot increase, so features surviving every such map are the stable topological ones. The module formalizes the converse direction of the RS Hodge conjecture: every coarse-graining-stable cohomology class arises from a J-cost minimal sub-ledger, which counts as an algebraic cycle (recognition-closed subgraph).
proof idea
The declaration is a direct structure definition. It introduces the two fields map : Fin n → Fin m and surjective : Function.Surjective map with no lemmas applied and no proof body.
why it matters in Recognition Science
This definition supplies the basic operation needed for the Hodge → Algebraic direction in the module. The module strengthens the RS translation by showing that coarse-graining-stable classes are generated by J-cost minima, referencing biggest-questions.md §XIII Q2 and the Millennium Prize Problems/hodge-unconditional-dec-14.tex. It touches the open question of an unconditional RS proof of the Hodge conjecture.
scope and limits
- Does not impose J-cost minimality on the map itself.
- Does not define the induced map on cohomology classes.
- Does not enforce preservation of defect bounds.
- Does not reference the phi-ladder or constants such as phi^5.
formal statement (Lean)
70structure CoarseGraining (n m : ℕ) where
71 map : Fin n → Fin m
72 surjective : Function.Surjective map
73
74/-- A class is coarse-graining-stable if it survives all coarse-grainings.
75 In RS terms: it is detected by the Data Processing Inequality —
76 D_KL only decreases under coarse-graining, so features that persist
77 through all coarse-grainings are the "real" topological features. -/