T3_Ledger_Forced
plain-language theorem explainer
T3 packages the pre-analytic ledger as four Boolean-floor laws: empty entry has zero recognition cost, empty join is a monoid unit, that unit is cost-neutral, and independent joins add costs. Forcing-chain authors cite it when stepping from T2 discreteness into T4 recognition and the complete T0–T8 record. It is a Prop-structure interface (definitional claim bundle), not a proved theorem with a body.
Claim. The ledger is forced on the Boolean floor when the recognition cost $C$ satisfies: $C(\mathsf{false})=0$; joining the empty configuration is a left identity on floor states; that identity is cost-neutral; and whenever configurations $\Gamma_1,\Gamma_2$ are independent, $C(\mathrm{join}(\Gamma_1,\Gamma_2))=C(\Gamma_1)+C(\Gamma_2)$.
background
In the Unified Forcing Chain, every level T−1 through T8 is claimed as a cost-forced inevitability from the Recognition Composition Law plus normalization and calibration. The module ladder places T3 after T0 (logic from cost) and T2 (discreteness): the ledger is the additive bookkeeping of recognition work at the pre-analytic floor; the reciprocal scalar ledger $J(x)=J(1/x)$ is treated as a later analytic refinement.
A configuration space supplies an empty configuration, a binary join, consistency, and an independence relation (no shared predicates), with join a commutative monoid and empty as identity. On the Boolean two-point floor the empty/false state is the neutral entry, and the Boolean recognition cost is the floor cost used by T0. Independence here means the two floor configurations may be joined without shared content, so additivity is the ledger law rather than a generic sum over events.
Upstream cost notions (J-cost of a recognition event, multiset ratio costs, multiplicative-recognizer derived cost) sit above this floor; T3 only records the discrete additive skeleton those analytic costs refine.
proof idea
No proof body: the declaration is a four-field Prop structure. Each field is a named ledger axiom on the Boolean floor cost and ConfigSpace.join.
empty_balanced fixes zero cost on the empty/false entry. empty_join_left is the monoid-unit law for join. empty_join_cost_neutral says that unit does not change cost. independent_join_additive is cost additivity under the configuration-space independence predicate.
Inhabitants are assembled elsewhere (T0 recognition-work plus the T2 floor split, via the T0–T2→T3 bridge). Downstream bridges project individual fields (e.g. empty balance into the T2–T3→T4 bridge) rather than re-proving the bundle.
why it matters
T3 is the ledger rung of the complete inevitability chain: after logic and discreteness, before recognition observables (T4), unique $J$ (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). The doc-comment states the ledger as additive bookkeeping of recognition work with neutral empty entry and additive independent joins.
It is consumed by CompleteForcingChain and CompleteForcingChainT8, by the T0–T2→T3 and T2–T3→T4 bridges, and by the theorem that builds the T2–T3→T4 bridge from a T3 witness (empty balance becomes the balanced-ledger hypothesis for floor recognition). Without this interface the chain cannot hand a balanced discrete ledger to T4.
Framework role: cost symmetry and discrete join-additivity are what later specialize to the reciprocal $J$-ledger; T3 itself stays at the Boolean floor and does not yet force the closed form of $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.