minJlogCost_monotoneStep_implies_postingStep
plain-language theorem explainer
If a monotone ledger transition from L to L' minimizes the Jlog cost among all monotone transitions from L, then the transition must be a single atomic posting of one unit to one account. Researchers modeling recognition events via ledger states and parity adjacency would cite this to reduce general monotone steps to unit posts. The proof picks a concrete single-post candidate at the first account, verifies its cost equals Jlog(1), applies the minimality hypothesis to bound the given cost by Jlog(1), and invokes the prior lemma that any such b-
Claim. Let $d$ be a positive integer. For ledger states $L,L'$ over $d$ accounts, suppose the transition is monotone (every debit and credit count is non-decreasing), $L$ is distinct from $L'$, and $L'$ attains the minimal ledger Jlog cost among all monotone transitions from $L$. Then there exist an account index $k$ and a side (debit or credit) such that $L'$ is obtained from $L$ by posting one unit on that side at account $k$.
background
LedgerState $d$ is the type Recognition.Ledger (AccountRS $d$), a pair of debit and credit vectors indexed by Fin $d$. MonotoneLedger $L$ $L'$ requires that every debit and credit entry of $L$ is at most the corresponding entry of $L'$. PostingStep $L$ $L'$ asserts that $L'$ equals post $L$ $k$ side for some account $k$ and side. The cost ledgerJlogCost $L$ $L'$ sums Jlog of the integer deltas on each debit and credit coordinate, where Jlog $t$ is the Recognition cost function applied to exp $t$ (equivalently $(e^t + e^{-t})/2 - 1$ in the Jlog module). The module upgrades vector lemmas to explicit ledger posting so that a single post changes the phi vector by exactly one unit and therefore flips exactly one parity bit.
proof idea
Tactic proof that first constructs a concrete candidate: the debit post at account 0. It shows this candidate is monotone, distinct from $L$, and has ledgerJlogCost exactly Jlog 1. Minimality then yields ledgerJlogCost $L$ $L'$ ≤ Jlog 1. The final step is a direct application of the upstream lemma postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1.
why it matters
The result closes the gap between arbitrary monotone ledger steps and the atomic PostingStep required by the parity-adjacency theorems in LedgerParityAdjacency. It thereby supplies the concrete unit-tick model needed for the eight-tick octave and one-bit parity changes that feed the Recognition Composition Law and the derivation of D = 3. The declaration sits inside the ledger-shaped model of Workstream B; its parent is the claim that posting-style updates induce one-bit adjacency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.