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

IndisputableMonolith.Foundation.LedgerCanonicality

show as:
view Lean formalization →

This module defines the canonical comparison cost on positive reals that satisfies the minimal ledger axioms of reciprocal symmetry, unit normalization, strict convexity, continuity, and calibration. Researchers reconstructing observables from zero-parameter ledgers cite it as the entry point for the axiom-closure plan. It supplies the basic structures that enable downstream derivations of the phi scale and hierarchical emergence. The module achieves this through axiomatic definitions that import and extend the Cost module.

claimLet $J: (0,1] to R$ be a comparison cost satisfying reciprocal symmetry $J(x)=J(x^{-1})$, unit normalization $J(1)=0$, strict convexity, continuity, and calibration to the self-similar fixed point.

background

The module operates inside the Recognition Science foundation, where physics derives from a single functional equation and the Recognition Composition Law. It introduces the admissible cost as the primitive object for ledger comparisons on positive reals, together with conserved charge and neutral-sector properties. These definitions rest on the upstream Cost module and prepare the zero-parameter ledger for multilevel composition. The local setting is the minimal axiom set that later modules convert into definitions rather than external assumptions.

proof idea

This is a definition module, no proofs. It organizes the ledger axioms into structures such as AdmissibleCost and ConservedCharge, providing the interface for neutral states and local composition.

why it matters in Recognition Science

This module supplies the canonical ledger to ClosedObservableFramework for absorbing R1, R2, R5, R6 as definitions and to HierarchyEmergence for forcing the phi scale from zero-parameter closure. It also supports DAlembert.LedgerFactorization in deriving the RCL from substitutivity and HierarchyForcing for uniform scaling. The module fills the foundational gap by establishing the minimal axioms that lead to the eight-tick octave and D=3 in the unified forcing chain.

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)