AdmissibleCost
plain-language theorem explainer
AdmissibleCost encodes the minimal axioms for a comparison cost J on positive reals inside the zero-parameter ledger interface. Researchers constructing the unconditional inevitability theorem cite this structure to supply the symmetric cost component. The declaration is a structure definition whose six fields directly package reciprocal symmetry, unit normalization, strict convexity, continuity, and second-derivative calibration.
Claim. A function $J:(0,∞)→ℝ$ is admissible when $J(x)=J(x^{-1})$ for all $x>0$, $J(1)=0$, $J$ is strictly convex on $(0,∞)$, continuous on $(0,∞)$, and the second derivative of $t↦J(e^t)$ at $t=0$ equals 1.
background
The module defines the zero-parameter local conserved comparison ledger as the refined primitive object for the unconditional inevitability theorem. This ledger packages a countable carrier, local binary comparison with a symmetric cost, a conserved scalar quantity, trivial external parameters, and closure under composition. AdmissibleCost supplies the cost component, whose doc-comment states it satisfies the minimal ledger axioms of reciprocal symmetry, unit normalization, strict convexity, continuity, and calibration.
proof idea
The declaration is a structure definition that directly encodes the five axioms listed in its doc-comment as fields on the function J.
why it matters
ZeroParameterComparisonLedger consumes this interface as its cost field and serves as the central primitive for the unconditional theorem. The structure implements the J-cost from T5 of the forcing chain, with the calibration condition ensuring consistency with the phi-ladder and Recognition Composition Law. It supplies the minimal cost axioms before downstream hierarchy and factorization results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.