IndisputableMonolith.NumberTheory.LogicLedgerInterop
This module bridges logic-derived integer ledgers to standard integer recoveries within Recognition Science number theory. It defines non-identity recovered ledgers as those whose integer value is positive and unequal to one, then links them to finite cyclic quotients via imported completeness results. The module supplies conversion functions and separation lemmas that make logic integers usable in phase-budget arguments. It consists of targeted interop definitions and lemmas rather than a single overarching proof.
claimLet $L$ be a logic integer ledger. The recovery map sends $L$ to an element of $Z$. The ledger is non-identity when this recovery is positive and not equal to $1$. The module also supplies the reciprocal ledger construction and the finite-phase separation map that places the phase of $L$ outside the identity class in a suitable cyclic quotient.
background
The module sits in the NumberTheory domain and imports IntegersFromLogic, which constructs the LogicInt type from logical primitives, together with FinitePhaseCompleteness. The latter states: 'The first phase-budget theorem: a non-identity integer ledger has a finite cyclic quotient in which its phase is not the identity phase.' Key definitions introduced are LogicInt (the logic-based integer type), logicIntToInt (the recovery map to ordinary integers), and auxiliary maps such as reciprocalIntegerLedger_of_logicInt. These objects allow the non-identity condition to be expressed directly in terms of the recovered integer value.
proof idea
This is a definition module, no proofs. It assembles a collection of supporting definitions (LogicInt, logicIntToInt) and lemmas (LogicIntNonIdentityReciprocal, natAbs_pos_of_logicInt_pos, reciprocalIntegerLedger_of_logicInt, logicInt_finite_phase_separates) that translate the upstream finite-phase statement into the language of logic integers.
why it matters in Recognition Science
The module supplies the arithmetic interop layer required by the finite phase completeness theorem, ensuring that non-identity reciprocal ledgers become visible in finite quotients. It thereby supports the RS claim that a non-identity reciprocal ledger cannot remain invisible across all finite phase quotients, feeding directly into the phase-budget results that rest on the eight-tick octave and the J-uniqueness fixed point.
scope and limits
- Does not prove the full phase-budget theorem.
- Does not treat infinite phase quotients.
- Does not compute explicit numerical phase values.
- Restricts attention to positive non-identity recoveries.