entryPhase
EntryPhase maps each ledger entry to the complex exponential of its discrete phase index drawn from the eight-tick cycle. Researchers constructing quantum amplitudes from recognition ledgers cite this definition when forming total phases for superpositions or deriving Born-rule weights. It is a one-line wrapper that delegates directly to the phaseExp function on the entry's phase field.
claimFor a ledger entry $e$ carrying phase index $k$ in the eight-tick cycle, the phase factor is $e^{i k π / 4}$.
background
LedgerEntry is the structure that records a single recognition event: it holds a unique identifier, a positive real ratio, the associated J-cost, and a phase index in the eight-tick cycle. The QuantumLedger module treats quantum states as superpositions over collections of such entries, with probabilities emerging from J-cost minimization rather than being introduced by postulate. The eight-tick phase definition supplies the angles $k π / 4$ for $k = 0, …, 7$, and phaseExp converts each angle to the corresponding point on the unit circle in the complex plane.
proof idea
It is a one-line wrapper that applies EightTick.phaseExp to the phase field of the supplied LedgerEntry.
why it matters in Recognition Science
This definition supplies the phase factor required by the downstream ledgerPhase construction, which assembles the total phase of a ledger as the product over its entries. It therefore embeds the eight-tick octave (T7) into the ledger-to-quantum mapping and supports the emergence of complex amplitudes needed for the Born-rule derivation in the Recognition Science framework.
scope and limits
- Does not compute or modify the J-cost of any entry.
- Does not enforce ledger balance conservation.
- Does not extend phases outside the discrete eight-tick indices.
- Does not derive probabilities or the Born rule.
Lean usage
noncomputable def ledgerPhase (L : Ledger) : ℂ := (L.entries.map entryPhase).prodformal statement (Lean)
189noncomputable def entryPhase (e : LedgerEntry) : ℂ :=
proof body
Definition body.
190 EightTick.phaseExp e.phase
191
192/-- The total phase of a ledger (product of entry phases). -/