T3_FromDistinction
plain-language theorem explainer
T3 on the observable quotient forced by a distinction witness: empty configuration is zero-cost and a left identity for join, empty join is cost-neutral, and independent joins add costs. Anyone closing the early forcing spine from a raw inequality to T0–T3 cites this package. It is a Prop-structure (definitional interface), not a proved theorem; the inhabiting proofs live in the T0+T2-to-T3 constructors.
Claim. Fix a type $K$ and a distinction witness $h:\exists x,y\in K,\, x\neq y$. Let $Q_h$ be the forced observable quotient of $h$, equipped with the transported configuration-space operations and recognition cost $C$. Then T3 on $Q_h$ asserts: $C(\mathrm{emp})=0$; $\mathrm{emp}\mathbin{\ast}\Gamma=\Gamma$ for every configuration $\Gamma$; $C(\mathrm{emp}\mathbin{\ast}\Gamma)=C(\Gamma)$; and if $\Gamma_1$ is independent of $\Gamma_2$, then $C(\Gamma_1\mathbin{\ast}\Gamma_2)=C(\Gamma_1)+C(\Gamma_2)$.
background
The module closes Phase 1 of the T−1→T8 path from a supplied distinction rather than from a global Boolean floor. Given $h:\exists x,y\in K,,x\neq y$, the forced observable quotient $Q_h=\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$ is built and shown equivalent to $\mathrm{Bool}$. Configuration space and recognition-work cost are transported across that equivalence, so every early spine step is stated on the quotient generated by the witness itself.
A configuration space supplies an empty configuration $\mathrm{emp}$, a binary join, a consistency predicate, and an independence relation (no shared predicates), with join a commutative monoid under $\mathrm{emp}$. Recognition cost $C$ is the work functional on those configurations. T0 packages the cheap-consistency / recognition-work surface on $Q_h$; T2 is the companion layer used with T0 to force the present T3 package.
T3 is the ledger fragment: emptiness is free and neutral, and independent joins are strictly additive in cost. That is the algebraic content needed before T4 and the later forcing chain (J-uniqueness, $\varphi$, eight-tick octave, $D=3$).
proof idea
No proof body: this is a Prop-valued structure definition. Its four fields name the T3 axioms on the forced quotient (zero cost of empty, left identity of empty join, cost-neutrality of empty join, additivity of $C$ under independent join).
Inhabitants are built elsewhere. The one-step constructor distinction_T0_T2_to_T3 takes a T0 package and a T2 package on the same quotient and fills the fields (empty-balanced from T0's consistency-cheap fact; the join identities and additivity from the transported ConfigSpace and cost laws). The top-level theorem distinction_forces_T3 is the composition that first forces T0 and T2 from $h$, then applies that constructor.
why it matters
This is the T3 slot in the distinction-threaded early spine. Downstream, distinction_forces_T3 asserts that any distinction witness forces T3 on its own observable quotient, and distinction_T0_T2_to_T3 records the exact T0+T2⇒T3 step. Both feed DistinctionToT0_Spine, the completed early slice: the supplied distinction forces the T−1 floor and T0–T3 on $Q_h$ (with T4 routed through the recognition-operator layer in the /reality variant).
Framework role: without a witness-local T3, the ledger additivity that underwrites recognition cost would sit on an unthreaded global Bool chain, breaking the module's design. With it, Phase 1 can hand a clean T0–T3 floor to the UnifiedForcingChain landmarks (T5 J-uniqueness via the RCL, T6 $\varphi$, T7 eight-tick, T8 $D=3$). Open remainder is the T4 and T5–T8 closure on the same transported floor, not a re-proof of these four field laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.