L0
plain-language theorem explainer
The loosest admissibility class of candidate recognition costs: real functions continuous on the positive reals. It is the baseline rung of the cost-layer maximal-forcing ladder, against which the five-gate class is a genuine tightening. Anyone citing independence of "equals J" over continuous candidates, or the L0-to-gate tightening certificate, uses this class. The body is a one-line structure instance fixing the admissible set and a label string.
Claim. Let $L_0$ be the admissibility class of candidate costs $F:\mathbb{R}\to\mathbb{R}$ whose admissible set is exactly the continuous functions on $(0,\infty)$, with label "continuous candidate costs on $(0,\infty)$".
background
The 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. An AdmissibilityClass is an abstract pair (admissible set, label string) so different phases can instantiate logic, cost, or physical carriers.
Recognition costs are constrained by five Law-of-Logic gates (reciprocal symmetry, normalization, the Recognition Composition Law, calibration, and continuity). Continuity alone is the weakest of these; the full conjunction is packaged later as gate-admissibility. Upstream cost notions (event J-cost, ratio-weighted multiset cost, multiplicative-recognizer derived cost) all live in this same functional layer.
$L_0$ is deliberately the loose baseline: every continuous positive-domain candidate is in, with no algebraic gate imposed yet.
proof idea
Definitional structure instance, not a proof. The admissible field is the set comprehension ${F\mid \mathrm{ContinuousOn}, F,(0,\infty)}$; the label is the fixed string naming that class. No lemmas are applied.
why it matters
Anchors Phase 1 of cost-layer maximal forcing. Downstream, the five-gate class is defined as a tightening of $L_0$ (every gate-admissible $F$ is continuous), and the independence theorem shows "equals $J$" is free over $L_0$: $J$ itself is continuous and satisfies the claim, while the zero function is continuous and fails it.
The legitimacy theorem then pairs that independence with forcedness over the gate class, proving the $L_0\to$ gate rung is not cheap tightening. That is the Phase 5 per-step evidence the ladder requires. The cost-universe closure certificate and classifier also reference $L_0$ as the open end of the chain. Framework landmark: this is the cost-side entry point that eventually wraps the published uniqueness theorem forcing $J(x)=(x+x^{-1})/2-1$ (T5 / RCL uniqueness) once the gates are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.