entry_cost_nonneg
plain-language theorem explainer
The theorem shows that the J-cost attached to any ledger entry is non-negative. Workers on the quantum ledger formalization cite it when assembling the list of basic properties needed for conservation and Born-rule derivations. The proof is a one-line term that rewrites the entry cost field to the underlying Jcost function and applies the non-negativity lemma for positive ratios.
Claim. For every ledger entry $e$ with positive ratio $r$, the associated cost satisfies $0 ≤ J(r)$, where $J$ denotes the recognition cost function.
background
In the Quantum Ledger module a LedgerEntry is a structure that records a single recognition event: it carries a natural-number identifier, a positive real ratio, and a cost field required to equal the J-cost of that ratio. The module treats quantum states as superpositions over such ledger configurations, with the Born rule emerging from cost minimization rather than being postulated. Upstream, Jcost_nonneg (from both the Cost and JcostCore modules) states that $J(x) ≥ 0$ for all $x > 0$, proved by rewriting to a square-over-positive-denominator form and invoking non-negativity of squares.
proof idea
The term proof rewrites the cost field of the supplied LedgerEntry via its defining equation, reducing the goal to an application of the Jcost_nonneg lemma on the entry's positive-ratio hypothesis.
why it matters
The result supplies the first conjunct of the quantum_ledger_fundamentals theorem, which collects the basic ledger properties required for the quantum-state interpretation. It thereby anchors the non-negativity of recognition costs inside the ledger-to-quantum bridge, consistent with the J-uniqueness step of the forcing chain and the subsequent derivation of the Born rule from cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.