forcedQuotientRecognitionCost_transport

This module opens the closure path from a supplied distinction witness to the early forcing spine (Phase 1 of T−1→T8). Given $h:\exists x,y\in K,,x\neq y$, one forms the forced observable quotient $\mathrm{ForcedQuotient}(h)=K/\sim_h$ and proves it equivalent to $\mathrm{Bool}$. The point is to thread T0 through that witness-generated quotient rather than through unthreaded global Boolean facts.

The forced quotient-to-Bool map is the coordinate equivalence used throughout. Recognition-work cost on the quotient is defined by pulling back the Boolean recognition cost along that equivalence: $C(\Gamma)$ is the Boolean cost of the image of $\Gamma$. The Boolean cost itself is the T−1→T0 recognition-work surface from the unified forcing chain.

This lemma records that the transport is literal, not up to a further isomorphism or renormalization.

One-line definitional reflexivity. The recognition-work cost on the forced quotient is defined by $C(\Gamma) := C_{\mathrm{Bool}}(\mathrm{equiv}(\Gamma))$, so the stated equality is rfl. No algebraic reduction or lemma application is required beyond unfolding that definition.

This identity is the cost-transport step that lets T0 live on the distinction-generated quotient. Downstream, distinction_forces_T0 packages the quotient-Bool equivalence with the recognition-work constraint to conclude that a supplied distinction forces T0 on its own observable quotient. The same transport is rewritten in rank1_cost_is_boolean_truncation to identify rank-1 ledger floor cost with Boolean cost of truncated multiplicity, and it feeds the Phase-2 ledger-floor bridge for every distinction witness and positive weight.

In the forcing chain this is the T−1→T0 floor threaded by the witness, not a free-standing Boolean axiom. Later T1–T4 steps in this module route through the transported floor rather than global Bool facts, keeping the distinction witness in the dependency path.