count
plain-language theorem explainer
Event count on a recognition cell is the cardinality of its multiset of canonical events. Cosmology and ledger arguments cite it as the simplest conserved functional under rung-coarsening. The definition is a one-line alias of multiset cardinality; no proof content.
Claim. For a multiset $m$ of canonical recognition events (each a directed posting source $\to$ target carrying a positive ratio), the event count is $\lvert m\rvert$, the cardinality of $m$.
background
Module T-1 formalizes rung-coarsening for the scale-adaptive Cosmogenesis engine: a recognition cell at one $\varphi$-rung is an unordered multiset of canonical events. An Event is a directed posting with natural-number endpoints and a positive real ratio; double-entry reciprocity is implicit.
Coarsening partitions events into internal (both endpoints in one block) and cross (endpoints in different blocks, relabeled to coarse sites). Conserved functionals of the cell are functions of the multiset alone. Among them, event count is the blunt size measure: how many recognition postings the cell carries, independent of ratios or geometry.
The sibling spectrum maps the same multiset to log-ratios; cost and net flow ($\sigma$) are heavier functionals. Count is the base instance used when stating that round-trip coarsen/refine preserves every multiset functional.
proof idea
Pure definition: count m is Multiset.card m. No lemmas, no tactics. Downstream preservation theorems reduce to the fact that round-trip returns the identical multiset, so cardinality is automatic.
why it matters
T-1 claims every conserved functional is preserved under coarsening because refine(coarsen $m$)=$m$. Event count is the first named instance (count_preserved in the module narrative): coarsening loses no recognition postings reality has determined.
That underwrites the "literal" reading of rung-coarsening in the Cosmogenesis spine: idle cells carry empty refinements, active cells keep exact event totals across $\varphi$-rungs, and cost/spectrum/$\sigma$ sit on the same multiset identity. Count is scaffolding for those stronger conservation statements rather than a deep theorem itself.
Framework role is local to cosmology ledger exactness, not the T0–T8 forcing chain; it supports exact multi-rung bookkeeping before continuum or gravity layers attach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.