ledgerPhase
plain-language theorem explainer
ledgerPhase assigns to any ledger the product of the complex phase factors of its entries. Researchers modeling quantum states as ledger superpositions cite it when extracting interference from eight-tick phases or verifying phase conservation. The definition is a direct one-line product after mapping entryPhase over the entry list.
Claim. For a ledger $L$ with entries $e_1, e_2, ..., e_n$, the total phase is $P(L) = e^{i theta_1} e^{i theta_2} ... e^{i theta_n}$, where each $theta_k$ is the eight-tick phase angle of entry $e_k$.
background
The QuantumLedger module treats a Ledger as a structure holding a list of LedgerEntry records together with a real balance equal to the sum of the logarithms of their ratios. This structure is interpreted as a quantum configuration whose superposition amplitudes arise from J-cost minimization, with phases supplied by the eight-tick cycle. Upstream, entryPhase wraps the eight-tick phase exponential, while the phase definition in EightTick supplies the discrete angles $k pi / 4$ for $k = 0$ to $7$.
proof idea
One-line definition that maps entryPhase over L.entries and returns the product of the resulting complex numbers.
why it matters
The definition supplies the total phase required by the downstream empty_ledger_phase theorem, which asserts that an empty ledger evaluates to phase 1. It anchors the module's claim that quantum states are ledger superpositions and that eight-tick interference emerges when phases are summed over all configurations. The result therefore closes one link in the ledger-to-quantum correspondence without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.