entryPhase
plain-language theorem explainer
The entryPhase definition assigns to each ledger entry its complex phase factor drawn from the eight-tick cycle. A physicist modeling quantum superpositions over recognition events would cite this when deriving the total phase of a ledger configuration. The definition is a direct one-line wrapper around the phaseExp function from the EightTick module.
Claim. For a ledger entry $e$ whose phase index lies in Fin 8, the phase factor is defined as $e^{i k π/4}$ where $k$ is that index.
background
The QuantumLedger module formalizes the link between Recognition Science ledgers and quantum states, treating ledger entries as recognition events that carry both a J-cost and a discrete phase. The LedgerEntry structure records an identifier, a positive real ratio, its J-cost, and a phase field taking values in Fin 8. These phases correspond to the eight-tick cycle whose angles are multiples of π/4. Upstream, the EightTick.phaseExp definition supplies the map from Fin 8 to ℂ via Complex.exp (Complex.I * phase k), with the explicit remark that each such factor raised to the eighth power equals 1.
proof idea
This is a one-line wrapper that applies the phaseExp function from EightTick directly to the phase field of the supplied LedgerEntry.
why it matters
The definition supplies the phase factor consumed by the downstream ledgerPhase function, which forms the product of all entry phases in a ledger. It implements the eight-tick octave (T7) inside the quantum-ledger connection, ensuring that phase factors close after eight steps as required by the forcing chain. The module doc-comment states that quantum states are ledger superpositions and that the Born rule emerges from J-cost minimization; entryPhase provides the phase component of that superposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.