mkEntry
plain-language theorem explainer
The entry constructor assembles a recognition event from a natural-number identifier, a positive real ratio, and an index in the eight-tick cycle. Modelers of the quantum-ledger connection invoke it to populate ledger configurations whose J-costs later yield Born-rule probabilities. The definition proceeds by direct record construction that sets the cost field to Jcost of the ratio and closes the equality by reflexivity.
Claim. Let $n$ be a natural number, $r>0$ a positive real, and $p$ an element of the finite set of eight phases. The constructor yields a ledger entry whose identifier is $n$, whose ratio is $r$, whose positivity witness is the given proof, whose cost equals $J(r)$, and whose phase is $p$.
background
A ledger entry is a single recognition event carrying an identifier, a configuration ratio, a positivity proof, a J-cost, and a phase in the eight-tick cycle. The module situates these entries inside quantum states realized as superpositions over ledger configurations, with the Born rule emerging from J-cost minimization rather than being postulated. Upstream, the phase function supplies the eight values $kπ/4$ for $k=0$ to $7$, while the cost operation on multiplicative recognizers supplies the derived J-cost map used for the entry.
proof idea
One-line record construction that directly assigns the supplied id, ratio, and positivity witness, computes cost via the J-cost map on the ratio, inserts the phase index, and discharges the cost-equality field by reflexivity.
why it matters
The definition supplies the atomic objects required by the module's stated theorems on ledger-entry cost equality and conservation. It instantiates the recognition events that become the basis vectors for the quantum superpositions described in the module documentation, thereby linking the eight-tick phase structure to the ledger formalism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.