AdmissibleCost
plain-language theorem explainer
AdmissibleCost encodes the five minimal axioms for a comparison cost function J on positive reals inside ledger constructions. Zero-parameter emergence proofs cite this structure when assembling the conserved charge component of a comparison ledger. The declaration is a plain structure definition that directly records reciprocal symmetry, unit normalization, strict convexity, continuity, and the second-derivative calibration condition.
Claim. A function $J:(0,∞)→ℝ$ satisfying $J(x)=J(x^{-1})$ for all $x>0$, $J(1)=0$, strict convexity on $(0,∞)$, continuity on $(0,∞)$, and $d²/dt² J(e^t)|_{t=0}=1$.
background
AdmissibleCost is the structure that encodes admissible cost functions for local binary comparisons inside the zero-parameter ledger. It requires a map J from positive reals to reals obeying reciprocal symmetry, normalization at unity, strict convexity on the positive ray, continuity, and the calibration fixing the second derivative of the exponential composition at zero. This definition appears in the module that packages the Zero-Parameter Local Conserved Comparison Ledger, whose four components (countable carrier, symmetric cost, conserved charge, and composition closure) feed every downstream emergence theorem.
proof idea
This declaration is a structure definition that directly encodes the five listed properties with no further proof obligations or lemmas applied.
why it matters
AdmissibleCost supplies the cost field to the ZeroParameterComparisonLedger structure, the central primitive for the unconditional inevitability theorem. It enforces the minimal ledger axioms required for conserved quantities and composition closure, consistent with J-uniqueness in the forcing chain and the phi-ladder scaling. It leaves open the derivation of an explicit closed form for J from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.