CostAdmissible
plain-language theorem explainer
A real function F is cost-admissible when it meets the five Law-of-Logic gates on recognition costs: reciprocal symmetry, F(1)=0, the Recognition Composition Law, quadratic calibration at the identity, and continuity on (0,∞). The maximal-forcing cost universe cites this as the gate predicate for the tightened class Lcost. Pure conjunction definition with no proof content.
Claim. A function $F:\mathbb{R}\to\mathbb{R}$ is cost-admissible when $F(x)=F(1/x)$ for all $x>0$, $F(1)=0$, $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all $x,y>0$, the second derivative of $t\mapsto F(e^t)$ at $0$ equals $1$, and $F$ is continuous on $(0,\infty)$.
background
This module is the first concrete maximal-forcing realization: the carrier is a candidate recognition cost $F:\mathbb{R}\to\mathbb{R}$, and the claim under closure is that $F$ equals the canonical cost $J$ on the positive reals. Admissibility packages the five gates the Law of Logic imposes on any such cost.
Reciprocal cost means $F(x)=F(1/x)$ for $x>0$. Normalization is $F(1)=0$. The Recognition Composition Law (RCL) is the functional equation $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$. Calibration is $G''(0)=1$ for $G(t)=F(e^t)$, equivalently $\lim_{t\to 0}2F(e^t)/t^2=1$. The fifth gate is continuity on $(0,\infty)$.
These predicates come from the cost functional-equation layer; the Aczel smoothness package is already a proved instance from Cost.AczelProof, not an extra hypothesis here.
proof idea
Definition only: the predicate is the five-way conjunction of reciprocal cost, normalization, the composition law, calibration, and continuity on the positive reals. No tactics, no lemmas applied, no term-mode construction beyond that conjunction.
why it matters
This is the gate predicate for the tightened cost class Lcost, whose admissible set is exactly the set of cost-admissible F. Lcost is the admissibility class over which Phase 2.1 discharges Forced Lcost isJClaim by wrapping law_of_logic_forces_jcost, turning the published J-uniqueness theorem into a ForcedInvariant.
In the forcing chain this sits at T5 (J-uniqueness via the RCL and the other gates) and roots the maximal-forcing scaffold in an existing sorry-free uniqueness result rather than a fresh assumption. Downstream, costUniverse, forced_isJ, and the classifier/certification stack all ride on Lcost, which is defined directly from this predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.