reciprocalIntegerLedger_of_logicInt
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.