module module high

`IndisputableMonolith.LedgerPostingAdjacency`

LedgerPostingAdjacency supplies the minimal carrier types for a d-account ledger, including AccountRS, LedgerState, phiVec, parity, Side, and post. It is referenced by parity-adjacency arguments but deliberately omits the recognition relation. The module contains only definitions.

claimDefines the carrier types for a $d$-account ledger: AccountRS, LedgerState (as integer vectors), phiVec (real vector), parity (mod-2 map), Side (debit/credit), and post (atomic update).

background

The module sits inside the Recognition Science ledger layer and imports Recognition (T1: nothing cannot recognize itself), Cost.Jlog, and LedgerParityAdjacency. The latter states that a single atomic ±1 update in one coordinate flips exactly one parity bit. Recognition relation is explicitly excluded from this carrier.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Provides the ledger carrier required by LedgerParityAdjacency for the one-bit adjacency claim of Workstream B2. It therefore supports the bridge from basic ledger states to parity patterns used in later forcing-chain steps.

scope and limits

Does not incorporate any recognition relation.
Does not contain theorems or proofs.
Does not compute J-costs or phi-ladder rungs.
Does not fix dimension D or constants such as phi.

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