Pith. sign in
module module moderate

IndisputableMonolith.Foundation.MaximalForcing.RSCostUniverse

show as:
view Lean formalization →

Packages the cost-function layer of Maximal Forcing: admissible recognition costs F : ℝ → ℝ under the five Law-of-Logic gates, base and cost universes L₀ and L_cost, and the forced claim that the unique cost is J. Foundation work cites it when wiring T5 uniqueness into the reality-closure certificate. Structure is definitional universes plus classifier lemmas routed through CostUniqueness and Aczél smoothness.

claimA candidate cost $F:\mathbb{R}\to\mathbb{R}$ is admissible when it satisfies the five gate conditions the Law of Logic imposes on any recognition cost. The cost universe is the forcing universe obtained by adjoining the claim that $F=J$, where $J(x)=\frac{x+x^{-1}}{2}-1$ on $\mathbb{R}_+$, to a base layer $L_0$. The module records that this is-$J$ claim lies in the reality closure, is forced, and is invariant, and supplies a classifier certificate for that universe.

background

Recognition Science forces the recognition cost from functional axioms rather than fitting it. The unique target is $J(x)=\cosh(\log x)-1=\frac{x+x^{-1}}{2}-1$ on $\mathbb{R}_+$ (forcing step T5). Upstream CostUniqueness states the consolidated theorem: any $F$ with symmetry, unit normalization, strict convexity, and calibration equals $J$ on the positive reals. Aczél smoothness supplies the analytic bootstrap: continuous solutions of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ are $C^\infty$ (in fact real analytic), which underwrites the regularity side of uniqueness.

This module sits in Maximal Forcing. RealityClosure is the crown interface: it does not assert the final theorem, but states the certificate shape $\forall C\in\mathrm{ForcingClosure}(P,U),,\mathrm{ClaimClassification}(U,C)$. The cost layer is the fragment of that program that treats candidate costs as claims inside a universe, with admissibility as the gate predicate and $L_0\subseteq L_{\mathrm{cost}}$ as the ambient layers.

proof idea

Definition-and-classifier module, not a single deep proof. It introduces CostAdmissible (the five-gate predicate on $F$), the base layer $L_0$ and cost layer $L_{\mathrm{cost}}$, and a tightening map relating them. The is-$J$ claim is packaged as a forcing claim; costUniverse is the corresponding universe. Lemmas then place that claim in the reality closure, record that it is forced and invariant, and emit a classifier certificate. Uniqueness content is imported from CostUniqueness (T5) and regularity from AczélProof; local work is universe bookkeeping and claim classification rather than a fresh functional-equation argument.

why it matters in Recognition Science

Closes the cost-function slot inside Maximal Forcing so the reality-closure certificate can treat "the cost is $J$" as a classified, forced claim rather than an external hypothesis. That is exactly T5 (J-uniqueness) in universe form, aligned with the Recognition Composition Law and the forcing chain. Downstream consumers are closure and classifier constructions in the Maximal Forcing program (RealityClosure's certificate interface); this module has no further used_by edges yet, so it is a leaf supplier of the cost-universe certificate. Without it, the crown closure would still carry an unclassified cost axiom.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (13)