T4_Recognition_Forced
plain-language theorem explainer
T4 packages the claim that a non-trivial discrete distinction on the Boolean two-point floor already forces a recognition witness and a recognition structure. Anyone citing the T−1–T8 inevitability chain uses this as the recognition step after ledger forcing. The declaration is a Prop-structure (field bundle), not a proved inhabitant; bridges later discharge its fields from T2/T3.
Claim. T4 holds when: (i) the Boolean carrier with marked state $\mathrm{true}$ and the standard Boolean recognition-work cost is a normalized two-point recognition floor (one empty/consistent point, one marked point, unit-normalized cost, equivalence to $\mathrm{Bool}$); (ii) there exist distinct Booleans; (iii) a recognition witness $\mathrm{Recognize}(\mathrm{Bool},\mathrm{Bool})$ is nonempty; (iv) some recognition structure has universe $\mathrm{Bool}$; (v) zero cost on the consistent point implies such a witness.
background
The Unified Forcing Chain module argues that T0–T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration), starting from an absolute floor. In that ladder, T4 is the recognition step: after discreteness (T2) and ledger symmetry (T3), recognition itself is forced rather than postulated.
A normalized two-point recognition floor is the abstract Boolean floor: one empty/consistent configuration, one marked inconsistent point, a unit-normalized recognition-work cost, and an equivalence showing $\mathrm{Bool}$ is only the canonical representative. The Boolean recognition cost carried from T−1/T0 is the concrete cost on that carrier. Recognition structures and $\mathrm{Recognize}$ witnesses are the minimal relational data that turn a discrete distinction into a recognition relation.
Upstream ledger and cost machinery (balanced Boolean ledger, cost-from-distinction) supply the zero-cost consistency side; the floor distinction is the non-singleton discrete seed already present at the absolute floor.
proof idea
No proof body: this is a structure definition bundling five propositions that together mean “recognition is forced.” Inhabitants are built elsewhere. Downstream, the T2–T3→T4 bridge fills distinction from T2 discreteness and zero-cost balance from T3 ledger symmetry, then certifies a balanced-floor recognition witness. The bridge helper that realizes T4→T5 simply projects the floor recognition and distinction fields and attaches floor/positive-ratio realizations. Treat this declaration as the interface type for those bridges, not as a tactic script.
why it matters
In the primer chain, T4 is the link “Recognition ← Ledger + observables,” sitting between T3 (ledger from $J(x)=J(1/x)$ cost symmetry) and T5 (unique $J$). The complete forcing-chain records and the T−1→T8 bridge re-export this structure so later steps can assume a recognition witness on the Boolean floor.
Downstream uses include CompleteForcingChain, CompleteForcingChainT8, the T2–T3→T4 bridge, and the T4→T5 realization/cost bridges. Honesty notes on the T4→T5 arrow warn that T5 uniqueness is proved from cost-uniqueness and logic-forces-$J$ lemmas and does not consume the floor cost as an essential hypothesis; T4 still supplies the recognition-realization surface the narrative chain needs before stating unique $J$, $\varphi$, eight-tick, and $D=3$.
The doc-comment keeps richer observable/$J$-stability as an analytic refinement, so this T4 is the pre-analytic forcing claim only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.