finite_phase_completeness
plain-language theorem explainer
Every reciprocal integer ledger admits a finite cyclic quotient. Number theorists in Recognition Science cite this as the base arithmetic fact supporting phase separation. The proof is a one-line term that directly instantiates the carrier field of the ledger structure together with its positivity and the trivial nonemptiness of any ZMod c for c positive.
Claim. Let $L$ be a reciprocal integer ledger (a structure consisting of a positive integer carrier not equal to 1 that satisfies a reciprocal budget condition). Then there exists a positive integer $c$ such that the cyclic group $Z/cZ$ is nonempty.
background
ReciprocalIntegerLedger is the structure with fields carrier : ℕ, carrier_pos : 0 < carrier, nonidentity : carrier ≠ 1, and has_reciprocal_budget : ∃ N, carrier ∣ N². The module FinitePhaseCompleteness supplies the first phase-budget theorem: a non-identity integer ledger has a finite cyclic quotient in which its phase is not the identity phase. This supplies the finite arithmetic content behind the Recognition Science claim that a non-identity reciprocal ledger cannot be invisible in all finite phase quotients. Upstream, the EightTick.phase definition supplies the 8-tick phases kπ/4 for k = 0..7 that motivate the cyclic quotients.
proof idea
One-line term proof that applies the carrier and carrier_pos fields of the ReciprocalIntegerLedger structure, then supplies the canonical element 0 to witness Nonempty (ZMod c). No additional lemmas are invoked beyond the structure projections and the standard fact that ZMod c is inhabited for c > 0.
why it matters
This theorem is the base case for the sibling result finite_phase_separates_nonidentity. It fills the finite-arithmetic step in the module's statement that non-identity reciprocal ledgers are separated from the identity in some finite cyclic quotient. The result sits inside the T7 eight-tick octave of the forcing chain and supplies the arithmetic substrate for later claims that non-identity carriers cannot remain invisible across all finite phase quotients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.