quantum_ledger_fundamentals
plain-language theorem explainer
The quantum ledger satisfies non-negative J-costs on every entry, zero balance on the empty ledger, invariance of balance under any update, and vanishing sum of the eight complex phase factors. Workers deriving quantum mechanics from recognition ledgers cite this as the base layer for superposition and interference. The proof is a single term that packages four sibling lemmas on costs and phases.
Claim. $ (∀ e, 0 ≤ Jcost(e)) ∧ (empty ledger has balance 0) ∧ (∀ ledger L and update u, balance(applyUpdate L u) = balance(L)) ∧ (∑_{k=0}^7 exp(i phase(k)) = 0) $
background
LedgerEntry is a structure recording a single recognition event: a positive ratio together with its J-cost (equal to J(ratio)) and an integer phase slot in the 8-tick cycle. Ledger is a list of such entries whose balance field equals the sum of the logarithms of the ratios, enforcing conservation by construction. The module sets the local setting that quantum states are superpositions over ledger configurations and that the Born rule will later emerge from J-cost minimization. Upstream, phaseExp(k) is defined as Complex.exp(i · phase k) and tick supplies the fundamental time quantum τ₀ = 1.
proof idea
Term-mode proof that directly constructs the four-way conjunction from the four sibling theorems entry_cost_nonneg, empty_ledger_balance, ledger_balance_conserved and eight_tick_interference.
why it matters
Supplies the ledger axioms required for the quantum-ledger correspondence stated in the module doc-comment. It anchors the 8-tick octave (T7) inside the ledger via the phase sum and prepares the ground for later theorems that derive the Born rule from J-cost minimization. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.