Logic enrichment and erased dependency: executable records
All five corpora target the installed Kappa v0.3.0 executable with SHA-256 5b9b64cac3cd2b43f381d085b46d248924bcc3a5e65cb5a987d44e7d5833c6b6. Each is private by default, exports only main, passes the four repository-root commands below, and returns [] from audit.
Chapter 92: predicativity classifier
Reproducibility record for exercise 92.6. The corpus is artifacts/ch92-ltt-predicativity-classifier/corpus.kp; accepted SHA-256 is b19c572d992a8c671827f4a14cb523fb1989107c2debc2bf9996e61f56c37142. Run From the directory printed above, run kappa check corpus.kp, then kappa test corpus.kp, kappa run corpus.kp, and kappa audit corpus.kp. The run prints five named PASS lines and ends All 5 Chapter 92 corpus cases passed. Replacing the comprehension classifier by analyticity makes the set-quantifier oracle fail and the test exit 1. This is finite syntax evidence, not the conservativity theorem.
Chapter 37: same-erasure admission
Reproducibility record for exercise 93.6. The corpus is artifacts/ch93-dependent-intersection-erasure-checker/corpus.kp; accepted SHA-256 is 1dfc9bfc35edb0ae99ed971198d344c1b1d1666789b15b29c6b4de496d60046f. Apply kappa check, test, run, and audit to that path. The run ends All 4 Chapter 93 corpus cases passed. Removing the same-erasure conjunct admits the unequal pair and makes the test exit 1. This does not prove PER soundness or normalization.
Chapter 94: polarity and subject
Reproducibility record for exercise 94.5. The corpus is artifacts/ch94-system-s-self-positivity-checker/corpus.kp; accepted SHA-256 is 8ef0beeec251b413b1312b469ed4465c86a7df200fb5a11ab8f8880061c5a0cc. The four standard commands pass; the run ends All 5 Chapter 94 corpus cases passed. Removing the arrow-domain polarity reversal makes the negative-arrow oracle fail and the test exit 1. The corpus is not a System S metatheory mechanization.
Chapter 95: predecessor order
Reproducibility record for exercise 95.6. The corpus is artifacts/ch95-very-dependent-order-checker/corpus.kp; accepted SHA-256 is de8962db7eeaa6b000c8b52601fc2981defc451bfcbb9d32a39a4361c3e2cae2. The four standard commands pass; the run ends All 5 Chapter 95 corpus cases passed. Replacing strict comparison by nonstrict comparison makes the self-edge and visibility oracles fail and the test exit 1. The finite label checker does not construct Hickey’s PERs.
Chapter 38: finite zero-cost observations
Reproducibility record for exercise 96.6. The corpus is artifacts/ch96-cdle-zero-cost-runtime/corpus.kp; accepted SHA-256 is f4c605706e3ca94ec26cdd9d9e2e9042aae0e0453fe3e138b4f18d6b6be39859. The four standard commands pass; the run ends All 5 Chapter 96 corpus cases passed. Unconditional intersection admission accepts the copying/identity pair and makes the test exit 1. These observations prove none of CDLE soundness, consistency, monotone recursion, or the generic reuse theorem.