Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LedgerCanonicality

show as:
view Lean formalization →

Defines the canonical comparison-ledger interface for Recognition Science foundation work: admissible costs on positive reals (reciprocal symmetry, unit normalization, strict convexity, continuity, calibration) together with zero-parameter ledger structure (conserved charge, neutral sector, multilevel and local composition). Hierarchy forcing, RCL factorization, and neutral-sector arguments import these structures. The module is definitional scaffolding over the Cost library.

claimAn admissible comparison cost $J:(0,\infty)\to\mathbb{R}$ obeys reciprocal symmetry $J(x)=J(x^{-1})$, unit normalization $J(1)=0$, strict convexity, continuity, and calibration. A zero-parameter comparison ledger packages such a $J$ with a conserved charge, a neutral sector (charge-zero states), and multilevel/local composition operations on comparisons.

background

Recognition Science treats physical comparison as a ledger: positive reals are ratios of observables, and a cost $J$ scores how far a ratio sits from identity. The Cost import supplies the ambient $J$-calculus; this module freezes the minimal axiom package that later forcing theorems treat as the only free structure.

An admissible cost is a comparison cost on $(0,\infty)$ with reciprocal symmetry, unit normalization, strict convexity, continuity, and calibration (the doc-comment package). Around it sit ledger primitives: a conserved charge on states, the neutral sector of charge-zero configurations, and flags for multilevel and local composition so hierarchical and contextual rewrites are well-typed.

The setting is pre-physics foundation work: no spacetime dimension, no $\varphi$, and no Recognition Composition Law yet. Those are forced downstream once a zero-parameter ledger is assumed nontrivial and closed under the composition interfaces defined here.

proof idea

This is a definition module, not a theorem package. It introduces structure classes and predicates (admissible cost, conserved charge, zero-parameter comparison ledger, neutral sector, multilevel/local composition) as Prop-carrying interfaces over the Cost library. No forcing argument is proved here; downstream modules discharge uniqueness and existence relative to these interfaces.

why it matters in Recognition Science

Every major Gap-closure path in Foundation imports this module as the shared ledger vocabulary. ClosedObservableFramework rebuilds observables and conservation as structure fields on top of it. LedgerFactorization derives the Recognition Composition Law from contextual substitutivity of ledger comparisons. HierarchyEmergence and HierarchyForcing use the zero-parameter multilevel ledger to force a minimal hierarchy and hence $\varphi$ as the unique admissible scale (T6 in the forcing chain). NeutralSector forces observable states into charge zero. PostingExtensivity and SubstitutivityForcing take the same interfaces toward additive scale composition and RCL combinators. Without a single canonical ledger signature, those arguments would not share hypotheses.

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)