logicIntToInt
plain-language theorem explainer
The abbreviation supplies the canonical recovery map from LogicInt, the Grothendieck completion of LogicNat, to the standard integers. Researchers converting between logic-native ledgers and integer phase budgets cite this alias when building reciprocal structures or applying finite phase completeness. It is a direct one-line alias to the established toInt quotient lift.
Claim. The recovery map from the Grothendieck completion of LogicNat under addition to the integers is the quotient lift of the core map on pairs of naturals.
background
LogicInt is the Grothendieck completion of LogicNat under addition, formed as the quotient of pairs of naturals by the appropriate equivalence. The toInt function is the recovery map LogicInt to Int obtained by lifting the core map on representatives while respecting the setoid. The module transfers recovered LogicInt ledgers onto the existing integer-ledger phase-budget surface.
proof idea
One-line wrapper that aliases the toInt recovery map defined in IntegersFromLogic.
why it matters
This alias is used by the non-identity reciprocal structure on LogicInt and by the conversion to reciprocal integer ledgers that feed finite phase completeness. It supplies the bridge from the logic foundation to number-theoretic ledger operations. The construction sits inside the interop layer that prepares integer data for phase-budget calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.