pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.LedgerUnits

show as:
view Lean formalization →

LedgerUnits defines the subgroup of ℤ generated by a base parameter δ and specializes to δ=1 to obtain a clean order isomorphism with the integers. It supplies conversion maps fromZ and toZ together with uniqueness and specification lemmas. Researchers building ledger-style dual complexity models cite it to discretize units for computation-versus-recognition arguments. The module consists of targeted definitions and basic equivalence lemmas rather than deep derivations.

claimLet $G = ⟨δ⟩ ⊆ ℤ$ be the cyclic subgroup generated by δ. Specializing to δ = 1 yields an order isomorphism φ: G → ℤ with explicit inverse maps satisfying φ ∘ ψ = id and ψ ∘ φ = id, together with uniqueness of representations.

background

The module introduces ledger units as the cyclic subgroup generated by δ inside the integers, with δ fixed to 1 to produce a direct order isomorphism. Core objects are DeltaSub (the generated subgroup), fromZ and toZ (the conversion functions), and supporting lemmas such as toZ_spec, rep_unique, and equiv_delta_one that certify the bijection and order preservation. The setting is a discrete-unit foundation for ledger-based representations; the module imports only Mathlib and relies on its subgroup-generation and order-isomorphism infrastructure.

proof idea

This is a definition module. It declares DeltaSub, fromZ, toZ and the one-step lemmas fromZ_one, toZ_one, toZ_fromZ_one, fromZ_toZ_one, equiv_delta_one, toZ_spec, rep_unique, toZ_fromZ, fromZ_toZ. Each lemma is a direct verification of the isomorphism properties using the δ = 1 specialization; no multi-step tactic chains or external results beyond Mathlib basics are required.

why it matters in Recognition Science

The module supplies the discrete unit structure consumed by the downstream ComputationBridge scaffold in IndisputableMonolith.Complexity. That bridge explores a hypothetical ledger-style dual-complexity approach to P versus NP but is explicitly marked as exploratory and outside the verified certificate chain (UltimateClosure, CPMClosureCert, etc.). LedgerUnits therefore provides the notational and isomorphism substrate for such exploratory work without participating in the main T0–T8 forcing chain or Recognition Composition Law derivations.

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)