Encyclopedia Foundation Foundation Ledger Composition To Jcost Ledger Composition Certificate
ARTICLE 4 claims 4 theorems
Foundation Ledger Composition To Jcost Ledger Composition Certificate
A machine-checked proof that the recognition cost's composition law is not an assumption but a forced consequence of ledger posting.
The certificate
The ledger, a discrete record of recognition events, forces the shape of the recognition cost. The declaration ledgerCompositionCertificate is a machine-checked collection of formal theorems that closes a specific gap: earlier work had assumed the cost obeys a composition law, but the certificate derives it from the ledger's own posting rules.
The composition law in question is the equation F(x·y) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y). The certificate proves this law is exactly the statement that the cost composes through a particular binary operation called the RCL combiner, where rclCombiner(u,v) = 2uv + 2u + 2v. This is a pure rearrangement, not a new assumption.
The certificate then proves that if a cost composes through any combiner P, and P satisfies primitive ledger posting with directional regularity, then P must equal the RCL combiner. This means the composition law is forced, not chosen. Feeding this into the earlier theorem law_of_logic_forces_jcost, the certificate concludes that any reciprocal, normalized, calibrated, and continuous cost that composes through such a ledger-posting combiner must equal J(x) = ½(x + x⁻¹) − 1.
The certificate also proves non-vacuity: the cost J itself composes through the RCL combiner, so J is a genuine fixed point of the entire setup. The construction is consistent, not empty.
What the certificate does not claim is that the cost's bare composability is derived. The existence of some combiner P through which F composes, written CostComposesThrough F P, remains an input hypothesis. The certificate isolates this residual cleanly: the "combiner is RCL" half is now a theorem, but the "some combiner exists" half is not. That is the remaining open step.
THEOREM satisfiesCompositionLaw_iff_rclCombiner · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **The composition law is the RCL combiner law on costs.** `F` satisfies the
recognition composition law iff its symmetric two-point combination
`F (x·y) + F (x/y)` equals `rclCombiner (F x) (F y)`. This is a pure
rearrangement: `rclCombiner u v = 2uv + 2u + 2v` is the composition-law RHS with
`u = F x`, `v = F y`. -/
theorem satisfiesCompositionLaw_iff_rclCombiner (F : ℝ → ℝ) :
SatisfiesCompositionLaw F ↔
∀ x y : ℝ, 0 < x → 0 < y →
F (x * y) + F (x / y) = rclCombiner (F x) (F y) := by
unfold SatisfiesCompositionLaw rclCombiner
constructor
· intro h x y hx hy; rw [h x y hx hy]
· intro h x y hx hy; rw [h x y hx hy]
THEOREM satisfiesCompositionLaw_of_ledgerComposes · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **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]
THEOREM ledgerComposition_forces_jcost · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **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
THEOREM jcost_composesThrough_rclCombiner · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **`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
What this page does not claim
The bare composability of the cost, CostComposesThrough F P, is not derived and remains an input hypothesis. The certificate does not prove that every cost satisfies the composition law; it proves the law is forced when composability and ledger posting hold. No claim is made about the physical interpretation of the ledger or the 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:
- What exactly is primitive ledger posting, and why does directional regularity select the RCL combiner?
- Under what conditions does a cost compose through some combiner at all?
- How does the RCL combiner relate to the physical interpretation of recognition events?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM satisfiesCompositionLaw_iff_rclCombiner · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **The composition law is the RCL combiner law on costs.** `F` satisfies the recognition composition law iff its symmetric two-point combination `F (x·y) + F (x/y)` equals `rclCombiner (F x) (F y)`. This is a pure rearrangement: `rclCombiner u v = 2uv + 2u + 2v` is the composition-law RHS with `u = F x`, `v = F y`. -/ theorem satisfiesCompositionLaw_iff_rclCombiner (F : ℝ → ℝ) : SatisfiesCompositionLaw F ↔ ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = rclCombiner (F x) (F y) := by unfold SatisfiesCompositionLaw rclCombiner constructor · intro h x y hx hy; rw [h x y hx hy] · intro h x y hx hy; rw [h x y hx hy]The composition law is exactly the statement that the cost composes through the RCL combiner. satisfiesCompositionLaw_iff_rclCombiner · IndisputableMonolith/Foundation/LedgerCompositionToJCost.leanTHEOREM satisfiesCompositionLaw_of_ledgerComposes · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **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]If a cost composes through a combiner P, and P satisfies primitive ledger posting with directional regularity, then P must equal the RCL combiner. satisfiesCompositionLaw_of_ledgerComposes · IndisputableMonolith/Foundation/LedgerCompositionToJCost.leanTHEOREM ledgerComposition_forces_jcost · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **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 hContAny reciprocal, normalized, calibrated, and continuous cost that composes through a ledger-posting combiner must equal J(x) = ½(x + x⁻¹) − 1. ledgerComposition_forces_jcost · IndisputableMonolith/Foundation/LedgerCompositionToJCost.leanTHEOREM jcost_composesThrough_rclCombiner · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean
/-- **`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 ringThe cost J itself composes through the RCL combiner. jcost_composesThrough_rclCombiner · IndisputableMonolith/Foundation/LedgerCompositionToJCost.lean