entry_cost_zero_iff_unity
plain-language theorem explainer
A ledger entry has zero J-cost precisely when its recognition ratio equals one. Researchers deriving the Born rule from cost minimization in the quantum ledger model cite this equivalence. The term proof rewrites the entry cost definition and applies the upstream zero-condition lemma for the J function on positive reals.
Claim. Let $e$ be a ledger entry with positive ratio $r$. The J-cost of $e$ equals zero if and only if $r = 1$.
background
The QuantumLedger module connects Recognition Science ledgers to quantum states by treating quantum states as superpositions over ledger configurations, with the Born rule emerging from J-cost minimization rather than being postulated. A LedgerEntry structure records a single recognition event through its configuration ratio $r > 0$ together with the associated J-cost that must equal Jcost of that ratio. The key upstream lemma states that Jcost of a positive real vanishes if and only if the argument equals one.
proof idea
The term proof rewrites the cost field of the entry via its defining equation and directly applies the lemma Jcost_eq_zero_iff to the ratio together with its positivity witness.
why it matters
This equivalence supports the emergence of the Born rule from J-cost minimization inside the quantum ledger construction. It supplies the base case for the module's listed theorems on ledger conservation and born_rule_from_jcost. In the forcing chain it instantiates the J-uniqueness property (T5) at the level of individual recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.