natAbs_pos_of_logicInt_pos
plain-language theorem explainer
Positive recovered integers in the LogicInt ledger map to positive natural carriers under integer conversion. Phase completeness arguments cite this to guarantee Nat-level positivity when building reciprocal ledgers from logic integers. The proof is a one-line term applying the standard natAbs positivity lemma after rewriting the strict inequality as nonzero.
Claim. If $z$ belongs to the Grothendieck completion of logic naturals and the recovered integer value of $z$ is strictly positive, then the natural absolute value of that recovered integer is strictly positive.
background
LogicLedgerInterop transfers recovered LogicInt ledgers to integer-ledger phase-budget surfaces. LogicInt is the Grothendieck completion of LogicNat under addition, constructed as the quotient of pairs of naturals by the standard equivalence for integers. Upstream, the LogicInt definition supplies the setoid quotient, while phase supplies the eight-tick angles $k pi/4$ and reciprocal supplies the inverse-ratio event in the ledger forcing.
proof idea
One-line wrapper that applies Int.natAbs_pos.mpr to the negation of equality obtained from ne_of_gt on the strict positivity hypothesis.
why it matters
It supplies the positive carrier in the reciprocalIntegerLedger_of_logicInt construction used by finite phase completeness. The lemma closes the sign gap in the logic-to-Nat ledger transfer inside the eight-tick phase structure. It touches the phase separation step without adding new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.