module module moderate

`IndisputableMonolith.LedgerPostingAdjacency`

LedgerPostingAdjacency supplies the minimal data carrier for a d-account ledger in the Recognition framework, setting recognition relations aside. It introduces LedgerState together with phiVec, parity, Side, post, and PostingStep to represent atomic updates. Ledger parity and adjacency work depends on these carriers to track single-coordinate changes. The module consists entirely of definitions with no proofs or theorems.

claimThe module declares types and functions for a minimal $d$-account ledger carrier: LedgerState as the state type, phiVec mapping states to vectors on the phi-ladder, parity as the mod-2 pattern, Side as debit or credit, post as the atomic update operation, and PostingStep as the one-step transition.

background

The module operates in the ledger layer of Recognition Science, importing the core Recognition axioms (T1: nothing cannot recognize itself), the J-cost machinery from Cost.Jlog, and the parity-adjacency bridge from LedgerParityAdjacency. It defines AccountRS as the account identifier, phiVec as the coordinate representation on the phi-ladder, and parity as the odd-even signature of the state vector. LedgerState serves as the minimal carrier that records these coordinates without embedding recognition relations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the state representation required by the parity-adjacency bridge in LedgerParityAdjacency, which converts single atomic postings into one-bit parity flips. It thereby supports the forcing-chain steps that link ledger updates to the eight-tick octave and spatial dimension count. No downstream theorems are yet recorded.

scope and limits

Does not embed recognition relations or J-cost evaluations.
Does not prove any theorems or lemmas.
Does not model multi-step or multi-account interactions beyond single postings.
Does not assign numerical values to phi or other constants.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.Jlog module_import
IndisputableMonolith.LedgerParityAdjacency module_import
IndisputableMonolith.Recognition module_import

declarations in this module (43)

def AccountRS L35
instance accountRS_atomicTick L48
abbrev LedgerState L58
abbrev phiVec L60
abbrev parity L63
inductive Side L68
def post L74
lemma phiVec_post_debit L84
lemma phiVec_post_credit L93
lemma phiVec_coordAtomicStep_of_post L104
theorem parity_oneBitDiff_of_post L133
def PostingStep L143
theorem postingStep_oneBitDiff L146
def ledgerL1Cost L154
def MonotoneLedger L159
def LegalAtomicTick L163
def ledgerJlogCost L169
theorem ledgerJlogCost_nonneg L173
lemma ledgerJlogCost_post L183
lemma intCast_ne_zero_of_ne_zero L243
lemma jlog_lt_jlog_of_one_lt L246
theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 L253
theorem ledgerL1Cost_eq_zero_iff L611
lemma post_monotone L664
lemma ledgerL1Cost_post L687
theorem legalAtomicTick_of_post L748
theorem postingStep_implies_legalAtomicTick L752
lemma int_natAbs_eq_one_of_nonneg L757
lemma int_eq_of_natAbs_eq_zero L773
lemma exists_unique_of_sum_univ_eq_one L776
theorem legalAtomicTick_implies_PostingStep L810
theorem postingStep_iff_legalAtomicTick L924
theorem minCost_monotoneStep_implies_postingStep L930
theorem minJlogCost_monotoneStep_implies_postingStep L969
theorem legalAtomicTick_oneBitDiff L994
def accountAt L1002
lemma postedAt_accountAt L1005
def stepAt L1012
lemma stepAt_isPostingStep L1016
theorem stepAt_oneBitDiff L1020
abbrev PostInstr L1027
def run L1030
theorem run_step_oneBitDiff L1036