ch:universe-paradoxes: ch:universe-paradoxes

Problem and invariant. Encode the assumption-use boundary of the Hurkens spine. Acceptance requires the four product operations, the small-universe embedding, large introduction and elimination, and large beta; it must not consult either small-beta flag.

Representation. A Boolean interface record is preferable here to a term AST: the artifact is advertised only as a dependency ledger. A term checker would need the four dependent product classifiers and conversion, which this corpus does not implement.

Build order. Start with the exact ten-flag interface. In separate cases delete ${\mathrm{\Pi }}_1$, ${\mathrm{\Pi }}_2$, ${\mathrm{\Pi }}_0$, ${\mathrm{\Pi }}_{01}$, and $u_0$. Then enable both unused small-beta flags, and finally delete large beta. Each change has one named oracle.

Observable result and mutation. The run prints eight named passes and the recorded summary. Mutate the checker so that it ignores large beta; the last negative oracle fails.

Acceptance and boundary. Run all four appendix E commands before and after restoring the mutation. Passing says only that the finite ledger matches the chapter’s declared dependency set. The mathematical proof remains lemma 76.3, theorem 76.4.