PRCFullStratification
plain-language theorem explainer
Packages the full honest forced-versus-assumed ledger for the primitive recognition cost program as one Prop-valued structure with eight fields. Anyone citing T0 continuum non-forcing, J-strength separation, or residual gauge freedom should quote this object. It is a definitional assembly of already-proved certificates, not a new derivation.
Claim. A proposition with eight strata: distinction alone forces the native number tower and rationals; continuous completion is a trace-closure commitment that strictly extends the carrier ($\sqrt{2}$ in $\mathbb{R}$, not in ratio orbits); the continuum is not distinction-forced; $J$ is unforced on the carrier yet selected on the completion; algebraic laws force the cost form to the gauge orbit $\{F_c:c>0\}$; residual freedom is exactly one positive real; and a reciprocal, normalized, composition-law, unit-calibrated $F$ with monotone log-transform equals $J(x)=(x+x^{-1})/2-1$ on positives without continuity.
background
The Primitive Recognition Calculus asks what a bare distinction act forces before any continuum or cost is assumed. The native carrier is the distinction-generated number tower (isomorphic to the naturals) and its rational field of ratio orbits; the continuous completion is a separate commitment.
The recognition cost is $J(x)=(x+x^{-1})/2-1$, equivalently $H(x)=J(x)+1=\frac12(x+x^{-1})$, under which the Recognition Composition Law becomes d'Alembert's equation. The gauge family is $F_c(x)=J(x^c)$ for $c>0$. Aczel smoothness says continuous d'Alembert solutions with $H(0)=1$ are smooth (cosh or constant).
Upstream certificates already discharge each stratum: kernel first-pass (distinction-only floor), trace-closure boundary, continuum non-forcing (countable native index versus uncountable reals), $J$-strength separation, and joint cost stratification (form forced, unit a gauge).
proof idea
No proof body: this is a Prop-valued structure whose eight fields are the stratification claims. Inhabitation is deferred to the sibling theorem that fills each field by a named certificate (kernel first-pass, trace-closure, completion strictly extends carrier, continuum not forced, $J$-strength separation, cost joint stratification, residual one-real freedom, and order-only $J$ selection), under an Aczel smoothness instance that is itself proved rather than axiomatic. The structure only fixes the interface.
why it matters
This is the top-level forced-versus-assumed object for the distinction program, superseding scattered per-stratum prose and restoring a stable full-stratification target. Downstream, one theorem inhabits it field-by-field with no project-local axioms.
Framework landmarks: it records the negative T0 answer (continuum not distinction-forced; obstruction is the cardinality gap), places T5 $J$-uniqueness strictly above the carrier via strength separation, and isolates residual freedom as one positive real after the composition law, reciprocity, and normalization force the form. The final field removes continuum analysis even from selecting canonical $J$: monotone $H$ plus calibration suffice. Open bookkeeping is closed; the scientific residual is the explicit gauge unit distinction does not fix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.