pith. sign in
module module high

IndisputableMonolith.Foundation.QuantumLedger

show as:
view Lean formalization →

QuantumLedger defines LedgerEntry and Ledger to record recognition events with associated costs in Recognition Science. It builds directly on J-symmetry from LedgerForcing and the 8-tick cycle from EightTick to ensure balance conservation in updates. Researchers extending the foundational ledger to quantum models cite these definitions. The module uses straightforward type definitions and nonnegativity lemmas rather than deep proofs.

claimIntroduces the type $LedgerEntry$ for a single recognition event carrying all RS data and the type $Ledger$ as an aggregate whose $totalCost$ is conserved under $applyUpdate$.

background

The module sits in the Foundation domain and assembles ledger primitives on top of three imports. The EightTick module states that reality operates on a discrete 8-tick cycle with phases 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. LedgerForcing proves that J-symmetry forces double-entry ledger structure, while Cost supplies the underlying J-cost function used in the nonnegativity results.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The ledger structures supply the concrete double-entry objects required by the forcing chain and feed parent constructions that apply the eight-tick octave and Recognition Composition Law. It concretizes the J-symmetry result from LedgerForcing for use in cost accounting and quantum extensions.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (24)