intCast_ne_zero_of_ne_zero
plain-language theorem explainer
If a nonzero integer is embedded into the reals, the image stays nonzero. This auxiliary fact prevents spurious zeros when integer ledger deltas are fed into Jlog cost sums inside the Recognition ledger model. The proof is a one-line wrapper that invokes exact_mod_cast on the given hypothesis.
Claim. Let $z$ be an integer. If $z ≠ 0$, then the canonical image of $z$ in the reals satisfies $(z : ℝ) ≠ 0$.
background
LedgerState d is the abbreviation Recognition.Ledger (AccountRS d), where AccountRS d equips the finite set Fin d with the trivial recognition relation. Side is the inductive type carrying debit and credit labels for atomic posts. The module models ledger updates in which a single post adds or subtracts exactly one unit at one coordinate, inducing a one-bit change in the parity vector phi = debit - credit. The integer-to-real cast appears when Jlog is applied to the delta vectors inside ledgerJlogCost.
proof idea
One-line wrapper that applies exact_mod_cast to the integer inequality hypothesis.
why it matters
Supplies the elementary non-vanishing fact required to keep Jlog arguments well-defined when integer deltas from ledger posts are cast to reals. It sits inside the ledger-posting adjacency development that bridges the abstract parity adjacency lemma to an explicit debit-credit ledger. The surrounding file contributes the concrete model needed before the Recognition Composition Law and phi-ladder mass formulas can be applied to posting sequences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.