LedgerEntry
plain-language theorem explainer
LedgerEntry structures a single recognition event by bundling a natural-number identifier, a positive real ratio, its J-cost, and a phase in the eight-tick cycle, with the field constraint that stored cost equals Jcost of the ratio. Researchers deriving quantum states from ledger superpositions cite it when constructing entries or proving cost properties. The definition is a direct structure declaration that enforces the J-cost equality at the type level.
Claim. A ledger entry is a tuple $(id, r, c, p)$ where $id$ is a natural number, $r > 0$ is a real ratio, $c$ is a real number satisfying $c = J(r)$, and $p$ is an integer phase in the set of eight possible values.
background
In Recognition Science the J-cost function is the unique solution to the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) for positive reals, and is non-negative. The eight-tick phase is drawn from the fundamental octave period of length 8. The module states that quantum states are ledger superpositions |ψ⟩ = Σ c_i |L_i⟩ where each L_i is a ledger configuration and the Born rule emerges from J-cost minimization.
proof idea
This is a structure definition whose fields directly encode the required data and the invariant cost = Jcost ratio; no separate proof is needed.
why it matters
LedgerEntry supplies the atomic object for the Ledger structure and for downstream results such as entry_cost_nonneg, entry_cost_zero_iff_unity, and quantum_ledger_fundamentals. It realizes the module's stated core concept of a recognition event carrying J-cost, thereby linking the ledger formalism to the eight-tick cycle and the emergence of quantum mechanics from cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.