Proof Foundation

This document defines the logical core zerg-proof/1. The notation below is metasyntax; source notation is defined in proof language. E ; G |- t : A means that term t has type A in global environment E and local telescope G. A telescope is an ordered list of typed bindings; later bindings may depend on earlier ones. Substitution is capture-avoiding.

C3-PROOF-001 — Kernel and completed proofs

The kernel checks a closed environment, an expected proposition P, and a completed term p, establishing E ; [] |- P : Prop and E ; [] |- p : P. The expected proposition is supplied by the claimant’s verifier or admission policy, not replaced by whatever proposition the submitted term proves. Parameters and hypotheses must be bound in P or disclosed in E.

Parsing, elaboration, proof search, tactics, model generation, external solvers, artifact transport, and caches are untrusted producers of kernel input. The kernel independently validates declarations, types, reductions, and dependency closure. It must not accept a producer’s claimed type, termination result, axiom list, or native evaluation result without checking the appropriate term. Proof terms contain no holes, unresolved metavariables, sorry, IO, unsafe operations, runtime object pointers, or calls into an execution engine.

C3-PROOF-002 — Universes and core terms

Levels are 0, parameters, succ(u), max(u,v), and imax(u,v). Assignments map every parameter to a natural number. max is maximum; imax(u,0)=0, and imax(u,v)=max(u,v) when v>0. Level equivalence means equality under every assignment. No inequalities or unsolved constraints are assumed at declaration acceptance. An implementation must decide the generated level equalities or return resource exhaustion, never assume equality.

Prop = Sort(0); Type(u) = Sort(succ(u)). Universes are noncumulative: Sort(u) : Sort(succ(u)), not Sort(u) : Sort(u) and not arbitrary larger sorts by subtyping. Explicitly defined lifting types may bridge universes.

Core terms are local variables, universe-instantiated global constants, Sort(u), dependent products Pi(x:A,B), abstractions Lam(x:A,t), applications App(f,a), and typed lets Let(x:A,a,t). Inductive types, constructors, and generated recursors are global constants. There is no primitive general fixed point, rewrite axiom, foreign function, or evaluator.

C3-PROOF-003 — Typing judgments

An environment and local telescope must be well formed before using a rule. All premises are checked, including the well-formedness of dependent types.

Form	Premises	Result
Variable	x:A in G	x:A
Sort	u well formed	Sort(u):Sort(succ(u))
Constant	accepted declaration c.{us}:A; exact arity of level substitution ls	c.{ls}:A[ls/us]
Product	A:Sort(u); under x:A, B:Sort(v)	Pi(x:A,B):Sort(imax(u,v))
Abstraction	product well formed; under x:A, t:B	Lam(x:A,t):Pi(x:A,B)
Application	f:Pi(x:A,B); a:A	App(f,a):B[a/x]
Let	A:Sort(u); a:A; under x:A, t:B	Let(x:A,a,t):B[a/x]
Conversion	t:A; B:Sort(u); A definitionally equal to B	t:B

Product formation is impredicative only when its result is a proposition. No source annotation can turn an arbitrary computation into a proof or waive one of these premises.

C3-PROOF-004 — Definitional equality

Definitional equality is the least typed congruence containing alpha-renaming, equivalent universe levels, beta reduction of application to abstraction, zeta reduction of lets, delta unfolding of accepted transparent definitions, and iota reduction of a generated recursor on its matching constructor. Additionally, if P:Prop and p:P and q:P, then p and q are definitionally equal (proof irrelevance). This rule cannot establish p:P in the first place and does not identify distinct propositions.

There is no function/record eta conversion in this initial core, no reduction of axioms or opaque declarations, and no equality derived from approximate numeric execution. Constants with checked opaque bodies remain typed but do not delta-reduce. A theorem is opaque after its body is checked. Its full body remains available for independent validation and assumption accounting.

Conversion must not invoke runtime code, a model, or an external oracle. Checkers may impose explicit node, depth, memory, and reduction budgets; exceeding one returns inconclusive, never equality or inequality evidence.

C3-PROOF-005 — Inductive families and positivity

An inductive declaration has fixed parameters ps, indices is, a result sort, and finitely many constructors. A constructor telescope ends in exactly the declared family I ps actual_indices. Parameters in every recursive occurrence must be the same variables, in the same order. Constructor names are fresh; all free names must be parameters, earlier fields, or accepted globals. Result indices and nonrecursive field types must not contain I.

The initial profile admits a single family per declaration, with recursive fields of form Pi(xs:As, I ps js) including the zero-binder case. None of As or js may contain I; delta expansion is used before this check. Occurrences to the left of such a function arrow, under an arbitrary type constructor, or in another field’s type are rejected. Nested and mutually recursive declarations are outside this initial profile rather than admitted by a trusted positivity annotation. Parameters and indices are themselves checked without the new family in scope.

For a data family in Sort(succ(u)), every constructor field type must inhabit a sort of level at most succ(u) under all universe assignments. This restriction does not bound fixed type parameters merely because their parameter type is a larger universe; it bounds the types of stored fields. Propositional families may quantify over arbitrary universes, subject to the elimination restriction below.

C3-PROOF-006 — Recursors and proposition elimination

The kernel generates a dependent recursor, never accepts an unchecked recursor signature. Given a motive M : Pi(is, Pi(v:I ps is, Sort(w))), each constructor branch takes its original fields plus one induction hypothesis per recursive field. For r : Pi(xs:As, I ps js), that hypothesis has type Pi(xs:As, M js (r xs)). The branch returns M actual_indices (ctor ps fields). Applying the recursor to that constructor reduces to its branch with these fields and recursively constructed hypotheses, preserving binder order.

A data family can eliminate into any well-formed target sort. A Prop family can always eliminate into Prop. Elimination into data is allowed only for an empty family, or a single-constructor family whose every field after fixed parameters is itself a proof (A:Prop). Constructor result indices remain fixed expressions in the parameters/fields. Thus False, True, conjunction, and identity permit this restricted elimination, whereas disjunction and an existential carrying a data witness do not. An opaque axiom of existence does not acquire an executable projection through this rule.

C3-PROOF-007 — Definitions and termination

Global declaration dependencies are acyclic, apart from the checked inductive family/constructor/recursor cluster. A definition is accepted only after its body checks against its declared type without that definition in scope. Surface recursion must elaborate into recursors. Structural recursion uses the corresponding constructor substructure; well-founded recursion supplies a checked accessibility proof and elaborates through its inductive recursor. Termination annotations alone do not add a kernel rule.

General-recursive Algorithm functions remain valid runtime programs under their own edition rules; they cannot be imported as transparent Proof terms. Their operational behavior can instead be represented by the explicit models in verification, including divergence.

C3-PROOF-008 — Assumptions and classical profiles

The default constructive profile permits no extra axioms. Typed local hypotheses are legitimate conditional premises, not proof of those premises. Global axioms are always named, typed constants associated with a named profile and lacking a reduction rule. A caller must explicitly admit their transitive footprint. The presence of an axiom in an imported module does not automatically make it an allowed assumption for every obligation.

The standard opt-in profiles add only the following principles, using the library definitions of Or, Not, Exists, and Nonempty:

Profile	Axiom schema
classical-em	forall (P:Prop) -> Or(P, Not(P))
classical-choice	forall (A:Type(u)) -> forall (h:Nonempty(A)) -> A
classical	Union of classical-em and classical-choice

Nonempty(A) is a Prop family with constructor A -> Nonempty(A) and no data eliminator. The choice constant has no computational reduction. Function extensionality and proposition extensionality are not implicit consequences or built-ins of these profiles; a package needing them must name and disclose separate custom axiom profiles. Custom profiles, including inconsistent ones, do not obtain a consistency guarantee from type checking. Policies may reject them entirely. A theorem using axiom bad : False is conditional on bad, never an unconditional proof of everything.

C3-PROOF-009 — Footprints and claims

The checker derives the axiom footprint from the complete transitive closure of the statement’s and proof’s referenced declarations, including types and opaque bodies. It includes imported assumptions; dead references are not silently erased to reduce the reported footprint. Required profile lists are allowlists, not author-supplied claims about which axioms were actually used. The receipt identifies the kernel semantics, actual checked environment, statement, proof, derived footprint, and checker implementation separately.

checked means derivability under that environment. rejected means this input did not meet a checking rule. unsupported means the requested profile is unavailable. inconclusive means a resource limit prevented a result. A rejected proof is not a disproof of its statement; a disproof requires a checked negation or a counterexample satisfying the declared semantic model. Consistency, normalization, and adequacy of the chosen foundation are explicit metatheoretic obligations, not facts certified merely by this document.