prc_full_stratification
plain-language theorem explainer
Under Aczél smoothness, the full PRC stratification is inhabited: a single checked ledger of what the δ-native calculus forces versus what stays free or needs completion. Anyone citing the forced-versus-assumed boundary for native cost uniqueness uses this object. The proof is a term-mode structure constructor that wires eight already-proved certificates field by field, with no project-local axioms.
Claim. Assuming the Aczél smoothness package (every continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^\infty$), the full PRC stratification holds: the kernel first-pass certificate; the trace-closure boundary; the $\delta$-native carrier strictly below its completion ($\exists x\in\mathbb{R},\,x^2=2$, yet no ratio-orbit squares to $2$); the continuum not $\delta$-forced; $J$-cost strength separation; joint forcing of the cost form; residual cost freedom exactly one real parameter; and $J$ forced by reciprocal symmetry, normalization, composition, unit calibration, and monotonicity of the log-transform alone.
background
Primitive Recognition Calculus (PRC) works on a $\delta$-native carrier built from distinction naturals and ratio orbits (rational multiplicative characters), not on $\mathbb{R}$ a priori. The completion is ordinary $\mathbb{R}$; the gap is witnessed already by $\sqrt{2}$, which exists in $\mathbb{R}$ but not as the real image of any RatioOrbit.
Cost uniqueness is organized around the recognition cost $J$, classically $J(x)=(x+x^{-1})/2-1$, obeying the Recognition Composition Law. The monotone route replaces continuity of the log-transform $H_F$ by monotonicity on $[0,\infty)$, together with reciprocal symmetry, normalization, composition, and unit calibration $G''(0)=1$.
The module assembles an honest forced-versus-free ledger. Upstream, kernel_first_pass_certificate supplies the $\delta$-only floor; prc_completion_strictly_extends_carrier and prc_continuum_not_forced separate carrier from continuum by cardinality and the missing square root; prc_cost_joint_stratification and prc_cost_freedom_is_one_real pin the cost form and residual freedom; law_of_logic_forces_jcost_monotone is the order-only $J$-forcing capstone. The only typeclass hypothesis is AczelSmoothnessPackage (continuous d'Alembert solutions are $C^\infty$), a proved instance, not an axiom.
proof idea
Term-mode inhabitant of the structure PRCFullStratification. Each field is filled by a named theorem:
delta_only_floor←kernel_first_pass_certificatecompletion_boundary←trace_closure_certificatecarrier_strictly_below_completion←prc_completion_strictly_extends_carrier(existence of $\sqrt{2}$ in $\mathbb{R}$, irrationality blocking ratio orbits)completion_not_forced←prc_continuum_not_forcedjcost_strength_separation←prc_jcost_strength_separationcost_form_forced←prc_cost_joint_stratificationresidual_freedom_is_one_real← lambda wrappingprc_cost_freedom_is_one_realjcost_forced_order_only← lambda wrappinglaw_of_logic_forces_jcost_monotone
No new algebra; the work is discharge-by-reference under the Aczél smoothness instance.
why it matters
This is the top-level "what is forced versus assumed" object for PRC native cost uniqueness, reconstructed after an earlier UniversalFoundation edit was reverted. It supersedes scattered per-stratum prose with one checked proposition assembled only from proved theorems.
In the Recognition forcing chain it sits at the cost-uniqueness joint that feeds T5 ($J$-uniqueness via the composition law and calibration). The order-only forcing field is the completeness-free analogue of classical continuous $J$-forcing: monotonicity of the log-transform replaces ContinuousOn, so $J$ is pinned without assuming the continuum up front. Carrier-versus-completion and continuum-not-forced fields make explicit that $\mathbb{R}$ is a completion choice, not a $\delta$-native theorem, while residual freedom collapses to a single real once the joint cost stratification is in place.
Downstream consumers read this ledger rather than re-proving the strata. The structure is the stable citation point for any argument that must distinguish kernel floor, trace boundary, cost form, and the one-real residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.