pith. sign in
module module moderate

IndisputableMonolith.LedgerUnits

show as:
view Lean formalization →

The LedgerUnits module defines the cyclic subgroup of the integers generated by a parameter δ and specializes to δ equal to one to obtain an order isomorphism with the integers. It supplies conversion maps between the subgroup and the integers together with uniqueness and round-trip lemmas. Researchers working on discrete ledger models in complexity theory would reference these units. The module consists entirely of definitions and elementary lemmas with no non-trivial proofs.

claimThe subgroup $\langle \delta \rangle \leq \mathbb{Z}$ generated by $\delta$, equipped with order-isomorphism maps between the subgroup and $\mathbb{Z}$ when $\delta = 1$.

background

The module establishes the subgroup of the integers generated by a parameter δ. The doc-comment states: 'The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism.' It defines the subgroup and supplies the conversion maps together with lemmas on specification, uniqueness, and the round-trip identities. The setting is purely algebraic and imports only Mathlib.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the basic unit conversions imported by the ComputationBridge scaffold. That downstream module is explicitly marked as a scaffold exploring a hypothetical P versus NP framework based on ledger-style dual complexity and lies outside the verified certificate chain.

scope and limits

used by (1)

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

declarations in this module (23)