module module

`IndisputableMonolith.Foundation.QuantumLedger`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.EightTick module_import
IndisputableMonolith.Foundation.LedgerForcing module_import

declarations in this module (24)

structure LedgerEntry L45
def mkEntry L60
theorem entry_cost_nonneg L70
theorem entry_cost_zero_iff_unity L75
structure Ledger L82
def totalCost L91
def emptyLedger L95
theorem empty_ledger_balance L101
theorem empty_ledger_cost L103
structure LedgerUpdate L109
def applyUpdate L120
theorem ledger_balance_conserved L133
theorem ledger_cost_additive L137
structure QuantumState L145
def probability L154
theorem prob_nonneg L158
theorem prob_sum_one L163
def expectedCost L170
theorem born_rule_jcost_connection L181
def entryPhase L189
def ledgerPhase L193
theorem empty_ledger_phase L197
theorem eight_tick_interference L204
theorem quantum_ledger_fundamentals L218