PRCShrunkCertificate
plain-language theorem explainer
Seven headlines of the δ program, bundled as one Prop: recognition has a single primitive, the cost form is forced up to gauge with curvature-1 member J, named RS constants and the φ/eight-tick/D=3 scaffold live in a countable proper subfield of ℝ closed under the needed operations, the RS chain is fed by calibrated δ-cost, and every reflexive formal system is degenerate or realizes δ. Foundation auditors cite this as the shrunk PRC certificate interface. It is a structure of propositions; inhabitation is a separate theorem.
Claim. A certificate asserting: (A) any exclusive trace judgment that always distinguishes the two endpoints coincides with endpoint equality and with the unique one-primitive act judgment; (B) second derivative of $\cosh(ct)-1$ at $0$ is $c^2$, positive scales are unique for that map, and curvature $1$ forces $c=1$; (C) the minimal RS field is a countable proper subset of $\mathbb{R}$ containing $\varphi$, $\pi$, $e$, and $\alpha^{-1}$; (D) second derivative of $J_{\mathrm{cost}}(e^t)$ at $0$ is $1$ with $\varphi$ in that field; (E) all $\varphi^n$, and scalars $8$ and $3$, lie in the field; (F) some countable proper subfield closed under $\exp$ and $\log$ contains $\pi$, $\varphi$, $e$, $\alpha^{-1}$; (G) every reflexive formal system is degenerate or realizes $\delta$.
background
The Primitive Recognition Calculus packages the δ program: derive comparison from one recognition act, force the cost functional, and keep the RS scaffold on a countable carrier strictly below the continuum.
The cost in view is the curvature-normalized $J(x)=\cosh(\log x)-1$, equivalently $(x+x^{-1})/2-1$ (T5). Calibration records that the second derivative of $\cosh(ct)-1$ at $0$ is $c^2$, so the argument unit is a gauge and curvature $1$ pins $c=1$. The Recognition Composition Law sits behind uniqueness of this form.
The minimal RS field is the countable set of reals generated for named constants; it must hold $\varphi$, $\pi$, $e$, and the constructed $\alpha^{-1}$, yet not equal $\mathbb{R}$. Upstream constants in scope include RS-native $G$, bridge ratio $K=\varphi^{1/2}$, tick $\tau_0=1$, and spatial dimension $D=3$. Distinction dichotomy classifies reflexive formal systems as degenerate or as realizing $\delta$.
proof idea
No proof body: this is a Prop-valued structure whose seven fields are the certificate headlines. Nothing is discharged here.
Inhabitation is the sibling theorem that the δ-program certificate holds. That theorem assigns each field to a named upstream result: comparison-is-derived (one primitive), calibration-unit-is-a-gauge (cost form and free unit), rs-physics-below-continuum (countable proper field with $\varphi,\pi,e,\alpha^{-1}$), delta-cost-feeds-rs-chain (curvature-1 entry of $J_{\mathrm{cost}}\circ\exp$), plus the scaffold-in-field, exp-log-closed subfield, and distinction-dichotomy lemmas from the imported PRC modules. Several of those assignments are still the closing path for the scaffold status.
why it matters
Single citation target for the shrunk δ-program certificate. The parent theorem is exactly the claim that this structure is inhabited, advertised as seven proved headlines with no axioms.
In the Recognition framework it compresses the bridge from T5 $J$-uniqueness and the RCL cost form to the countable-carrier thesis: integer powers of $\varphi$ (the φ-ladder), the eight-tick octave (scalar 8), and $D=3$ all sit in the same countable field that already holds $\pi$, $e$, and $\alpha^{-1}$. Headline (G) is the classification half of Item 4: a reflexive foundation cannot avoid $\delta$ without degeneracy.
The module frames this as the load-bearing statements of the δ program as one small object. Fully discharging every field without sorry is what promotes the scaffold to a proved certificate; open infrared boundary data on $\alpha^{-1}(0)$ remain outside this bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.