ledgerL1Cost_post
The lemma shows that applying a single atomic post to a d-dimensional ledger state changes its L1 cost by exactly one. Ledger-model researchers cite it to confirm that posting steps realize the minimal unit cost in the Recognition framework. The proof uses case split on debit versus credit, Finset sum erasure to isolate the changed coordinate, and direct simplification to verify the other vector remains untouched.
claimLet $L$ be a ledger state with debit and credit vectors indexed by $d$ accounts. For any account index $k$ and side $s$ (debit or credit), the L1 cost of the updated state obtained by posting one unit at $k$ on side $s$ equals 1: $C_{L1}(L, post(L,k,s)) = 1$.
background
LedgerState d is the type of pairs of debit and credit vectors over Fin d, each entry an integer recording recognition events at that account. The post operation adds exactly one unit to either the debit or credit component at a chosen index k, leaving the opposite vector unchanged. ledgerL1Cost is the sum of absolute differences across all debit entries plus the same sum across all credit entries, measuring the total integer displacement between two ledger states. The module upgrades an abstract vector model to this explicit posting ledger so that parity changes become one-bit adjacency steps. Upstream LedgerState structures in VariationalDynamics and InformationIsLedger supply the conserved log-ratio and event-list interpretations that this concrete carrier refines.
proof idea
The tactic proof opens with classical and cases on side. For debit it defines an auxiliary function f for absolute debit differences, applies Finset.add_sum_erase to split the sum at k, proves f k = 1 by direct simplification of post, shows the erased sum vanishes by sum_eq_zero on the remaining indices, then reassembles to obtain debit sum = 1 and credit sum = 0. The credit case mirrors the argument with roles reversed. Both branches finish by unfolding ledgerL1Cost and substituting the two sums.
why it matters in Recognition Science
This lemma supplies the cost side of the LegalAtomicTick predicate used by legalAtomicTick_of_post, which in turn feeds minCost_monotoneStep_implies_postingStep. It therefore closes the gap between the abstract Recognition ledger and the concrete posting model required for parity one-bit adjacency. In the framework it realizes the minimal-cost atomic tick that preserves the J-cost structure while advancing the phi-ladder by a single rung, consistent with the eight-tick octave and D = 3 spatial embedding. No open scaffolding remains at this node.
scope and limits
- Does not claim that every minimal-cost step must be a single post.
- Does not extend to non-integer or continuous ledger updates.
- Does not address multi-account simultaneous postings.
- Does not derive the posting rule from an underlying variational principle.
Lean usage
refine ⟨post_monotone (d := d) L k side, ledgerL1Cost_post (d := d) L k side⟩formal statement (Lean)
687private lemma ledgerL1Cost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
688 ledgerL1Cost (d := d) L (post L k side) = 1 := by
proof body
Tactic-mode proof.
689 classical
690 cases side with
691 | debit =>
692 -- debit changes by +1 at k; credit unchanged
693 have hdebit :
694 (∑ i : Fin d, Int.natAbs ((post L k Side.debit).debit i - L.debit i)) = 1 := by
695 -- isolate `k` and show everything else is 0
696 let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.debit).debit i - L.debit i)
697 have hsplit :=
698 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
699 have fk : f k = 1 := by
700 simp [f, post]
701 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
702 refine Finset.sum_eq_zero ?_
703 intro i hi
704 have hik : i ≠ k := by
705 simpa [Finset.mem_erase] using hi
706 simp [f, post, hik]
707 -- rewrite `∑ univ` using `hsplit.symm`
708 simpa [f] using (by
709 calc
710 (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
711 simpa using hsplit.symm
712 _ = 1 := by simp [fk, hErase])
713 have hcredit :
714 (∑ i : Fin d, Int.natAbs ((post L k Side.debit).credit i - L.credit i)) = 0 := by
715 -- credit is unchanged everywhere
716 refine Finset.sum_eq_zero ?_
717 intro i _
718 simp [post]
719 -- assemble
720 simp [ledgerL1Cost, hdebit, hcredit]
721 | credit =>
722 -- credit changes by +1 at k; debit unchanged
723 have hdebit :
724 (∑ i : Fin d, Int.natAbs ((post L k Side.credit).debit i - L.debit i)) = 0 := by
725 refine Finset.sum_eq_zero ?_
726 intro i _
727 simp [post]
728 have hcredit :
729 (∑ i : Fin d, Int.natAbs ((post L k Side.credit).credit i - L.credit i)) = 1 := by
730 let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.credit).credit i - L.credit i)
731 have hsplit :=
732 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
733 have fk : f k = 1 := by
734 simp [f, post]
735 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
736 refine Finset.sum_eq_zero ?_
737 intro i hi
738 have hik : i ≠ k := by
739 simpa [Finset.mem_erase] using hi
740 simp [f, post, hik]
741 simpa [f] using (by
742 calc
743 (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
744 simpa using hsplit.symm
745 _ = 1 := by simp [fk, hErase])
746 simp [ledgerL1Cost, hdebit, hcredit]
747