pith. sign in
module module moderate

IndisputableMonolith.NumberTheory.FinitePhaseCompleteness

show as:
view Lean formalization →

The module supplies the reciprocal integer ledger carrier together with finite phase completeness and non-identity separation results. Researchers building logic-ledger interop surfaces in Recognition Science cite it to bridge integer phases with budget accounting. The module organizes sibling definitions and lemmas without containing standalone proofs.

claimThe reciprocal integer ledger carrier, denoted $R$, satisfies finite phase completeness: every non-identity element is separated by a finite phase partition under the J-cost.

background

The NumberTheory.FinitePhaseCompleteness module introduces the reciprocal integer ledger as a carrier for integers closed under the reciprocal operation. It adopts the J-cost and Recognition Composition Law conventions from the surrounding number-theory layer and restricts attention to finite phases on the phi-ladder. The module thereby prepares ledger objects for transfer to phase-budget surfaces.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the finite-phase objects required by LogicLedgerInterop, which transfers the recovered LogicInt ledger to the existing integer-ledger phase-budget surface. It therefore closes the number-theory segment of the ledger construction inside the Recognition Science framework.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (3)