BooleanFloorAtomRouteEquivalence
plain-language theorem explainer
The Boolean floor-configuration path and the Boolean atom-support path out of a fixed absolute-floor certificate are the same two-point construction: empty is the false atom, marked is the true atom. Anyone working the T-1 bridge into the support-event or T0 layers cites this certificate. It is a pure Prop bundle (routes, support equalities, identity equivalence on Bool), propositionally unique by subsingleton.
Claim. Fix an absolute-floor closure certificate $C$. A Boolean-floor/atom-route equivalence for $C$ is the assertion that (i) the Boolean floor configuration interface is realized from $C$'s Boolean witness, (ii) the Boolean two-atom support universe is realized from $C$, (iii) the empty configuration equals the false atom and the marked configuration equals the true atom, (iv) the false and true atom supports are the corresponding singletons in the canonical distinction-atom carrier $A$, and (v) there exists an equivalence $e:\mathrm{Bool}\simeq A$ with $e(\mathsf{false})=\mathsf{false}$ and $e(\mathsf{true})=\mathsf{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). T-1 is the absolute floor: a meta-language Prop distinction together with a non-singleton universe, packaged as an absolute-floor closure certificate carrying a Boolean absolute-floor witness.
Two concrete two-point presentations leave that floor. The floor-configuration route records that the Boolean witness yields the empty/marked ledger interface of a configuration space (empty configuration is false, dichotomy and nontriviality). The atom-universe route records that the same closure supplies the canonical distinction-atom carrier used by support events, where independence is disjointness of finite supports.
A configuration space is the abstract monoid of configurations with empty unit, join, consistency, and independence. Support events are the canonical model whose carrier is finite atom sets. This structure asserts those two routes are literally the same Bool two-point object.
proof idea
No proof body: the declaration is a Prop-valued structure, not a theorem. It packages six fields (floor route, atom route, empty=false, marked=true, the two singleton support equalities, and existence of an identity-on-points equivalence Bool ≃ canonical atom). A companion Subsingleton instance discharges uniqueness by rfl (all fields are propositions). The inhabiting construction lives downstream in the named equivalence theorem, which fills the fields from the Boolean-floor-from-witness and atom-universe-from-floor lemmas plus reflexivity.
why it matters
In the complete inevitability chain, T-1 must hand a single unambiguous two-point carrier to every later layer. This certificate is the glue: it identifies the Boolean floor used by the T0 logic-from-cost bridge with the Boolean atom universe used by the support-event and distinction layers, so no second Boolean ontology is smuggled in.
The parent theorem boolean_floor_atom_route_equivalence inhabits the structure from any absolute-floor closure certificate. The structure also appears on the T5-to-T6 self-similarity bridge dependency surface, keeping the early Boolean identification available when the chain later forces unique J and then φ as the self-similar ratio. Framework landmark: T-1 absolute floor feeding T0 (logic from cost minimization). It closes a definitional gap rather than an open analytic question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.