costUniverse
plain-language theorem explainer
The cost-layer claim universe packages candidate recognition costs F : ℝ → ℝ as realizations, with gate-class admissibility Lcost and the singleton claim that F equals the canonical J-cost on (0, ∞). Anyone citing maximal-forcing closure for the Law of Logic cost theorem uses this universe as the ambient ClaimUniverse. It is a pure structure instance: Realization, admissibility, and claims are filled in by definition, with no proof obligation.
Claim. The cost-layer claim universe is the triple whose realizations are maps $F : \mathbb{R} \to \mathbb{R}$, whose admissibility class is the five-gate class (reciprocal symmetry, normalization, Recognition Composition Law, calibration, continuity), and whose claim set is the singleton $\{F = J \text{ on } (0,\infty)\}$.
background
Maximal forcing works over a ClaimUniverse: a carrier of realizations, an admissibility class on that carrier, and a set of reality claims to close under a primitive. This module is the first concrete instantiation. Realizations are candidate recognition costs $F : \mathbb{R} \to \mathbb{R}$.
Admissibility is the gate class Lcost: the conjunction of the five conditions the Law of Logic imposes on any cost (reciprocal symmetry, normalization, the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, calibration, continuity). The Aczél smoothness package that upgrades continuous d'Alembert solutions to $C^\infty$ is a proved instance from Cost.AczelProof, not an extra hypothesis.
The single claim under closure is isJClaim: $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$ is the canonical cost forced by T5 uniqueness.
proof idea
Pure definitional instance of ClaimUniverse. The three fields are set by hand: Realization is ℝ → ℝ, admissibility is the gate class Lcost, and claims is the singleton set containing isJClaim. No tactics, no lemmas, no proof body beyond field assignment.
why it matters
This is Phase 1 of the cost-layer maximal-forcing scaffold: the ambient universe on which Phase 2.1 wraps the published uniqueness theorem law_of_logic_forces_jcost into a ForcedInvariant. Downstream, isJClaim_in_closure places the claim in the closure, forced_isJ / isJForcedInvariant record forcedness, costUniverse_classifier classifies every claim in the closure, and costUniverseCert discharges maximal_forcing_closure unconditionally for this universe.
Framework landmark: T5 J-uniqueness and the Recognition Composition Law, packaged so a real RS theorem becomes the first populated forced-register slot rather than a fresh assumption. The module doc states the intent explicitly: root the program in an existing sorry-free uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.