forcedQuotient_recognition_work_constraint
plain-language theorem explainer
Given any type with two distinct elements, the forced observable quotient carries a recognition-work constraint certificate. Citers are those closing the distinction-to-T0 path on the witness-generated floor rather than global Bool. The proof is a one-line application of the general recognition-work constraint theorem to the cost already transported onto that quotient.
Claim. Let $K$ be any type and suppose there exist $x,y\in K$ with $x\neq y$. Write $Q$ for the forced observable quotient of $K$ by the distinction setoid. Then there is a nonempty recognition-work constraint certificate on $Q$: a cost $C:Q\to\mathbb{R}_{\ge 0}$ obeying dichotomy (zero iff consistent) and independent additivity, with $C(\emptyset)=0$ and $C>0$ exactly on inconsistent configurations.
background
This module opens Phase 1 of the T−1→T8 closure: start from a supplied distinction witness $h:\exists x,y:K,,x\neq y$, build the forced observable quotient $Q=\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$, and transport Boolean configuration structure and recognition cost across the equivalence $Q\simeq\mathrm{Bool}$. The point is to run the early forcing spine on the quotient generated by the witness itself, not on an unthreaded global Boolean floor.
A cost function on a configuration space is a map $C$ to nonnegative reals satisfying dichotomy (cost zero iff the configuration is consistent) and independent additivity (cost adds over joins of configurations that share no predicates). The recognition-work constraint certificate packages such a cost with its immediate consequences: empty cost zero, positivity exactly on inconsistent configurations, and a calibration that picks a specific inconsistent configuration of positive cost.
Upstream, the general recognition-work constraint theorem states that any cost function on any configuration space yields a nonempty such certificate. The sibling forcedQuotientRecognitionCost supplies the concrete cost on $Q$ obtained by transport from the Boolean floor.
proof idea
One-line term wrapper. Apply the general recognition-work constraint theorem to the already-constructed cost on the forced quotient (the transported recognition cost for witness $h$). That theorem returns Nonempty (RecognitionWorkConstraintCert Config) for any cost satisfying the bridge axioms, so the goal is immediate.
why it matters
This is the recognition-work leg of T0 on the distinction-generated quotient. Downstream, distinction_forces_T0 assembles T0-from-distinction by bundling three pieces: the quotient-to-Bool equivalence, this recognition-work certificate, and a consistency-cheapness fact. Without this lemma the transported floor would have configuration structure but no certified recognition-work surface.
In the broader forcing chain this is Phase 1 scaffolding toward T0–T4 routed through the witness quotient rather than global Bool. The module doc is explicit: T1–T4 will ride this transported floor. It does not yet touch J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8); those sit further along the spine once T0 is locked on the distinction quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.