boolean_floor_atom_route_equivalence
plain-language theorem explainer
From any absolute-floor closure certificate, the Boolean configuration route and the Boolean atom-universe route are the same two-point exit: empty maps to false and marked maps to true, with matching supports. Anyone citing the T-1 handoff into discrete logic or the unified forcing chain would use this identification. The proof fills the equivalence structure by invoking the two existing route constructors and discharging the remaining fields by reflexivity plus the identity equivalence on Bool.
Claim. Given an absolute-floor closure certificate $C$, the Boolean floor-configuration route extracted from $C$'s Boolean witness and the Boolean atom-universe route extracted from $C$ are the same two-point construction: the empty configuration equals the false atom, the marked configuration equals the true atom, their supports match, and the two routes are equivalent via the identity map on $\mathrm{Bool}$.
background
The module builds the complete inevitability chain T-1 through T8 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. That certificate carries a Boolean witness and two self-bootstrap routes.
Two sibling presentations of the same two-point discrete exit appear at this layer. The floor route builds a Boolean configuration space from the witness (empty versus marked). The atom route builds a Boolean distinction-atom universe from the same certificate (false versus true). The structure being proved asserts that these are not merely analogous but definitionally the same two-point route: empty is false, marked is true, supports agree, and a route equivalence exists.
Upstream, the absolute-floor closure certificate is the joint Prop bundling self-bootstrap data, a nontriviality specification equivalence, and the Boolean witness. The Boolean floor-config-from-witness and distinction-atom-universe-from-absolute-floor constructors supply the two legs that this theorem glues.
proof idea
The proof is a structure constructor for the Boolean floor/atom route-equivalence Prop. It sets the floor leg to the existing Boolean floor-config-from-witness applied to the certificate's Boolean witness, and the atom leg to distinction-atom-universe-from-absolute-floor on the full certificate.
The four identification fields (empty config is the false atom, marked config is the true atom, and the two support equalities) are pure definitional equalities, each closed by rfl.
The route-equivalence field is built by refine as a pair whose first component is the identity equivalence on Bool; the two remaining proof obligations are again closed by rfl. No nontrivial algebraic rewriting is required.
why it matters
This declaration seals the T-1 exit: once an absolute-floor certificate exists, there is a single canonical two-point Boolean route, whether one speaks in configuration language or atom-support language. That identification keeps the forcing chain from carrying two competing discrete floors into T0 (logic from cost) and the later ledger steps.
Downstream it is consumed by the T5-to-T6 self-similarity bridge certificate and by the theorem that the bridge holds. The bridge records that unique $J$ plus realized hierarchy dynamics force the scale ratio $\varphi$; a clean Boolean floor/atom identification at T-1 prevents a fork in the discrete substrate those hierarchy arguments sit on. In the primer landmarks this sits at T-1 feeding the chain that reaches T5 $J$-uniqueness and T6 $\varphi$ as the self-similar fixed point.
No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.