KernelFirstPassCertificate
plain-language theorem explainer
First-pass PRC kernel certificate: one Prop bundling every concrete surface in the initial theorem chain (strength tags, traces, judgments, orbit arithmetic through integers and rationals, J-cost, real-completion boundary). Cited by the delta-only floor of PRC stratification and by universal foundation certificates. Pure specification structure; inhabitance is proved separately by a field-by-field constructor.
Claim. A first-pass PRC kernel certificate asserts: nonempty strength tags, traces, and judgments; closed trace-logic, formal-system, and inevitability certificates; endpoint classes for every judgment-trace pair; distinction naturals equivalent to $\mathbb{N}$ with faithful $+$ and $\times$; inhabited PRC integer and rational surfaces with injective displays to $\mathbb{Z}$ and $\mathbb{Q}$, ring and field laws, and display-preserving arithmetic; closed order, divisibility, Euclidean, J-cost, and recognizer-bridge certificates; and the real Cauchy, null-setoid, triangle, ordered-field, and completion chain.
background
Primitive Recognition Calculus rebuilds arithmetic and analysis from recognition traces. A strength tag marks the delta-only floor; a trace is a finite recognition transcript; a judgment is a stable predicate on transcripts. Distinction naturals are the orbit carrier of iterated distinctions, with a verifier map reading off iteration count.
Signed and ratio orbits are the internal integer and rational carriers before quotienting; the PRC integer and rational surfaces are the quotients, with displays into classical $\mathbb{Z}$ and $\mathbb{Q}$. J-cost and the Recognition Composition Law enter through the J-cost and recognizer-bridge certificates, tying positive PRC ratios to $J(x)=(x+x^{-1})/2-1$.
The module packages the first theorem chain as named sub-certificates (trace logic, formal systems, inevitability, integer order, orbit divisibility, real Cauchy ledgers, null-distance setoid, triangle moduli, ordered-field promotion, real-completion boundary). This structure is that analytic specification, not its inhabitance proof.
proof idea
No proof body: the declaration is a structure of type Prop. Each field is a Nonempty existence claim, a universal algebraic identity (commutativity, associativity, distributivity, display preservation, reciprocal cancellation), or a nested certificate imported from sibling modules (trace logic, formal systems, inevitability, integer order, orbit divisibility and Euclidean arithmetic, J-cost, rational field, recognizer bridge, and the real Cauchy/null-setoid/triangle/ordered-field family through the real-completion boundary). Inhabitance is discharged elsewhere by a constructor filling every field.
why it matters
K7/A2 bundling certificate: every stage of the first PRC theorem chain has a concrete Lean object. Downstream, the inhabitance theorem constructs a value of this type. Full stratification takes it as the delta-only floor. Both universal foundation certificates carry it as the delta kernel, closing the top-level theorem with the promoted complete ordered-field surface.
In Recognition Science it marks the delta-only arithmetic floor before continuum completion: orbits give countable distinction naturals, integers, and rationals with native J-cost, while the real-completion boundary and continuum-not-forced results sit strictly above. Explicitly not the final inevitability theorem; it only certifies that first-pass surfaces exist and compose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.