T0_To_T1_Bridge
plain-language theorem explainer
Packages the step from forced Boolean recognition-work logic (T0) to the Meta-Principle (T1): inconsistent states cannot be selected at zero cost. Anyone citing the T−1→T1 or full T0–T8 forcing certificates uses this bridge record. It is a Prop-structure whose second field pins T1 exactly to the corollary extracted from a T0 hypothesis.
Claim. Given a witness $h_0$ that logic is forced as the zero/positive split of Boolean recognition work, a T0-to-T1 bridge is a pair consisting of a T1 Meta-Principle witness (inconsistent configurations have strictly positive cost; zero-cost configurations are consistent; the marked inconsistent bit has positive cost) together with a proof that this T1 witness equals the canonical corollary of $h_0$.
background
This module isolates the first three levels of the Recognition Science forcing chain without importing the analytic $J$-cost surface. T−1 is the absolute floor of distinguishability. T0 asserts that logic is the zero/positive split of recognition work on the Boolean configuration space: the consistent state has cost zero, every inconsistent state has positive cost, and the cost is additive on independent joins.
T1 is the cost-form Meta-Principle: an inconsistent recognition-work state cannot be selected at zero cost. Concretely it records the same inconsistency-positive and zero-cost-consistent laws, plus the marked fact that the Boolean true (inconsistent) bit has positive cost. The upstream theorem t1_corollary_of_t0 shows T1 is literally a projection of T0: the two shared fields are copied, and the marked positive cost is T0's inconsistency law applied to true.
The local setting is deliberately pre-analytic: only the Boolean recognition-work split and consistency predicate appear, not the continuous $J(x)=(x+x^{-1})/2-1$ cost of later chain steps.
proof idea
No proof body: this is a Prop-valued structure definition. Its fields are (i) a T1 Meta-Principle witness and (ii) an equality asserting that witness is definitionally the output of t1_corollary_of_t0 on the supplied T0 hypothesis. The actual construction is discharged downstream by t0_to_t1_bridge_holds, which fills t1 with that corollary and closes the equality by rfl.
why it matters
This bridge is the typed hinge between T0 and T1 in the forcing chain. It is required by the compact public certificate TMinus1ToT1Cert (fields t0_to_t1 and t1) and is re-exported into CompleteForcingChainT8 and the full CompleteForcingChain (T0–T8) records. Those parents assemble the absolute floor, the T−1→T0 bridge, forced logic, this T0→T1 step, and the Meta-Principle into one certificate.
In the primer landmarks this is the opening of the T0–T8 chain: T0 forces logic as cost polarity; T1 is the Meta-Principle that inconsistent floor states are never free. Later steps (T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick octave, T8 $D=3$) sit above this pre-analytic floor. The honesty note on the T8 certificate stresses that T5 uniqueness does not consume this floor bridge beyond re-export; the present declaration only certifies the T0→T1 arrow itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.