T4_Recognition_Forced
plain-language theorem explainer
T4 packages the claim that the Boolean two-point floor carries a recognition witness: distinct states exist, recognition Bool→Bool is inhabited, some RecognitionStructure has carrier Bool, and zero cost on the consistent state implies recognition is available. Downstream T2/T3→T4 and T4→T5 bridges and the complete T−1..T8 spine cite it. Pure Prop structure (definitional interface), no proof body.
Claim. The T4 recognition package on the Boolean floor asserts: (i) $\exists a,b:\mathrm{Bool}$ with $a\neq b$; (ii) the type of recognition maps $\mathrm{Bool}\to\mathrm{Bool}$ is inhabited; (iii) there exists a recognition structure whose underlying carrier equals $\mathrm{Bool}$; (iv) if the Boolean recognition-work cost of the consistent state is zero ($C(\mathsf{false})=0$), then recognition $\mathrm{Bool}\to\mathrm{Bool}$ is inhabited.
background
This module is the public T−1 through T8 forcing spine. T−1 is the absolute distinguishability floor; T0 the Boolean recognition-work split; T1 the cost-form meta-principle; T2 two-state discreteness; T3 additive ledger bookkeeping; T4 the recognition witness on that discrete floor. Later steps force J-uniqueness (T5), φ (T6), the eight-tick octave (T7), and D=3 (T8).
The Boolean recognition-work cost is the concrete two-point cost $C(\mathsf{false})=0$, $C(\mathsf{true})=1$. A recognition structure is a symmetric, reflexive binary relation recognizes on a carrier type. Upstream discreteness (T2) already forces the exhaustive split $\Gamma=\mathsf{false}\lor\Gamma=\mathsf{true}$ with zero cost selecting consistency and positive cost selecting the marked state; the ledger package (T3) records that the empty state is balanced and join-neutral.
T4 sits after that split and ledger: it records that recognition itself is forced as a witness on the Boolean carrier, not merely that costs and joins behave correctly.
proof idea
Definitional Prop structure, not a proved theorem. The four fields are the interface: existential distinction on Bool; Nonempty of recognition Bool→Bool; existence of a RecognitionStructure with carrier Bool; and the implication from zero Boolean cost on false to inhabited recognition. Inhabitants are supplied later by bridge constructors such as T2_T3_To_T4_Bridge, which derive distinction from T2 and balanced-floor recognition certificates from T3's empty-cost identity.
why it matters
T4 is the spine step the module labels "recognition witness on the discrete floor." It is consumed by T2_T3_To_T4_Bridge, the T4→T5 realization and cost bridges, t4_to_t5_bridge_holds, and the aggregate CompleteForcingChainT8 / CompleteForcingChain records.
In the forcing chain it is the hinge between ledger discreteness and the reciprocal cost law: once recognition is witnessed on Bool, later bridges expose a realization surface and an RCL surface aimed at T5 (J-uniqueness, $J(x)=(x+x^{-1})/2-1$).
Audit honesty note on the T4→T5 arrow: T5 uniqueness is proved from CostUniqueness and law_of_logic_forces_jcost and does not substantively consume the T−1..T4 floor; deleting T−1..T4 would break no T5 proof. The open gap is that the floor's own cost cannot satisfy the continuous reciprocal law that forces J. T4 still earns its place as the named recognition interface the public spine and bridge records thread through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.