supportMap
plain-language theorem explainer
Projects a support-bearing event to its finite set of atoms. Anyone working the Boolean-atom or seed-support models in the forcing chain cites this as the canonical support extractor. The body is a one-field projection: no proof content.
Claim. For a support event $a$ on an atom type $A$, the support map returns the finite set $\mathrm{supp}(a)\subseteq A$ carried by $a$.
background
In the Unified Forcing Chain, independence is not an extra predicate: it is disjointness of finite supports. The carrier is SupportEvent, a structure whose only data is a Finset of atoms. Join is union and the empty event is the empty set, so the configuration space is the free join-semilattice on finite subsets.
The module's stronger claim is that T-1 through T8 are forced from the Recognition Composition Law plus normalization and calibration. At the absolute-floor end, a bare distinction must be realized by two seed events whose supports do not overlap. The support map is the forgetful arrow that turns those events into the sets used by every disjointness and observation lemma downstream.
Upstream cost definitions (J-cost on ratios, recognizer-derived cost, observer cost) motivate why support cardinality later becomes the recognition-work measure; this map itself only exposes the underlying finite set.
proof idea
Definitional one-liner: return the structure field support. No tactics, no lemmas.
why it matters
This is the handle every seed-support and observation certificate uses. Downstream it appears in the canonical level-tagged seed model, the two-atom disjointness theorem for false/true seed events, the canonical support-observation package (finite-support observation plus identity quotient), and the Boolean floor/atom-route equivalence that identifies the T-1 two-point construction with empty vs marked atom.
In the forcing chain it sits under T-1 (absolute floor) and the Boolean atom universe: once supports are exposed, independence is Finset disjointness, and the Boolean floor route collapses to the same two-point distinction. It does not itself force J, φ, or D=3; it supplies the set-theoretic interface those later steps consume when they talk about independent recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.