finite_phase_separates_nonidentity
plain-language theorem explainer
A non-identity reciprocal integer ledger separates from the identity in the finite cyclic quotient Z/(carrier+1)Z. Number theorists formalizing phase budgets within Recognition Science cite this arithmetic separation. The proof exhibits the modulus carrier+1, assumes congruence to 1, reduces the remainders explicitly via modular inequalities, and contradicts the nonidentity hypothesis.
Claim. Let $L$ be a reciprocal integer ledger with positive integer carrier $n$ satisfying $n ≠ 1$ and $n$ dividing some square. Then there exists a positive integer $c$ such that the image of $n$ in $ℤ/cℤ$ is not equal to $1$.
background
The module FinitePhaseCompleteness supplies the first phase-budget theorem: a non-identity integer ledger possesses a finite cyclic quotient in which its phase differs from the identity phase. This supplies the finite arithmetic content behind the Recognition Science claim that a non-identity reciprocal ledger cannot remain invisible across all finite phase quotients. A ReciprocalIntegerLedger consists of a carrier : ℕ together with proofs that the carrier is positive, not equal to 1, and divides some square.
proof idea
Tactic-mode proof. The existential is witnessed by the modulus carrier+1 together with Nat.succ_pos. The assumption that the carrier equals 1 in this ZMod is converted via ZMod.natCast_eq_natCast_iff' into an equality of naturals. Explicit remainders are computed with Nat.mod_eq_of_lt (using carrier < carrier+1 and 1 < carrier+1 from carrier_pos), the equality is rewritten, and L.nonidentity yields the contradiction.
why it matters
The theorem is invoked directly by logicInt_finite_phase_separates to transfer the separation property to LogicIntNonIdentityReciprocal objects. It occupies the finite-arithmetic slot in the Recognition Science phase-budget chain, realizing the module claim that non-identity ledgers are detectable in some finite quotient. No open scaffolding remains; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.