Primary references and the accepted foundation, autonomy and assurance tradeoffs.
Proof and Intent: Prior Art and Decisions
Status: informative design rationale. Normative meaning belongs to the C3 clauses and grammar, not to a changing external implementation.
Primary references consulted on 2026-09-09:
- Lean reference: universes informs the separate Prop/data universes, impredicative propositions, universe polymorphism, and noncumulative universe choice. Zerg specifies its own rules and serialization; it does not inherit future Lean changes.
- Lean reference: inductive types informs constructor/recursor checking and strict positivity. Zerg’s first profile deliberately restricts nested/mutual declarations and does not claim source or kernel-term compatibility.
- Validating a Lean proof informs the separation of untrusted proof production, small-kernel checking, the exact challenge, and disclosed assumptions. A proof of a different proposition or a hidden axiom is not acceptable evidence for the requested obligation. These sources are comparison material, not a Lean dependency.
Decision ledger
| Decision | Chosen behavior and reason |
|---|---|
| Proof’s primary purpose | Verification across existing paradigms, with standalone mathematics as a foundation |
| Foundation ownership | Zerg-owned dependent type theory; no mandatory Lean checker or imported acceptance authority |
| Logic default | Constructive; named opt-in classical profiles and visible transitive assumptions |
| Conversion | Explicit core reductions and proof irrelevance; no primitive quotient or eta rule in the first core |
| Extraction | Computational witnesses with checked erasure/representation; not arbitrary theorems or bare existence |
| Ninth paradigm | Keep Intent as both prose authority and explicit runtime resolution; no implicit comment execution |
| Runtime products | Checked code and typed plans composed from existing checked operations |
| Approval | Policy-delegated human or agent endorsement; autonomy does not require a human gate |
| Assurance | Explicit per-obligation mix, with mandatory proofs failing closed and evidence kinds kept distinct |
| Runtime scope | Explicit host effect/capability, bounded providers/context/actions, recorded replay and revisions |
| Artifact strategy | Logical ZLM4 and canonical identity framing now; physical container packing later |
| Compatibility | Additive Core-3 preview; old editions/artifacts and natural-language authority retain their meaning |
The relevant intuition is propositions-as-types: a completed proof term inhabits the requested proposition, and composition checks that each premise matches. It is not a rule that arbitrary typed programs are true, nor a consequence of Gödel’s incompleteness results. No terminating proof-search procedure is promised to decide every proposition. A checked theorem is conditional on its logic, definitions, and assumptions; empirical model validation is a different kind of evidence.
The spectrum is useful for organizing intent, justification, and realizations, but does not prove English-to-formal faithfulness or guarantee a physical implementation. Formalization approval, semantic-model adequacy, backend preservation, and live action authority remain explicit boundaries precisely because a proof kernel cannot settle them merely from an English request.