tighten_L0_Lcost
plain-language theorem explainer
The gate-tightened cost class is a tightening of the continuous-candidate class: every cost meeting the five Law-of-Logic gates is continuous on the positive reals. Builders of the maximal-forcing cost-layer realization cite this to order the two admissibility classes before forcing uniqueness of J. The subset proof is a one-line projection of the continuity conjunct; the strictness witness is left as True.
Claim. There is a tightening from the class of continuous candidate costs on $(0,\infty)$ to the class of gate-admissible costs (reciprocal symmetry, normalization, the Recognition Composition Law, calibration, and continuity): every gate-admissible $F:\mathbb{R}\to\mathbb{R}$ lies in the continuous-candidate class. The optional strictness witness is the trivial proposition $\top$.
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 Law-of-Logic gates (reciprocal symmetry, normalization, RCL, calibration, continuity); the Aczel smoothness package is supplied by a proved instance, not an extra hypothesis. The claim under closure is that $F$ equals the canonical cost $J$ on the positive reals.
Two nested admissibility classes appear. The loose class consists of functions continuous on $(0,\infty)$. The tight class consists of functions satisfying the full five-gate package CostAdmissible. A Tightening from $A$ to $B$ is a structure whose core field asserts that every $B$-admissible realization is $A$-admissible; an optional strictness witness is a separate Prop so the order remains usable when strict inclusion is not yet proved.
Upstream, the Recognition Composition Law and the J-uniqueness theorem (forcing-chain T5) already pin the unique continuous cost meeting the gates to $J(x)=(x+x^{-1})/2-1$.
proof idea
The definition assembles a Tightening record. The subset field is a short tactic proof: introduce a gate-admissible $F$ and project the continuity conjunct out of the five-fold product that defines gate-admissibility (hF.2.2.2.2). No external lemmas are invoked. The strictness witness is set to True, matching the doc-comment that strictness is deferred.
why it matters
This is the first link in the cost-layer maximal-forcing scaffold (Phase 1). It places the gate-tightened class strictly inside the continuous-candidate class in the admissibility order, so later results can promote selected claims to forced invariants after tightening. Phase 2.1 discharges forced uniqueness of $J$ over the gate class by wrapping the published theorem that the Law of Logic forces the canonical cost, turning a real RS uniqueness theorem into a ForcedInvariant over an admissible class.
Framework landmarks in view: T5 J-uniqueness, the Recognition Composition Law as one of the five gates, and the cost-layer root of the maximal-forcing program. No downstream consumers are wired yet in the graph; the immediate parent pattern is the forced-register closure of the is-J claim over the gate class. The deferred strictness witness is the only open local stub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.