Machine-Checked Contracts for a Bounded Process Kernel in Lean 4

We present a bounded Lean 4 artifact that machine-checks five exact contracts, organized in four R1–R4 families, for one fixed process kernel using Lean Std without Mathlib. For the exact current interfaces, Lean proves: contractibility of fixed-source extension records from a typed process quotient into the artifact's explicit IndependentAlgebra target interface; acceptance of a finite already-resolved checker if and only if its decoded boundaries inhabit a strict square; the declared fieldwise Refines relation between the mathematical numeric payload of an already-parsed RawBundle and that checker bundle; a one-way normalized sequential white relational refinement of decoded processes; and conditional soundness of a finite provenance-DAG checker when accepted-ground truth and rule soundness are supplied. These results share a representation-boundary discipline but do not compose into an end-to-end correctness theorem. In particular, they do not verify CPython, raw JSON or UTF-8 parsing, SHA-256, filesystem access, or external reference resolution. They establish neither general free-monoidal or coherence priority, non-strict strictification, a morphism-equality decision procedure, an inverse relational comparison, provenance-created truth, nor empirical utility. The contribution is therefore a report of a bounded formal artifact and its exact theorem contracts, including nearby false propositions and explicit trust boundaries, rather than a verified implementation of an entire knowledge-representation system.