Encyclopedia Foundation Foundation Ledger To Factorization Free Ledger Combiner Semantics Iff Ledger Lin

ARTICLE 3 claims 3 theorems

Foundation Ledger To Factorization Free Ledger Combiner Semantics Iff Ledger Lin

A machine-checked proof shows that two seemingly different descriptions of how a recognition ledger combines events are actually the same condition.

Verify this page

The equivalence

A ledger, in the Recognition Science framework, is a discrete record of recognition events. The framework asks how two such records combine. One way to describe a combiner is by its free semantics: it obeys a small set of structural rules about how postings add and how the unit behaves. Another way is by its linear response: in its second argument, the combiner behaves like a straight line, so that the effect of posting two amounts equals the sum of the effects of posting each separately.

The declaration freeLedgerCombinerSemantics_iff_ledgerLinearResponse proves that these two descriptions are equivalent. If a combiner satisfies the free semantics, then it necessarily has a linear response in its second argument. Conversely, if a combiner has a linear response, then it satisfies the free semantics. The proof is machine-checked in the framework's library of formal theorems, meaning the equivalence is not a heuristic or a numerical coincidence but a derived logical fact.

This equivalence matters because it connects two levels of description. The free semantics is a set of axioms about how a combiner should behave in the abstract. The linear response is a concrete property that can be checked directly. The theorem says that these are the same thing: there is no gap between the abstract rules and the concrete behavior. This is the bridge that lets the framework move from the ledger to the factorization gate, which is the next step in the forcing chain that leads to the cost function.

What the theorem does not claim is that every combiner has a linear response. It only says that if a combiner satisfies the free semantics, then it does. Nor does it claim that the linear response property alone is enough to force the full cost function; that requires additional conditions such as symmetry and the boundary law. The equivalence is a precise, conditional statement, not a universal law.

THEOREM freeLedgerCombinerSemantics_iff_ledgerLinearResponse · IndisputableMonolith/Foundation/LedgerToFactorization.lean
freeLedgerCombinerSemantics_iff_ledgerLinearResponse · IndisputableMonolith/Foundation/LedgerToFactorization.lean:587 
/-- Completed ledger-linear response is exactly free-ledger posting semantics
plus continuity. -/
theorem freeLedgerCombinerSemantics_iff_ledgerLinearResponse (P : ℝ → ℝ → ℝ) :
    FreeLedgerCombinerSemantics P ↔ LedgerLinearResponse P := by
  constructor
  · exact ledgerLinearResponse_from_free_ledger P
  · intro h
    refine {
      symmetric := h.symmetric
      zeroBoundary := h.zeroBoundary
      unitDiagonal := h.unitDiagonal
      rightPostedAdditive := ?_
      rightContinuous := ?_
      free_ledger_additivity := h.free_ledger_additivity
    }
    · intro u v w
      rw [h.rightResponse u (v + w), h.rightResponse u v, h.rightResponse u w]
      ring
    · intro u
      have hfun :
          (fun v => P u v) =
            fun v => (P u 1 - P u 0) * v + P u 0 := by
        funext v
        exact h.rightResponse u v
      rw [hfun]
      exact (continuous_const.mul continuous_id).add continuous_const
THEOREM ledgerLinearResponse_from_free_ledger · IndisputableMonolith/Foundation/LedgerToFactorization.lean
ledgerLinearResponse_from_free_ledger · IndisputableMonolith/Foundation/LedgerToFactorization.lean:444 
/-- Continuous additive posting response is linear over `ℝ`, so free-ledger
semantics supplies the exact `LedgerLinearResponse` bridge. -/
theorem ledgerLinearResponse_from_free_ledger
    (P : ℝ → ℝ → ℝ) (h : FreeLedgerCombinerSemantics P) :
    LedgerLinearResponse P := by
  refine {
    symmetric := h.symmetric
    zeroBoundary := h.zeroBoundary
    unitDiagonal := h.unitDiagonal
    rightResponse := ?_
    free_ledger_additivity := h.free_ledger_additivity
  }
  intro u v
  let response : ℝ →+ ℝ := {
    toFun := fun t => P u t - P u 0
    map_zero' := by ring
    map_add' := by
      intro a b
      exact h.rightPostedAdditive u a b
  }
  have hresponse_cont : Continuous response := by
    change Continuous fun t => P u t - P u 0
    exact (h.rightContinuous u).sub continuous_const
  let linearResponse : ℝ →L[ℝ] ℝ :=
    AddMonoidHom.toRealLinearMap response hresponse_cont
  have hlinear :
      response v = v * response 1 := by
    have hsmul := linearResponse.map_smul v 1
    change response (v * 1) = v * response 1 at hsmul
    simpa using hsmul
  change P u v = (P u 1 - P u 0) * v + P u 0
  have hcomm : v * (P u 1 - P u 0) = (P u 1 - P u 0) * v := by ring
  have hsub : P u v - P u 0 = (P u 1 - P u 0) * v := by
    simpa [response, hcomm] using hlinear
  linarith
THEOREM freeLedgerCombinerSemantics_iff_ledgerLinearResponse · IndisputableMonolith/Foundation/LedgerToFactorization.lean
freeLedgerCombinerSemantics_iff_ledgerLinearResponse · IndisputableMonolith/Foundation/LedgerToFactorization.lean:587 
/-- Completed ledger-linear response is exactly free-ledger posting semantics
plus continuity. -/
theorem freeLedgerCombinerSemantics_iff_ledgerLinearResponse (P : ℝ → ℝ → ℝ) :
    FreeLedgerCombinerSemantics P ↔ LedgerLinearResponse P := by
  constructor
  · exact ledgerLinearResponse_from_free_ledger P
  · intro h
    refine {
      symmetric := h.symmetric
      zeroBoundary := h.zeroBoundary
      unitDiagonal := h.unitDiagonal
      rightPostedAdditive := ?_
      rightContinuous := ?_
      free_ledger_additivity := h.free_ledger_additivity
    }
    · intro u v w
      rw [h.rightResponse u (v + w), h.rightResponse u v, h.rightResponse u w]
      ring
    · intro u
      have hfun :
          (fun v => P u v) =
            fun v => (P u 1 - P u 0) * v + P u 0 := by
        funext v
        exact h.rightResponse u v
      rw [hfun]
      exact (continuous_const.mul continuous_id).add continuous_const

What this page does not claim

This theorem does not claim that every combiner has a linear response. This theorem does not claim that linear response alone forces the full cost function. This theorem does not claim that the free semantics is the only way to characterize a combiner.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND