kernel_first_pass_certificate
plain-language theorem explainer
The first-pass Primitive Recognition Calculus kernel is inhabited: every stage of the first theorem chain has a concrete Lean witness (strength tags, traces, judgments, orbit arithmetic, integer and rational surfaces, J-cost, real completion). Full stratification and the universal-foundation certificate cite it as the delta-only floor. The proof is a structure inhabitant wiring existing certificates field by field.
Claim. The first-pass PRC kernel certificate is inhabited: nonempty strength tags, traces, and judgments; certificates for trace logic, formal-system embedding, and inevitability; orbit equivalence to $\mathbb{N}$ with faithful $+$ and $\cdot$; integer and rational surfaces with injective displays; integer order; orbit divisibility and Euclidean algorithms; a PRC $J$-cost and rational field; ring and field laws; trace-closure and real Cauchy structure; $J$-cost distance triangles; and promoted real complete ordered field, continuity, completeness, and completion-boundary certificates.
background
The Primitive Recognition Calculus rebuilds arithmetic and analysis from recognition primitives rather than positing Peano or field axioms. The first-pass kernel certificate is a bundling Prop: each stage of the analytic specification already has a concrete Lean object, without yet claiming the final inevitability theorem.
Upstream, LogicNat recovers ordinary naturals: successor is generator application, and addition and multiplication are proved associative and commutative, with toNat a ring homomorphism (recovery theorems for addition and multiplication, carrier equivalence to Nat). Distinction orbits inherit that arithmetic; signed and ratio orbits display to integers and rationals.
Local setting is Foundation.PrimitiveRecognitionCalculus.Kernel. Sibling certificates (trace logic, formal systems, inevitability, integer order, orbit divisibility, J-cost, rational field, real Cauchy and completion) are the pieces this structure assembles. Doc-comment K7/A2: the analytic specification has concrete Lean objects for each stage in the first theorem chain.
proof idea
Structure inhabitant for the first-pass kernel certificate. Nonemptiness fields close by explicit constructors: delta-only strength tag, empty trace, verifier-equality judgment, left endpoint class, DistinctionNat equivalence to Nat, integer zero, and a nonzero-denominator rational from succ zero via zero-ne-succ.
Most analytic fields are one-line plugs of named certificates (trace logic, formal system, inevitability, integer and rational ring laws, J-cost, real Cauchy and completion packages, trace-closure). Orbit arithmetic faithfulness uses toNat_add and toNat_mul. Display agreement uses balanced-iff and cross-equality-iff lemmas. A few fields are trivial (rfl for reciprocal denominator) or simpa wrappers (mul-recip-cancel). No new deep argument: assembly of already-proved stage certificates.
why it matters
This is the K7/A2 bundling step that turns a scattered first theorem chain into a single inhabited kernel Prop. Downstream, full stratification takes it as the delta-only floor (discharged field-by-field from proven theorems, no project-local axioms), and the universal-foundation conditional certificate takes it as the kernel field beside the promoted real complete ordered field.
In the Recognition framework it sits under Foundation, before cost uniqueness and universal foundation close. It does not itself force T5 J-uniqueness or the RCL; those enter through the plugged J-cost and distance certificates. It is scaffolding closure for the first-pass surface, not the final inevitability theorem (explicit in the structure doc). Parent consumers treat it as the delta-only floor of the stratification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.