trueAtomSupportEvent
plain-language theorem explainer
Seed support event whose finite support is the singleton {true} on the canonical two-atom distinction universe (Bool). Anyone building the atom-support route from the absolute floor, or proving the two seed supports are disjoint, cites this carrier. The body is a one-line structure constructor packing that singleton.
Claim. The seed support event for the true atom is the support-bearing event on the canonical two-atom universe (identified with $\mathrm{Bool}$) whose support is the singleton Finset $\{true\}$.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). Near T-1, a bare distinction must supply a concrete two-point carrier before ledger and recognition structure can sit on top of it.
SupportEvent is the canonical model of a support-bearing event: a structure whose only data is a finite set of atoms. Independence is not an extra predicate; it is ordinary disjointness of those finite supports. The carrier type here is the canonical distinction atom universe, defined to be Bool.
Together with the matching false-atom seed, this true-atom seed is the minimal pair of events that witness a non-singleton universe of atoms forced by a bare distinction.
proof idea
Pure definition, not a proof. The structure constructor for a support event is applied to the singleton Finset {true} on the Boolean atom type. No lemmas are invoked; the term is the packed support.
why it matters
This seed is one half of the two-point atom-support route out of the absolute floor (T-1). Downstream, canonicalDistinctionAtom_seed_disjoint uses it (with the false seed) to prove the two canonical supports are disjoint, which is exactly independence in the SupportEvent model. CanonicalDistinctionAtomUniverse packages that disjointness into the certificate that the Boolean atom carrier is a genuine finite distinction universe. BooleanFloorAtomRouteEquivalence then identifies the Boolean floor-configuration route with this atom-support route: false is the empty/configuration atom and true is the marked atom. Without these seeds the T-1 non-singleton precondition cannot be stated in the support-event language that later feeds T0 logic-from-cost and the rest of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.