Lcost
plain-language theorem explainer
The gate-tightened cost class of candidate recognition costs F : ℝ → ℝ that meet all five Law-of-Logic gates: reciprocal symmetry, normalization, RCL, calibration, and continuity on (0,∞). Anyone building the cost-layer claim universe or the L0→Lcost tightening cites it. Pure structure packaging: the admissible set is exactly CostAdmissible.
Claim. Let $\mathcal{L}_{\mathrm{cost}}$ be the admissibility class of maps $F:\mathbb{R}\to\mathbb{R}$ whose admissible set is exactly those $F$ that are reciprocal, normalized, satisfy the Recognition Composition Law, are calibrated, and are 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}$. Admissibility is the conjunction of the five gates the Law of Logic imposes on any cost; the claim under closure is that $F$ equals the canonical cost $J$ on the positive reals.
CostAdmissible F is that five-way conjunction: reciprocal cost, normalized, satisfies the Recognition Composition Law (RCL: $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ in the canonical case), calibrated, and continuous on $(0,\infty)$. The looser class $L_0$ keeps only continuity on $(0,\infty)$.
AdmissibilityClass R is the abstract scaffold: a set of admissible realizations of type $R$ plus a label string. Different phases instantiate $R$ by logic realizations, costs, or physical models.
proof idea
Definition, not a proof. Instantiates AdmissibilityClass (ℝ → ℝ) by setting the admissible set to { F | CostAdmissible F } and fixing the label string that names the five gates. No lemmas are applied; the mathematical content lives entirely in the CostAdmissible predicate.
why it matters
Roots Phase 1 of maximal forcing in a published, sorry-free uniqueness theorem rather than a fresh axiom. It is the admissibility field of costUniverse and the class over which forced_isJ wraps law_of_logic_forces_jcost, proving Forced(Lcost, isJClaim) end to end.
Downstream, tightening_L0_Lcost_effective shows the gates do real work: isJClaim is Independent over L0 but Forced over Lcost. That is the Phase 5 legitimacy evidence for the L0→Lcost rung. Framework landmark: T5 J-uniqueness and the RCL gate that forces $J(x)=(x+x^{-1})/2-1$. Also feeds costUniverseCert, which discharges maximal_forcing_closure unconditionally for the cost universe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.