Foundation Ledger To Factorization Free Ledger Combiner Semantics From Primitive

The bridge from ledger to factorization

A ledger, a discrete record of recognition events, needs a rule for how two postings combine. The framework's machine-checked library of formal theorems proves that a very simple rule, called primitive posting, is enough to reach the full combiner. The declaration freeLedgerCombinerSemantics_from_primitiveLedgerPosting states this bridge: if a two-variable combiner obeys primitive posting semantics and is continuous in its second argument, then it automatically satisfies the stronger free-ledger combiner semantics.

Primitive posting semantics is a minimal set of conditions. It requires symmetry, zero cost at the unit, a composition law, and a boundary condition. The theorem adds one regularity condition: continuity in the second argument. Under those assumptions, the combiner is forced to be linear in its second argument, which is exactly what the free-ledger semantics demands. The proof is a chain of implications: primitive posting gives discrete posting, which forces an affine response on natural numbers, and continuity extends that to all real numbers.

The result matters because it closes a gap in the framework's derivation. The factorization step, which produces the RCL polynomial, needs a combiner with a right-affine response. The theorem shows that this response is not an extra assumption; it follows from the primitive posting rule plus continuity. The library proves this in a machine-checked way, so the implication is airtight within the framework's axioms.

What the theorem does not claim is just as important. It does not say that primitive posting alone, without continuity, forces the combiner. It does not say that the combiner is unique; other combiners could satisfy the same conditions if continuity fails. It also does not claim that the primitive posting rule is the only way to reach the free-ledger semantics; the library shows other routes, such as monotonicity or nonnegativity, also work.

The practical consequence is that the framework's Phase 3 bridge, from the recognition ledger to the factorization gate, rests on a single, checkable condition. A reader who accepts primitive posting and continuity can accept the free-ledger combiner, and from there the factorization polynomial follows. The theorem turns a suspected gap into a proved implication, and it does so with the precision that only a machine-checked proof can offer.

/-- Primitive ledger posting plus continuity gives the completed free-ledger
posting semantics.  The additive response law is no longer a separate
assumption: realize arbitrary real postings `v` and `w` as the costs of two
primitive defects in a two-generator ledger. -/
theorem freeLedgerCombinerSemantics_from_primitiveLedgerPosting
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hcont : ∀ u, Continuous fun v => P u v) :
    FreeLedgerCombinerSemantics P := by
  refine {
    symmetric := h.symmetric
    zeroBoundary := h.zeroBoundary
    unitDiagonal := h.unitDiagonal
    rightPostedAdditive := ?_
    rightContinuous := hcont
    free_ledger_additivity := h.free_ledger_additivity
  }
  exact primitiveLedgerPosting_forces_rightPostedAdditive P h

/-- Primitive ledger posting specializes to the natural-number rank-one ledger
surface. -/
theorem discreteLedgerPosting_from_primitiveLedgerPosting
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P) :
    DiscreteLedgerPostingSemantics P := by
  refine {
    symmetric := h.symmetric
    zeroBoundary := h.zeroBoundary
    unitDiagonal := h.unitDiagonal
    rightNatPostedAdditive := ?_
    free_ledger_additivity := h.free_ledger_additivity
  }
  intro u m n
  let Γ : RecognitionLedgerFloor.DefectLedger Unit := Finsupp.single () m
  let Δ : RecognitionLedgerFloor.DefectLedger Unit := Finsupp.single () n
  have hpost := h.rightLedgerPostedAdditive u Unit (fun _ : Unit => (1 : ℝ)) Γ Δ
  have hΓ :
      RecognitionLedgerFloor.ledgerCost (fun _ : Unit => (1 : ℝ)) Γ = (m : ℝ) := by
    simpa [Γ] using RecognitionLedgerFloor.unit_cost_is_generator_count (I := Unit) () m
  have hΔ :
      RecognitionLedgerFloor.ledgerCost (fun _ : Unit => (1 : ℝ)) Δ = (n : ℝ) := by
    simpa [Δ] using RecognitionLedgerFloor.unit_cost_is_generator_count (I := Unit) () n
  have hsum :
      RecognitionLedgerFloor.ledgerCost (fun _ : Unit => (1 : ℝ)) (Γ + Δ) =
        ((m + n : ℕ) : ℝ) := by
    rw [RecognitionLedgerFloor.ledgerCost_add, hΓ, hΔ]
    norm_num
  simpa [hΓ, hΔ, hsum] using hpost

/-- Primitive ledger posting already forces affine response on the actual
natural-number rank-one ledger-cost surface. -/
theorem primitiveLedgerPosting_forces_natAffineResponse
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P) :
    ∀ u (n : ℕ),
      P u (n : ℝ) = (P u 1 - P u 0) * (n : ℝ) + P u 0 :=
  discreteLedgerPosting_forces_natAffineResponse P
    (discreteLedgerPosting_from_primitiveLedgerPosting P h)

/-- Primitive ledger posting plus continuity forces completed real
ledger-linear response. -/
theorem ledgerLinearResponse_from_primitiveLedgerPosting
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hcont : ∀ u, Continuous fun v => P u v) :
    LedgerLinearResponse P :=
  ledgerLinearResponse_from_free_ledger P
    (freeLedgerCombinerSemantics_from_primitiveLedgerPosting P h hcont)

/-- Ledger-linear response supplies the `rightAffine` field of the
factorization gate. -/
theorem rightAffine_of_ledgerLinearResponse
    (P : ℝ → ℝ → ℝ) (h : LedgerLinearResponse P) :
    ∀ u, ∃ α β, ∀ v, P u v = α * v + β := by
  intro u
  exact ⟨P u 1 - P u 0, P u 0, h.rightResponse u⟩

What this page does not claim

Primitive posting alone, without continuity, forces the free-ledger combiner. The combiner is unique under these conditions; other combiners may exist if continuity fails. The primitive posting rule is the only way to reach the free-ledger semantics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LedgerToFactorization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: