forcedBooleanCoordinateChange
plain-language theorem explainer
Coordinate change between two Boolean coordinate systems on the quotient forced by one distinction witness. Anyone proving uniqueness of those coordinates up to Boolean automorphism cites this map. It is the composite of the inverse of the first coordinate equivalence with the second, yielding a Bool automorphism.
Claim. Fix a type $K$ with a distinction witness $h:\exists x,y\in K,\,x\neq y$. Given two Boolean coordinate systems $c_1,c_2$ on the forced observable quotient of $h$ (each an equivalence from that quotient to $\mathrm{Bool}$), the coordinate change is the Boolean automorphism $c_1.\mathrm{coord}^{-1}\circ c_2.\mathrm{coord}:\mathrm{Bool}\simeq\mathrm{Bool}$.
background
The module rebuilds the T−1 floor from a single object-level distinction witness $h:\exists x,y:K,,x\neq y$, rather than from an external admissibility package. From $h$ one constructs a marked pair, the Boolean projection generated by that distinction, the observable equivalence relation it induces, and the resulting two-class quotient.
A Boolean coordinate system on that quotient is a structure packaging an equivalence $\mathrm{Quotient}(\sim_h)\simeq\mathrm{Bool}$. Two such systems may label the two classes differently; the present definition records the pure relabeling between them. The ambient thesis is that once a distinction exists, the Boolean/observable floor is forced, not assumed as an extra measure.
proof idea
One-line definitional composite: take the inverse of the first coordinate equivalence and transitively compose with the second. The result is an equivalence $\mathrm{Bool}\simeq\mathrm{Bool}$. No lemmas are invoked; the term is pure equivalence algebra on the two packaged maps.
why it matters
This map is the witness used by the uniqueness theorem: Boolean coordinates forced by the same distinction are unique up to Boolean automorphism, stated as $c_2.\mathrm{coord}=c_1.\mathrm{coord}\circ(\text{coordinate change})$. That uniqueness is one of the explicit deliverables of the T−1 repair listed in the module doc (alongside the marked pair, Boolean projection, observable setoid, two-class quotient, and the legacy raw floor for RealityCertificate).
In the Recognition forcing chain this sits below T0–T8: it closes the object-level Boolean floor so that later steps (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) rest on a distinction-forced rather than half-measure interface. Without a distinction there is no forcing; with one, the coordinate ambiguity is exactly $\mathrm{Aut}(\mathrm{Bool})$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.