LogicIntNonIdentityReciprocal
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.
claimFor $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 in Recognition Science
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.
scope and limits
- Does not assert existence of any such z.
- Does not relate N to the J-cost or phi-ladder.
- Does not itself prove phase separation.
- Does not restrict z to values arising from the forcing chain.
formal statement (Lean)
23structure LogicIntNonIdentityReciprocal (z : LogicInt) : Prop where
24 pos : 0 < logicIntToInt z
25 nonidentity : logicIntToInt z ≠ 1
26 reciprocal_budget : ∃ N : ℕ, 0 < N ∧ Int.natAbs (logicIntToInt z) ∣ N ^ 2
27
28/-- Positive recovered integers yield positive natural carriers. -/