logicIntToInt
plain-language theorem explainer
The abbreviation supplies the recovery map sending a LogicInt, the Grothendieck completion of LogicNat, to a standard integer. Researchers bridging logic ledgers to integer phase budgets cite it when converting representations for reciprocal calculations. It is realized as a direct alias to the existing quotient-lifted toInt function.
Claim. The recovery map $f : LInt → ℤ$ is the quotient lift of the core map sending a pair of naturals $(a,b)$ to $a-b$, where $LInt$ denotes the Grothendieck completion of LogicNat under addition.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of LogicNat × LogicNat by the appropriate equivalence. The toInt function is the induced map to ℤ that respects this equivalence and recovers the difference of the pair representatives. The module transfers recovered LogicInt ledgers onto the integer-ledger phase-budget surface required by finite phase completeness.
proof idea
One-line wrapper that aliases the toInt recovery map already defined in IntegersFromLogic.
why it matters
It supplies the conversion used by LogicIntNonIdentityReciprocal to enforce the positive non-identity condition and by reciprocalIntegerLedger_of_logicInt to produce the Nat-level carrier for phase completeness. This interop step connects the logic-based integer construction to the number-theoretic machinery that feeds finite phase completeness and reciprocal budget calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.