IndisputableMonolith.Foundation.MaximalForcing.RSCostUniverse
Defines the cost-function layer of Maximal Forcing: admissible costs F : R → R obey five Law-of-Logic gates, and the cost universe is the forcing closure of those gates. Anyone citing T5 (J-uniqueness) or the reality-closure certificate uses this module to pin that the only forced cost claim is "F equals J". The argument packages CostUniqueness and Aczél smoothness into a classifier and a certificate that J is forced and L0-independent.
claimA candidate cost $F:\mathbb{R}\to\mathbb{R}$ is admissible when it meets the five gate conditions the Law of Logic imposes on recognition costs. The cost universe is the forcing closure of those gates. Inside that universe the claim "$F=J$" (with $J(x)=(x+x^{-1})/2-1$) is forced, invariant, and independent over the base layer $L_0$; a classifier and certificate record that classification.
background
Maximal Forcing builds a reality-closure certificate: every claim in a forcing closure receives a definite classification. This module supplies the cost-function stratum of that program. Recognition cost is the functional that measures mismatch under reciprocal scaling; the unique continuous, symmetric, strictly convex, calibrated solution is $J(x)=\cosh(\log x)-1$, forced at chain step T5.
Upstream, CostUniqueness states that any $F$ obeying symmetry, unit normalization, strict convexity, and calibration equals $J$ on $\mathbb{R}_+$. AczélProof supplies the analytic bootstrap: continuous solutions of d'Alembert's equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ are real-analytic, which underwrites uniqueness arguments for the cost functional equation (RCL).
Locally the module introduces admissibility gates (CostAdmissible), base and cost layers $L_0$ and $L_{\mathrm{cost}}$, the claim isJClaim, the costUniverse as a forcing closure, and the certificate objects that RealityClosure expects.
proof idea
Not a single theorem: a small stack of definitions and packaging lemmas. Admissibility is the five-gate Prop on $F$. $L_0$ and $L_{\mathrm{cost}}$ are successive layers; tighten_L0_Lcost relates them. isJClaim is the proposition that the cost equals $J$. forced_isJ and isJClaim_in_closure apply CostUniqueness (and the Aczél smoothness path) inside the closure so that isJ is forced and invariant (isJForcedInvariant). costUniverse_classifier and costUniverseCert match the RealityClosure certificate interface; isJ_independent_over_L0 records independence over the base layer. No deep new analysis lives here: the hard uniqueness work is imported.
why it matters in Recognition Science
Closes the cost slot in the Maximal Forcing crown interface. RealityClosure demands, for every claim $C$ in the forcing closure, a ClaimClassification; this module produces that classification for the recognition-cost claim and the accompanying certificate. Without it, T5 (J-uniqueness via RCL, symmetry, convexity, calibration) would sit outside the forcing ledger.
Downstream the empty used_by list on this page is expected for a leaf certificate module: parent consumers are the reality-closure assembler and any audit that checks the forcing chain T5–T8. Framework landmarks hit directly: T5 J-uniqueness, the Recognition Composition Law, and the identification $J(x)=\cosh(\log x)-1$. Scaffolding risk is low if CostUniqueness and AczélProof remain sorry-free; the open obligation is only wiring this certificate into the final forall-C classification theorem stated in RealityClosure.
scope and limits
- Does not re-prove J-uniqueness; imports CostUniqueness and Aczél smoothness.
- Does not force spacetime dimension, eight-tick period, or phi; only the cost layer.
- Does not assert the final RealityClosure forall-C theorem; only the cost-universe certificate.
- Does not treat discrete or non-measurable costs outside the five admissibility gates.
- Does not derive particle masses, alpha, or rung formulas from the cost universe.