forcedQuotientRecognitionCost
plain-language theorem explainer
Given a distinction witness on a type K, the recognition-work cost on the forced observable quotient is the Boolean recognition cost pulled back along the forced quotient-to-Bool equivalence. Anyone closing the T−1→T0 spine from a concrete distinction cites this surface. The definition is a structure instance that transports nonnegativity, dichotomy, and independent additivity fieldwise from the Boolean cost.
Claim. For any type $K$ and witness $h:\exists x\,y:K,\,x\neq y$, there is a cost function $C$ on the forced observable quotient $Q_h$ defined by $C(\Gamma)=C_{\mathrm{Bool}}(\varphi_h(\Gamma))$, where $\varphi_h:Q_h\simeq\mathrm{Bool}$ is the forced coordinate equivalence and $C_{\mathrm{Bool}}$ is the Boolean recognition-work cost. The transported $C$ satisfies nonnegativity, dichotomy (zero cost iff the configuration is consistent), and independent additivity over joins.
background
The module DistinctionToT4 opens the real closure path from a supplied distinction witness to the early forcing spine (Phase 1 of T−1→T8). Given $h:\exists x,y:K,,x\neq y$, the forced observable quotient $Q_h$ is the quotient of $K$ by the forced observable setoid; it is equivalent to $\mathrm{Bool}$. The point is not to reuse the global Boolean chain while ignoring the witness, but to thread cost and configuration structure through that quotient.
A cost function on a configuration space is a map $C$ into the nonnegative reals obeying two recognition-work axioms: dichotomy (cost vanishes exactly on consistent configurations) and independent additivity (cost adds over joins of configurations that share no predicates). The Boolean recognition-work cost already satisfies these on the global Bool floor.
Upstream, TMinus1ForcedFromDistinction builds the quotient and the Bool equivalence. UnifiedForcingChain supplies the Boolean recognition cost used as the transport source.
proof idea
The definition builds a CostFunction instance on the forced quotient by pure transport. Cost of a quotient configuration $\Gamma$ is the Boolean recognition cost of its image under the forced quotient-to-Bool equivalence.
Nonnegativity applies the Boolean nonnegativity field to that image. Dichotomy is rewritten as the Boolean dichotomy statement on the image, then discharged by the Boolean field. Additivity rewrites the join of two quotient configurations via join-compatibility of the Bool equivalence, then invokes Boolean additivity on the two images (using the same independence hypothesis).
why it matters
This is the recognition-work floor on the distinction-generated quotient, not the unthreaded global Bool. Downstream it feeds the recognition-work constraint certificate, the T0-from-distinction structure, and the theorem that a supplied distinction forces T0 on its own observable quotient. The T1–T4 packages and the step theorems (T0 to T1, T1 to T2, etc.) route through this transported cost rather than global Bool facts.
In the Recognition Science forcing chain, T0 is the recognition-work surface that begins the spine toward T5 J-uniqueness, T6 $\varphi$ as self-similar fixed point, T7 eight-tick octave, and T8 with $D=3$. Closing T0 on the quotient generated by the distinction itself is the first concrete step of that Phase-1 path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.