T3_Ledger_Forced
plain-language theorem explainer
T3 packages the additive ledger law on the Boolean recognition floor: empty is zero-cost and join-neutral, and independent joins add costs. Anyone citing the T−1…T8 forcing spine uses this as the bookkeeping interface between discreteness (T2) and recognition witnesses (T4). It is a Prop-structure definition, not a proved theorem; instances are supplied by the T0/T2→T3 bridge.
Claim. The ledger-forced predicate on the Boolean floor asserts four laws for the unit recognition cost $C$ (with $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$): (i) $C(\mathsf{false})=0$; (ii) joining the empty configuration on the left is identity, $\mathsf{false}\mathbin{*}\Gamma=\Gamma$; (iii) that join is cost-neutral, $C(\mathsf{false}\mathbin{*}\Gamma)=C(\Gamma)$; (iv) if $\Gamma_1$ and $\Gamma_2$ are independent then $C(\Gamma_1\mathbin{*}\Gamma_2)=C(\Gamma_1)+C(\Gamma_2)$.
background
The public T−1…T8 spine (this module) exposes theory-only forcing steps from an absolute distinguishability floor through D=3. T3 is the additive ledger bookkeeping layer: after T2 has forced two-state discreteness of the Boolean floor, recognition work must be tracked by a monoidal cost that treats the empty consistent entry as neutral and adds on independent joins.
A configuration space supplies empty emp, binary join, consistency, and an independence relation (no shared predicates), with join a commutative monoid. On Bool, the concrete recognition-work cost is $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$. Independence here is the ConfigSpace relation, not the MaximalForcing claim-independence predicate.
Upstream, T0 supplies recognition-work structure and T2 the floor split (every state is false or true, zero cost selects consistency, positive cost selects the marked state). The UnifiedForcingChain twin states the same T3 content: empty consistent entry neutral, independent joins add costs; the reciprocal scalar ledger is a later analytic refinement.
proof idea
No proof body: this is a bare structure … : Prop bundling four fields. Inhabitants are constructed elsewhere, chiefly by the T0/T2→T3 bridge, which takes empty-join neutrality from the Boolean ConfigSpace interface and additivity from T0 recognition-work, then packages them into these fields. Downstream, t2_t3_to_t4_bridge_holds simply projects empty_balanced and feeds it to the balanced-floor recognition certificate.
why it matters
T3 is the ledger step in the forcing chain (primer T0–T8): it turns the discrete two-point floor into additive bookkeeping of recognition work, the pre-analytic substrate before T5’s unique reciprocal cost $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law.
It is consumed by T0_T2_To_T3_Bridge (ledger forced from T0 additivity plus T2 floor split), T2_T3_To_T4_Bridge / t2_t3_to_t4_bridge_holds (balanced ledger and floor recognition cert from empty_balanced), and the complete spines CompleteForcingChainT8 and CompleteForcingChain. Without T3, the T4 recognition-witness step has no balanced zero-cost entry to certify.
Note the honesty audit on the complete chain: T5 uniqueness is proved from CostUniqueness and the law-of-logic→Jcost path and does not logically depend on T−1…T4; T3 still matters for the ledger and T4 layers of the public spine, not as a hidden hypothesis inside J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.