logicIntToInt
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove any properties of the recovery map.
- Does not introduce new arithmetic operations.
- Does not connect directly to J-cost or the phi-ladder.
- Does not handle the inverse map from Int to LogicInt.
Lean usage
example (z : LogicInt) : Int := logicIntToInt zformal statement (Lean)
19abbrev logicIntToInt : LogicInt → Int := Foundation.IntegersFromLogic.LogicInt.toInt
proof body
Definition body.
20
21/-- A recovered integer ledger is non-identity when its `Int` recovery is
22positive and not equal to one. -/