IndisputableMonolith.Foundation.LedgerToFactorization
Bridges the free recognition ledger floor to the D'Alembert factorization gate: monotone additive real responses are linear, and primitive or discrete ledger posting forces affine combiner semantics. Anyone closing Phase 3 from ledger composition to the J-cost law cites this layer. Order-regularity replaces the usual continuity gate; posting axioms lift through free, discrete, and rational layers into the factorization algebra.
claimMonotone additive $f:\mathbb{R}\to\mathbb{R}$ are linear (order-regular Cauchy). Primitive ledger posting forces right-posted additivity and free combiner semantics; discrete posting yields a natural affine response on $\mathbb{N}$, feeding the factorization gate that makes the combiner affine in its second argument.
background
Recognition Science builds the cost $J$ from a free additive ledger floor rather than assuming the composition law. The Recognition Ledger Floor module closes the two genuine T-1/T0 audit gaps: a free additive cost floor and the dual structure needed so that posting is not smuggled in as a continuity hypothesis.
FactorizationForcing supplies the algebraic core of the B2 program: once factorization plus three-way compatibility give that the combiner is affine in its second argument, the rest of the forcing is pure algebra. The hard analytic step is exactly that affine response.
This module sits between those two. It treats ledger posting (primitive, free, discrete, rational) as the source of additivity and monotonicity, then converts those into the linear or affine maps the factorization gate consumes. The DOC note on monotone additive responses is the order-regularity replacement for the classical continuity gate in the additive Cauchy equation.
proof idea
The module is a short forcing ladder, not a single theorem.
First, pure real analysis: monotone (or antitone) additive maps $\mathbb{R}\to\mathbb{R}$ are linear; nonnegativity on the nonnegative ray upgrades additivity to monotonicity. That discharges the continuity gate by order regularity.
Next, semantic layers: PrimitiveLedgerPostingSemantics forces right-posted additivity; free combiner semantics is recovered from the primitive posting axioms; discrete posting is the specialization to $\mathbb{N}$; rational posting sits above discrete. The key bridge lemma is that discrete posting forces a natural affine response, which is exactly the input FactorizationForcing needs for the combiner to be affine in its second argument.
No single master theorem: each step is a short implication from posting axioms to the next semantic interface.
why it matters in Recognition Science
Phase 3 endpoint LedgerCompositionToJCost imports this module to close a structural gap: law_of_logic_forces_jcost existed, but its composition-law hypothesis was assumed rather than derived from the recognition ledger. Downstream doc: this layer makes the composition law a consequence of ledger posting plus factorization, not an extra axiom.
In the broader chain, that supplies the Recognition Composition Law (RCL) input that forces $J(x)=(x+x^{-1})/2-1$ (T5 J-uniqueness) and the self-similar fixed point $\varphi$ (T6). Without the monotone-additive-to-linear step and the discrete-to-affine posting bridge, the ledger floor and the factorization gate remain disconnected, and the J-cost law stays conditional.
Parent consumer is Foundation.LedgerCompositionToJCost; upstream suppliers are RecognitionLedgerFloor and DAlembert.FactorizationForcing.
scope and limits
- Does not prove the full J-cost uniqueness theorem; only the ledger-to-affine bridge.
- Does not derive factorization or three-way compatibility; those live in FactorizationForcing.
- Does not close T5–T8; it only feeds the composition-law hypothesis for Phase 3.
- Does not claim continuity-based Cauchy solutions; it uses order regularity instead.
- Does not treat non-monotone pathological additive maps (Hamel bases).
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