LogicInt
plain-language theorem explainer
LogicInt aliases the Grothendieck completion of LogicNat under addition to serve as the integer ledger on the phase-budget surface. Researchers bridging logic foundations to Recognition number theory cite this alias when importing the integer operations for downstream ring identities. The declaration is a direct one-line abbreviation with no additional content or obligations.
Claim. Let $LogicInt$ be the Grothendieck completion of the logic naturals under addition, realized as the quotient of pairs of logic naturals by the equivalence $(a,b)sim(c,d)$ iff $a+d=b+c$.
background
The LogicLedgerInterop module transfers the recovered LogicInt ledger to the existing integer-ledger phase-budget surface. Upstream, LogicInt is the Grothendieck completion of LogicNat under addition, defined as the quotient of LogicNat × LogicNat by the setoid equivalence. This supplies the additive group structure used by the ring operations in the foundation layer.
proof idea
The declaration is a one-line abbreviation that directly references the LogicInt definition from the IntegersFromLogic foundation module.
why it matters
This alias enables LogicInt in the number theory interop layer and is referenced by forty downstream declarations, including the addition operation and the associativity, commutativity, and distributivity theorems. Those results apply the transfer principle eq_iff_toInt_eq to reduce LogicInt equations to standard integer arithmetic. It supplies the integer ledger required for phase budgets in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.