IndisputableMonolith.Foundation.LedgerToFactorization
Bridge from the free recognition ledger floor to the factorization gate of B2 closure. Monotone (and antitone) additive real maps are linear, replacing continuity in the additive Cauchy step; ledger posting is packaged as primitive, free, discrete, and rational combiner semantics that force affine linear response. Downstream composition-to-J work imports this bridge. The module is a chain of classical regularity lemmas plus semantic embeddings.
claimMonotone additive maps $f:\mathbb{R}\to\mathbb{R}$ are $\mathbb{R}$-linear (likewise antitone). Primitive, free, discrete, and rational ledger-posting semantics force an affine linear response of the combiner in its second argument, connecting the recognition ledger floor to factorization forcing.
background
RecognitionLedgerFloor supplies the free additive cost floor that closes the two genuine T-1/T0 audit gaps (the Anil critique), rather than restating two-state minimality. FactorizationForcing is the algebraic core of the B2 program: once factorization plus three-way compatibility yield that the combiner is affine in its second argument, the remaining forcing is pure algebra.
This module sits between those layers. It treats order regularity as a stand-in for the usual continuity gate on additive Cauchy solutions over the reals, then defines ledger posting at several structure levels (primitive postings, free combiners, discrete and rational refinements) so that the ledger's additive bookkeeping becomes the linear response the factorization gate consumes.
Sibling content centers on LedgerLinearResponse and the forcing arrows from primitive posting to right-posted additivity, free combiner semantics, and natural affine response.
proof idea
Classical regularity first: monotone additive real maps are linear; antitone additive maps are linear; additive maps nonnegative on the nonnegative reals are monotone. Those lemmas replace a continuity hypothesis in the additive Cauchy step.
Semantic ladder next: PrimitiveLedgerPostingSemantics is the base posting interface; freeLedgerCombinerSemantics_from_primitiveLedgerPosting lifts it to FreeLedgerCombinerSemantics; discrete and rational posting semantics refine the same story. Forcing theorems show primitive posting forces right-posted additivity, and discrete posting forces a natural affine response (LedgerLinearResponse). The module is therefore regularity lemmas plus a chain of semantic embeddings into the factorization setting.
why it matters in Recognition Science
Direct parent is LedgerCompositionToJCost (Phase 3 endpoint). That module exists because law_of_logic_forces_jcost previously assumed SatisfiesCompositionLaw F rather than deriving it from the recognition ledger; it closes the gap structurally so ledger composition forces the recognition cost $J$.
Without the linear-response bridge here, FactorizationForcing cannot attach to RecognitionLedgerFloor, and the composition law (RCL) never becomes a theorem about actual ledger postings. In the broader forcing chain this is infrastructure toward T5 J-uniqueness, $J(x)=(x+x^{-1})/2-1$, not a substitute for it. It is the order-regular path from additive ledger bookkeeping to the affine combiner the B2 algebra needs.
scope and limits
- Does not derive the recognition cost $J$ or the full composition law RCL.
- Does not prove J-uniqueness (T5) or fix $\varphi$ (T6).
- Does not treat continuity-based Cauchy solutions beyond order regularity.
- Does not force eight-tick structure, $D=3$, or coupling constants.
- Does not close mass-ladder or $\alpha$-band claims.
used by (1)
depends on (2)
declarations in this module (46)
-
theorem
monotone_additive_isLinear -
theorem
antitone_additive_isLinear -
theorem
additive_nonnegOnNonneg_isMonotone -
structure
LedgerLinearResponse -
structure
FreeLedgerCombinerSemantics -
structure
PrimitiveLedgerPostingSemantics -
theorem
primitiveLedgerPosting_forces_rightPostedAdditive -
theorem
freeLedgerCombinerSemantics_from_primitiveLedgerPosting -
structure
DiscreteLedgerPostingSemantics -
theorem
discreteLedgerPosting_from_primitiveLedgerPosting -
structure
RationalLedgerPostingSemantics -
theorem
discreteLedgerPosting_forces_natAffineResponse -
theorem
primitiveLedgerPosting_forces_natAffineResponse -
theorem
rclCombiner_discreteLedgerPostingSemantics -
theorem
rclCombiner_primitiveLedgerPostingSemantics -
theorem
ledgerLinearResponse_from_rationalLedgerPosting -
theorem
rclCombiner_rationalLedgerPostingSemantics -
theorem
rationalLedgerPosting_iff_ledgerLinearResponse -
theorem
ledgerLinearResponse_from_free_ledger -
theorem
ledgerLinearResponse_from_primitiveLedgerPosting -
theorem
ledgerLinearResponse_from_primitiveLedgerPosting_monotone -
theorem
ledgerLinearResponse_from_primitiveLedgerPosting_nonneg -
theorem
ledgerLinearResponse_from_primitiveLedgerPosting_directional -
theorem
freeLedgerCombinerSemantics_iff_ledgerLinearResponse -
theorem
rightAffine_of_ledgerLinearResponse -
theorem
factorizationGate_of_ledgerLinearResponse -
theorem
ledgerLinearResponse_forces_rcl -
theorem
factorizationGate_of_primitiveLedgerPosting -
theorem
primitiveLedgerPosting_forces_rcl -
theorem
factorizationGate_of_primitiveLedgerPosting_monotone -
theorem
primitiveLedgerPosting_monotone_forces_rcl -
theorem
factorizationGate_of_primitiveLedgerPosting_nonneg -
theorem
primitiveLedgerPosting_nonneg_forces_rcl -
theorem
factorizationGate_of_primitiveLedgerPosting_directional -
theorem
primitiveLedgerPosting_directional_forces_rcl -
theorem
ledgerCost_le_add_right -
theorem
rclCombiner_postingNonneg -
theorem
rclCombiner_directional -
theorem
rclCombiner_ledgerLinearResponse -
theorem
rclCombiner_freeLedgerSemantics -
theorem
ledgerLinearResponse_iff_rcl -
theorem
factorizationGate_of_rationalLedgerPosting -
theorem
rationalLedgerPosting_forces_rcl -
theorem
rationalLedgerPosting_iff_rcl -
theorem
freeLedgerCombinerSemantics_iff_rationalLedgerPosting -
theorem
freeLedgerCombinerSemantics_iff_rcl