reciprocalIntegerLedger_of_logicInt
Converts a non-identity logic integer (positive recovered value not equal to 1, with absolute value dividing some square) into the natural-number reciprocal ledger required for finite-phase separation. Researchers bridging logic-based integers to the phase-budget surface cite it to apply separation results downstream. The definition is a direct structure constructor that sets the carrier to the absolute value and delegates positivity and budget checks to prior lemmas on logic integers.
claimLet $z$ be a logic integer whose recovered integer value is positive, not equal to 1, and whose absolute value divides $N^2$ for some natural $N>0$. The associated reciprocal integer ledger has natural carrier equal to the absolute value of the recovered integer, together with the induced positivity, non-identity, and reciprocal-budget properties.
background
The module transfers recovered logic integers to the integer-ledger phase-budget surface. LogicInt is the Grothendieck completion of LogicNat under addition, so integers arise as equivalence classes of pairs of naturals. The non-identity reciprocal condition requires the recovered value to be positive, unequal to 1, and to satisfy the divisibility condition that its absolute value divides some square $N^2$ with $N>0$.
proof idea
The definition constructs the reciprocal integer ledger structure by setting the carrier to the natural absolute value of the recovered integer. Positivity is obtained by applying the lemma natAbs_pos_of_logicInt_pos to the positivity hypothesis. Non-identity proceeds by contradiction: assume the carrier equals 1, cast to recover the integer value 1, and contradict the nonidentity hypothesis. The reciprocal budget is extracted by case analysis on the witness supplied in the input structure.
why it matters in Recognition Science
This supplies the bridge used by logicInt_finite_phase_separates, which states that recovered non-identity integer ledgers possess a finite phase separating them from identity. It completes the interop layer that lets finite-phase completeness operate on logic-derived integers, supporting transfer from logic constructions to the phase-budget surface in eight-tick arguments.
scope and limits
- Does not prove existence of any non-identity logic integer.
- Does not compute explicit numerical carriers or phases.
- Does not handle the identity case for logic integers.
- Does not extend the construction beyond the reciprocal-budget setting.
Lean usage
logicInt_finite_phase_separates (reciprocalIntegerLedger_of_logicInt h)formal statement (Lean)
37def reciprocalIntegerLedger_of_logicInt
38 {z : LogicInt}
39 (h : LogicIntNonIdentityReciprocal z) :
40 ReciprocalIntegerLedger where
41 carrier := Int.natAbs (logicIntToInt z)
proof body
Definition body.
42 carrier_pos := natAbs_pos_of_logicInt_pos h.pos
43 nonidentity := by
44 intro hcarrier
45 have h_toInt_abs : Int.natAbs (logicIntToInt z) = 1 := hcarrier
46 have h_toInt : logicIntToInt z = 1 := by
47 have habs_cast : (Int.natAbs (logicIntToInt z) : Int) = 1 := by
48 exact_mod_cast h_toInt_abs
49 rw [Int.natAbs_of_nonneg (le_of_lt h.pos)] at habs_cast
50 exact habs_cast
51 exact h.nonidentity h_toInt
52 has_reciprocal_budget := by
53 rcases h.reciprocal_budget with ⟨N, _hNpos, hdiv⟩
54 exact ⟨N, hdiv⟩
55
56/-- Recovered non-identity integer ledgers have a finite phase separating
57them from identity. -/