pith. sign in
module module high

IndisputableMonolith.Foundation.LedgerCanonicality

show as:
view Lean formalization →

The module defines the canonical comparison cost on positive reals that meets the minimal ledger axioms of reciprocal symmetry, unit normalization, strict convexity, continuity, and calibration. Researchers building the Recognition Science foundation cite it when establishing the base cost structure before deriving the Recognition Composition Law or forcing the phi scale. It supplies a collection of definitions that capture these properties directly from the imported Cost primitives.

claimA comparison cost $C: (0,1] ^2 to R$ on positive reals satisfying reciprocal symmetry $C(x,y)=C(y,x)$, unit normalization $C(1,1)=0$, strict convexity, continuity, and calibration to the form $J(x)=(x+x^{-1})/2-1$.

background

The module sits in the Foundation domain and imports the Cost module to supply basic cost primitives. It introduces sibling definitions such as AdmissibleCost, which encodes the comparison cost obeying the five minimal ledger axioms listed in the module doc-comment, along with ConservedCharge and ZeroParameterComparisonLedger. These objects prepare the zero-parameter ledger setting used throughout the axiom-closure plan.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base ledger axioms that downstream modules rely on for gap closure. ClosedObservableFramework absorbs these as structure fields in Phases 1-2 and 6. DAlembert.LedgerFactorization derives the Recognition Composition Law from the contextual substitutivity and factorization properties built here. HierarchyEmergence and HierarchyForcing use the zero-parameter ledger to force phi and the minimal hierarchy, while NeutralSector and PostingExtensivity close further steps toward additive scale composition.

scope and limits

used by (7)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)