finite_phase_separates_nonidentity
Non-identity reciprocal integer ledgers admit a finite cyclic quotient separating their carrier from the identity element. Number theorists formalizing phase budgets in Recognition Science cite this as the basic finite arithmetic fact. The proof selects modulus equal to carrier plus one, reduces the assumed equality in the quotient to modular identities, and obtains a contradiction with the nonidentity hypothesis.
claimLet $L$ be a reciprocal integer ledger whose carrier $n$ satisfies $n > 0$ and $n ≠ 1$. Then there exists a positive integer $c$ such that the residue class of $n$ in $ℤ/cℤ$ is not equal to $1$.
background
ReciprocalIntegerLedger is the structure whose fields are a positive integer carrier, a proof of carrier positivity, a proof that the carrier differs from 1, and the existence of an integer N such that the carrier divides N squared. The module FinitePhaseCompleteness presents the first phase-budget theorem: a non-identity integer ledger possesses a finite cyclic quotient in which its phase is not the identity phase. This supplies the finite arithmetic content of the Recognition Science claim that a non-identity reciprocal ledger cannot be invisible in every finite phase quotient.
proof idea
The tactic proof constructs the witness c := L.carrier + 1 and invokes Nat.succ_pos for positivity. It assumes equality of the carrier with 1 inside ZMod c, applies the natCast_eq_natCast_iff lemma to obtain an equality of remainders, computes the two remainders explicitly via mod_eq_of_lt, and feeds the resulting equality carrier = 1 into the nonidentity field to reach a contradiction.
why it matters in Recognition Science
The declaration supplies the finite-arithmetic foundation for phase separation. It is invoked directly by logicInt_finite_phase_separates in LogicLedgerInterop to transfer the separation property to non-identity reciprocal logic integers. The result therefore closes the finite half of the Recognition Science statement that non-identity reciprocal ledgers are visible in some finite phase quotient, consistent with the phase-budget theorems and the eight-tick octave structure of the framework.
scope and limits
- Does not establish separation inside the infinite cyclic group ℤ.
- Does not invoke or rely on the has_reciprocal_budget field of the ledger.
- Does not produce an explicit bound on the size of the separating modulus.
- Does not extend to real-valued or continuous carriers.
Lean usage
finite_phase_separates_nonidentity (reciprocalIntegerLedger_of_logicInt h)formal statement (Lean)
33theorem finite_phase_separates_nonidentity (L : ReciprocalIntegerLedger) :
34 ∃ c : ℕ, 0 < c ∧ (L.carrier : ZMod c) ≠ 1 := by
proof body
Tactic-mode proof.
35 refine ⟨L.carrier + 1, Nat.succ_pos L.carrier, ?_⟩
36 intro h
37 have hmod := (ZMod.natCast_eq_natCast_iff' L.carrier 1 (L.carrier + 1)).mp h
38 have hleft : L.carrier % (L.carrier + 1) = L.carrier :=
39 Nat.mod_eq_of_lt (Nat.lt_succ_self L.carrier)
40 have hright : 1 % (L.carrier + 1) = 1 := by
41 apply Nat.mod_eq_of_lt
42 exact Nat.succ_lt_succ L.carrier_pos
43 rw [hleft, hright] at hmod
44 exact L.nonidentity hmod
45
46end FinitePhaseCompleteness
47end NumberTheory
48end IndisputableMonolith