LogicIntNonIdentityReciprocal
plain-language theorem explainer
LogicIntNonIdentityReciprocal encodes the predicate on a recovered integer z that is positive, unequal to one, and admits a natural N whose square is divisible by the absolute value of z. Researchers transferring logic-derived integers into the phase-budget surface cite this predicate to apply finite phase separation. The declaration is a bare structure with three fields and no proof obligations.
Claim. For $z$ recovered from the logic ledger, the predicate holds when $z > 0$, $z ≠ 1$, and there exists $N ∈ ℕ$ with $N > 0$ such that $|z|$ divides $N^2$.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of pairs of LogicNat. The abbreviation logicIntToInt recovers the corresponding element of the standard integers. The module transfers recovered LogicInt ledgers onto the integer-ledger phase-budget surface so that finite phase completeness results become applicable.
proof idea
The declaration is a direct structure definition whose three fields are positivity of the recovered integer, inequality to one, and existence of a suitable natural N for the reciprocal budget condition. No lemmas or tactics are invoked.
why it matters
The predicate supplies the hypothesis for logicInt_finite_phase_separates, which shows that recovered non-identity integer ledgers admit a finite phase separation from identity, and for the conversion reciprocalIntegerLedger_of_logicInt that produces the Nat-level reciprocal ledger. It thereby closes the transfer from logic integers to the phase-budget surface used in finite phase completeness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.