phiVec_post_debit
The lemma shows that a debit post at account k increments exactly one coordinate of the phi-vector by 1 while leaving all others fixed. Ledger-modeling work in recognition dynamics cites it to track atomic updates before invoking parity-adjacency results. The proof splits on whether the queried index matches k, then simplifies the post and phiVec definitions with arithmetic normalization.
claimLet $d$ be a natural number and let $L$ be a ledger state on $d$ accounts. For indices $k,i$ in the finite set of size $d$, the phi-vector after a debit post at account $k$ satisfies $phi_i(post(L,k,debit)) = phi_i(L) + 1$ if $i=k$ and $phi_i(L)$ otherwise, where $phi$ extracts the net recognition value per account from the underlying Recognition.Ledger structure.
background
The module equips a $d$-account ledger with explicit debit/credit vectors and atomic posting operations. LedgerState $d$ is the abbreviation Recognition.Ledger (AccountRS $d$), where AccountRS $d$ carries the finite set Fin $d$ together with the trivial recognition relation. phiVec is the abbreviation Recognition.phi, returning a map Fin $d$ to integers that records the net value (debit minus credit) at each account. The post function, when applied with Side.debit, increments the debit entry at the chosen account $k$ by one while leaving credit unchanged.
proof idea
The tactic proof opens with by_cases on the equality $i = k$. The equal case substitutes the hypothesis, then applies simp on the definitions of post, phiVec and Recognition.phi followed by ring_nf to clear the arithmetic. The unequal case applies simp directly, using the inequality hypothesis to select the unchanged branch of the if-expression inside post.
why it matters in Recognition Science
The result is invoked inside phiVec_coordAtomicStep_of_post to establish that any single post (debit or credit) produces a one-coordinate atomic step in the phi-vector. It supplies the debit half of the explicit posting model that converts the abstract ledger into the concrete adjacency data required by LedgerParityAdjacency. Within the Recognition framework the lemma therefore closes the local update rule needed before the eight-tick octave and phi-ladder constructions can be applied to ledger states.
scope and limits
- Does not treat the credit posting case.
- Does not establish any global conservation law beyond the single-coordinate change.
- Does not derive the posting model from a deeper variational principle.
- Does not compose multiple posts or address tick sequences.
Lean usage
have h : phiVec (post L k Side.debit) i = if i = k then phiVec L i + 1 else phiVec L i := phiVec_post_debit L k iformal statement (Lean)
84@[simp] lemma phiVec_post_debit {d : Nat} (L : LedgerState d) (k : Fin d) (i : Fin d) :
85 phiVec (d := d) (post L k Side.debit) i =
proof body
Tactic-mode proof.
86 (if i = k then phiVec (d := d) L i + 1 else phiVec (d := d) L i) := by
87 by_cases hik : i = k
88 · subst hik
89 simp [post, phiVec, Recognition.phi]
90 ring_nf
91 · simp [post, phiVec, Recognition.phi, hik]
92