Event
plain-language theorem explainer
A recognition event is a directed posting from a natural-number source site to a target site, carrying a real ratio. Cosmology modules treat a recognition cell as a multiset of these events. Downstream coarsening, refinement triggers, and conservation proofs all quantify over this type. The declaration is a plain three-field structure with no proof obligations.
Claim. A recognition event is a triple $(s,t,r)$ with source site $s \in \mathbb{N}$, target site $t \in \mathbb{N}$, and ratio $r \in \mathbb{R}$. It records a directed posting $s \to t$ carrying ratio $r$; the double-entry reciprocal is left implicit.
background
Module T-1 (rung-coarsening) models a recognition cell at one phi-rung as a multiset of canonical recognition events. Order is irrelevant: every conserved functional of the cell is a function of that multiset alone. A block map $\mathrm{block}:\mathbb{N}\to\mathbb{N}$ sends fine sites to coarse sites and partitions events into internal (both endpoints in one block) and cross (endpoints in different blocks).
The structure here is the atomic datum of that model: source and target are discrete site labels, and ratio is the real coordinate that enters recognition cost (the same ratio coordinate used in CPT factorization arguments). Downstream, cost of a singleton multiset is just the cost weight of the event's ratio, and demand of a coarse block is the cost of its internal postings.
This is the cosmology-layer event type, not the finite-space distinction event of the primitive recognition calculus (which is a predicate on $\mathrm{Fin}(N+1)$). The double-entry reciprocal is not stored as a second field; it is recovered by the ledger conventions referenced as doubled in the module.
proof idea
No proof. The declaration is a three-field structure (source, target, ratio) with default constructor and projections. Downstream lemmas pattern-match on these fields or build singleton multisets such as ${\langle 0,1,r\rangle}$.
why it matters
T-1 of the scale-adaptive Cosmogenesis engine treats coarsening as sigma-exact and cost-exact precisely because cells are multisets of these events. Round-trip identity, cost partition, spectrum preservation, and idle-cell emptiness are all statements about Multiset Event under block maps.
The RefineTrigger layer builds on the same type: demand is internal cost of events in a block; the law-given descent rule descends exactly blocks that carry an internal posting; epsilon_unsafe exhibits a single-event cell whose demand is an arbitrarily small positive J-cost, so only the zero threshold is lossless. cost_singleton reduces cost on a singleton to the weight of e.ratio.
In the broader RS picture this is the discrete posting atom of the ledger at cosmological rungs: ratios feed the J-cost, and conservation of count, cost, spectrum, and net flow under coarsening is what makes rung ascent "literal" rather than approximate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.