pith. sign in
structure

ZeroParameterComparisonLedger

definition
show as:
module
IndisputableMonolith.Foundation.LedgerCanonicality
domain
Foundation
line
44 · github
papers citing
8 papers (below)

plain-language theorem explainer

A ZeroParameterComparisonLedger packages a nonempty countable carrier, an admissible cost J on positive reals, a conserved charge map, and closure under multiplicative composition with no free parameters. Recognition Science researchers cite this interface when deriving the unconditional inevitability theorem from ledger axioms alone. The declaration is a direct structure definition that assembles the required fields without lemmas or proof steps.

Claim. A structure on a type $C$ consisting of: nonempty countable carrier $C$; admissible cost $J: (0,∞)→ℝ$ obeying reciprocal symmetry $J(x)=J(x^{-1})$, $J(1)=0$, strict convexity, continuity, and calibration of the second derivative at the origin; conserved charge $χ:C→ℝ$; no injective embedding $ℝ→C$; and the property that for all positive $x,y$ there exists a continuous $P$ such that $J(xy)+J(x/y)=P(J(x),J(y))$.

background

The module defines the ZeroParameterComparisonLedger as the single primitive object consumed by every downstream emergence theorem. It requires a countable carrier equipped with a conserved scalar charge and an admissible cost $J$ on positive reals. AdmissibleCost encodes reciprocal symmetry, unit normalization at 1, strict convexity on $(0,∞)$, continuity, and the calibration condition that the second derivative of $J∘exp$ at 0 equals 1. ConservedCharge supplies a map $χ$ whose level sets are invariant under the ledger operations.

proof idea

This declaration is a structure definition with an empty proof body. It directly records the fields carrier_nonempty, carrier_countable, cost (of type AdmissibleCost), charge (of type ConservedCharge), no_free_knobs, cost_sufficient, has_composition, and composition_continuous without applying any upstream lemmas.

why it matters

The structure supplies the input interface for the Ledger Reconstruction Theorem in ClosedObservableFramework, which shows that any closed observable framework canonically carries a zero-parameter comparison ledger. It occupies the base position in the forcing chain before multilevel composition classes (HasMultilevelComposition, HasLocalComposition) and neutral-sector dynamics are derived. The definition closes the seam between the arithmetic embedding and the RCL identity used in substitutivity_from_ledger.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 8 of 8)