Foundation Ledger Composition To Jcost Satisfies Composition Law Of Ledger Compo

The composition law

The cost function sits at the center of Recognition Science. It assigns a number to each recognition event, and the framework's central question is what form that number can take. The answer turns on a composition law: a rule for how the cost of two events combines into the cost of their product. The law is the equation F(x·y) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y), where F is the cost and x and y are positive numbers. This is not an arbitrary choice. The framework's machine-checked library of formal theorems proves that if the cost composes through a combiner that satisfies primitive ledger posting with directional regularity, then the combiner must equal this specific form, and the composition law follows.

The theorem satisfiesCompositionLaw_of_ledgerComposes states this result. It takes three inputs: a cost function F, a combiner P that pairs two costs, and the assumption that F composes through P. The combiner P must satisfy primitive ledger posting, which means it behaves like a discrete record of events, and it must have directional regularity, meaning each slice is monotone or antitone. Under these conditions, the theorem derives the composition law for F. The key move is that the combiner P is forced to equal the RCL combiner, rclCombiner(u,v) = 2uv + 2u + 2v. Once that holds, the composition law is a pure rearrangement. The theorem replaces an assumption with a derivation: the composition law is no longer an input but a consequence of the ledger structure.

The result matters because it closes a gap in the framework's chain. The main theorem law_of_logic_forces_jcost requires the composition law as a hypothesis. This result proves that hypothesis follows from the ledger-side statement that the cost composes through a ledger-posting combiner. The residual assumption is bare composability: that some combiner P exists such that F composes through it. The theorem does not prove that every cost composes through some combiner. It proves that if such a combiner exists and satisfies the ledger conditions, then the composition law holds. The framework also shows the construction is non-vacuous: the cost J(x) = (x + 1/x)/2 − 1 itself composes through the RCL combiner, so it is a genuine fixed point of the setup.

What the theorem does not claim is equally precise. It does not prove that the cost function F equals J on its own. That requires additional hypotheses: reciprocal, normalized, calibrated, and continuous on the positive ray. These combine with the composition law in the larger theorem ledgerComposition_forces_jcost to force F = J. The theorem also does not prove that the combiner P is unique. It proves that under the ledger and regularity conditions, P must equal rclCombiner. The existence of such a P is assumed, not derived. Finally, the theorem does not establish that the ledger-posting semantics themselves are the only possible structure. It shows that within the framework's definitions, the composition law is forced, not that the framework's definitions exhaust all possibilities.

/-- **Ledger posting + directional regularity force the cost's composition
law.**  If `F` composes through a combiner `P`, and `P` is a primitive
ledger-posting combiner with per-slice directional regularity, then `P` is
forced to be `rclCombiner` (Phase 3), so `F` satisfies the recognition
composition law. -/
theorem satisfiesCompositionLaw_of_ledgerComposes (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hP : PrimitiveLedgerPostingSemantics P)
    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v))
    (hCompose : CostComposesThrough F P) :
    SatisfiesCompositionLaw F := by
  have hPrcl : ∀ u v, P u v = rclCombiner u v :=
    primitiveLedgerPosting_directional_forces_rcl P hP hdir
  apply satisfiesCompositionLaw_of_composesThrough_rcl
  intro x y hx hy
  rw [hCompose x y hx hy, hPrcl]

/-- **Ledger posting + directional regularity force the cost's composition
law.**  If `F` composes through a combiner `P`, and `P` is a primitive
ledger-posting combiner with per-slice directional regularity, then `P` is
forced to be `rclCombiner` (Phase 3), so `F` satisfies the recognition
composition law. -/
theorem satisfiesCompositionLaw_of_ledgerComposes (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hP : PrimitiveLedgerPostingSemantics P)
    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v))
    (hCompose : CostComposesThrough F P) :
    SatisfiesCompositionLaw F := by
  have hPrcl : ∀ u v, P u v = rclCombiner u v :=
    primitiveLedgerPosting_directional_forces_rcl P hP hdir
  apply satisfiesCompositionLaw_of_composesThrough_rcl
  intro x y hx hy
  rw [hCompose x y hx hy, hPrcl]

/-- **`J` composes through the RCL combiner.**  The recognition cost
`J(x) = ½(x + x⁻¹) − 1` satisfies `J (x·y) + J (x/y) = rclCombiner (J x) (J y)`
for positive `x, y`.  This shows the ledger-composition setup is non-vacuous:
`J` is a fixed point of the composition law it forces. -/
theorem jcost_composesThrough_rclCombiner :
    CostComposesThrough Cost.Jcost rclCombiner := by
  intro x y hx hy
  have hx0 : x ≠ 0 := ne_of_gt hx
  have hy0 : y ≠ 0 := ne_of_gt hy
  unfold Cost.Jcost rclCombiner
  field_simp
  ring

/-- **Ledger composition forces `J`.**  If the recognition cost `F` is
reciprocal, normalized, calibrated, and continuous on the positive ray, and it
composes through a combiner `P` that satisfies primitive ledger posting with
per-slice directional regularity, then `F = J` on positives.

This is the genuine discharge of the Phase 3 "Apply `law_of_logic_forces_jcost`"
item: the previously-assumed `SatisfiesCompositionLaw F` hypothesis is replaced
by the ledger-side pair (cost composes through `P`) ∧ (`P` is a ledger-posting
combiner), and the "combiner = RCL" half is a theorem, not an assumption. -/
theorem ledgerComposition_forces_jcost
    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hRecip : IsReciprocalCost F)
    (hNorm : IsNormalized F)
    (hCalib : IsCalibrated F)
    (hCont : ContinuousOn F (Set.Ioi 0))
    (hP : PrimitiveLedgerPostingSemantics P)
    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v))
    (hCompose : CostComposesThrough F P) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  have hComp : SatisfiesCompositionLaw F :=
    satisfiesCompositionLaw_of_ledgerComposes F P hP hdir hCompose
  exact law_of_logic_forces_jcost F hRecip hNorm hComp hCalib hCont

What this page does not claim

This theorem alone does not prove F equals J; it requires reciprocal, normalized, calibrated, and continuous hypotheses. The theorem assumes the existence of a combiner P; it does not prove every cost composes through some combiner. The framework's ledger-posting semantics are not shown to be the only possible structure for a recognition cost.

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/LedgerCompositionToJCost.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: