pith. sign in
class

CostFunctionalAxioms

definition
show as:
module
IndisputableMonolith.Foundation.CostAxioms
domain
Foundation
line
82 · github
papers citing
1 paper (below)

plain-language theorem explainer

The CostFunctionalAxioms class packages the three primitive axioms that any cost functional must obey in Recognition Science. A researcher deriving uniqueness of the J functional or symmetry properties would cite this bundle to access normalization, the recognition composition law, and calibration at once. It is realized as a class extension over the three separate axiom classes with no further proof obligations.

Claim. A function $F: (0,∞) → ℝ$ satisfies the cost functional axioms when it obeys normalization $F(1)=0$, the recognition composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all $x,y>0$, and calibration $d^2/dt^2 F(e^t)|_{t=0}=1$.

background

The module CostAxioms formalizes the primitive foundation of Recognition Science. It introduces three axioms: Normalization requires that the cost at unity vanishes, $F(1)=0$; Composition encodes the recognition composition law, the multiplicative form of d'Alembert's equation; Calibration fixes the curvature by requiring the second logarithmic derivative at zero to equal one. These axioms are more primitive than logic, encoding economic inevitability where low-cost configurations correspond to consistency. Upstream, the canonical arithmetic object supplies the initial Peano structure, but the cost axioms stand independently.

proof idea

This declaration is a one-line wrapper that extends the Normalization, Composition, and Calibration classes to form the complete axiom bundle for a cost functional.

why it matters

This axiom bundle is the starting point for the uniqueness theorem uniqueness_specification, which establishes that any sufficiently regular function satisfying these axioms equals the canonical J. It fills the T5 uniqueness step in the forcing chain, where J-uniqueness follows from the recognition composition law. The bundle enables derivation of symmetry and non-negativity properties used throughout the framework, including the mass formula and Berry creation threshold.

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

papers checked against this theorem (showing 1 of 1)