CoarseGraining
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.