ReciprocalIntegerLedger
plain-language theorem explainer
A structure packages a positive integer carrier not equal to 1 that divides some square N squared. Number theorists and Recognition Science researchers cite it to formalize non-identity reciprocal ledgers for phase-budget arguments. The definition is a direct record of four fields with no computation or lemmas.
Claim. A reciprocal integer ledger is a natural number $c > 0$ with $c ≠ 1$ such that $c$ divides $N^2$ for some natural number $N$.
background
The Finite Phase Completeness module 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 structure encodes the arithmetic carrier for that claim, drawing on the reciprocal automorphism from CostAlgebra (the map $x ↦ x^{-1}$ on positive elements) and the phase definition from EightTick. Engineering siblings supply analogous carrier and positivity constraints, such as the 5φ Hz frequency with its strict positivity proof.
proof idea
The declaration is a bare structure definition. It records the four fields carrier, carrier_pos, nonidentity, and has_reciprocal_budget with no tactics, no applied lemmas, and no reduction steps.
why it matters
The structure supplies the input type for finite_phase_completeness (every such ledger admits a finite cyclic phase quotient) and finite_phase_separates_nonidentity (separation from 1 in Z/(c+1)Z). It supplies the finite-arithmetic content of the Recognition Science statement that a non-identity reciprocal ledger cannot remain invisible across all finite phase quotients, linking directly to the eight-tick octave and T7 phase structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.