Kernel checking and definition processing

The full trusted-core signature $T_{\mathsf{impl}}$ is predicative and has dependent products and sums, unit, Booleans, naturals, intensional identity, strict Russell universes, and vectors. Its external level expressions are generated by zero, successor, and maximum. The explicitness and relevance bits on product syntax are checked metadata; the typing and conversion rules do not inspect them. The auxiliary proof fragment $T_{\mathsf{el}}$ deletes Booleans, vectors, and those two bits. The bidirectional soundness and completeness results theorem 48.19, theorem 48.20 range over the full $T_{\mathsf{impl}}$ rule card. The fragment $T_{\mathsf{el}}$ is used only by later local proof arguments; it is not the signature of those two bidirectional theorems. The missing full normalization theorem recorded in proposition 110.17 therefore limits normalization and conversion decision, not the stated conditional bidirectional results.

For the full reconstructed $T_{\mathsf{impl}}$ certificate language, theorem 110.23, corollary 110.24 prove the independent annotation-recheck and kernel guarantee under the printed conversion-decision and inversion-oracle contracts. Conversion never invokes elaboration search. These results concern a checked final term; they prove nothing about arbitrary surface syntax, tactics, plugins, termination checking, or an implementation that omits the final recheck. The Kappa corpus checks eleven finite observations, including accepted application and identity certificates and rejected malformed identity eliminators, and proves none of these metatheorems.

The source-bounded comparison in convention 110.29, proposition 110.30 has two separate interfaces. Coquand’s 1996 closure checker proves semantic soundness for a $\mathsf{Type}:\mathsf{Type}$ product calculus, but proves neither termination nor completeness there. The pinned bidirectional-PCUIC development proves inference and checking soundness and completeness up to cumulativity for its global-environment-indexed judgments. Restricting the latter to a $\mathrm{\Pi }$-and-universe core, or stratifying the former’s single universe, supplies a comparison only. Neither source theorem discharges a case of the full-Timpl completeness induction.

The local reducibility signature $T_{\mathrm{\Pi }\mathbf{2}}$ has the structural and dependent-product rules, beta and eta conversion for products, Booleans, and the displayed dependent Boolean eliminator. It has no universes and no identity type. Its local Tait argument proves closed Boolean canonicity theorem 49.2; Boolean separation is proposition 49.3. The simply typed NbE interlude separately proves normalization and decidable equality only for its STLC signature, by theorem 49.29, theorem 49.33, corollary 49.34.

The chapter’s main local construction instead has the full reconstructed signature $T_{\mathsf{impl}}$: structural rules; dependent products with both binder bits, beta and eta; dependent sums with beta and eta; Unit with eta; Booleans and naturals with dependent eliminators; intensional identity with $J$; vectors with dependent induction; and strict Russell universes with explicit lifts and exactly the printed lift equations. At that exact signature theorem 111.76 proves normality, soundness, completeness, and idempotence; theorem 49.18 proves the stated closed canonicity results; corollary 49.20 decides conversion; and theorem 111.81, corollary 111.82 supply the six total conversion/head-inversion operations and demands D1, D2, and D4. These are local theorems, not consequences of the neighbouring-signature proof below. The local proof transports quotations from depth $n$ to depth $n^{\prime }$ along an explicit world embedding; ordinary weakening alone is not used for that step. Its simultaneous escape theorem includes type quotation, code quotation, and element normality, so universe escape has no reverse dependency on a later normality lemma. Every semantic membership judgment is formed at a displayed support: ${\mathsf{Elt}}_{\mathrm{\Psi }}(\alpha )\subseteq D_{\mathrm{\Psi }}\times D_{\mathrm{\Psi }}$. Thus Unit is total only on values admissible at that support, and a dependent product or sum ranges at a target $\mathrm{\Phi }$ over ${\mathsf{Elt}}_{\mathrm{\Phi }}({\mathit{\sigma }}_{\ast }\alpha )$. The membership evidence supplies both endpoint-admissibility premises needed to extend a related environment; no theorem extends an environment by an arbitrary raw value of $D$. The neutral relation is a partial equivalence relation on all admissible neutrals. Its field $K_{\mathrm{\Psi }}$ consists exactly of the neutrals whose readback is defined after every typed target weakening, and reflection is invoked only with explicit field evidence $k{\approx }_{\mathrm{\Psi }}^{\mathrm{ne}}k$.

The comparison signature $T_{\mathsf{Coq}}$ is Coquand’s cumulative category-with-families signature with structural operations, product eta, Russell universes $U_n$ satisfying ${\mathsf{Type}}_n=\mathsf{Elem}(U_n)$, and the two-element type $N_2$ with its curried recursor. The initial-model normalization construction yields decidable equality exactly at that signature, as proved in theorem 49.17. Its universe-indexed normalization fibres $U_n^{\prime }$ prevent deleting the universe structure from the proof. The construction therefore supplies no theorem for $T_{\mathrm{\Pi }\mathbf{2}}$, $T_{\mathsf{el}}$, or $T_{\mathsf{impl}}$, and neither normalization proof transfers across those signatures. The local $T_{\mathsf{impl}}$ proof does include identity and $J$; the $T_{\mathsf{Coq}}$ signature does not. General recursion, equality reflection, impredicativity, quotient computation, and arbitrary rewrite rules remain outside both endpoints.

Surface elaboration targets the explicit kernel of chapter 48. Contextual metavariables carry declaration telescopes; the direct unifier handles typed rigid decomposition and distinct-variable pattern spines, while universe constraints are finite maximum/difference problems. Soundness requires metavariable scope, a solved acyclic substitution, discharged formation guards, and independent kernel rechecking. The completeness theorem is policy-relative to the printed bidirectional and pattern fragment. It does not cover unrestricted higher-order unification, polymorphic recursion, canonical-structure search, recursive guard checking, or arbitrary universe polymorphism.

The mathematical input is a finite acyclic term graph over a finite first-order signature, with one shared node per flexible variable and a finite list of distinguished equality pairs. Valid quotients are homogeneous and acyclic. Root-class transitions construct a compact triangular MGU; the Paterson–Wegman refinement is linear only under constant-time pointer operations and monotone parent/link cursors on the explicitly stored records. The bound concerns shared recipes, not expanded substitution trees. The Kappa companion checks a finite syntactic worklist solver. Its five oracles include the compact ledger

This ledger does not implement or establish the pointer-machine bound.

The kernel remains exactly $T_{\mathsf{impl}}$; tactics add no typing or conversion rule. A goal is a well-formed context and type, a proof state is a finite list of goals plus a validation, and the primitive and tactical semantics is the finite calculus of definition 114.1, definition 114.2, definition 114.4. Primitive validity and induction over tactic evaluation prove tactic soundness theorem 114.5. Contextual metavariable closure is the separate scope theorem proposition 114.7. Deterministic certificate replay ends with an independent kernel call, so theorem 114.10 trusts neither search nor the trace. The LCF sources motivate validations and tacticals; they do not prove this finite calculus. The Kappa replayer checks only the stated finite propositional fragment. Success $T\mathsf{@}g\Downarrow (\overrightarrow{h},V)$ and failure $\mathsf{fails}(T,g)$ are distinct judgments. Choice consults failure before its right branch; repetition is exactly the ${\mathsf{Rep}}_T$ closure of validation-composing steps that strictly decrease the printed lexicographic measure. No termination claim is made for an unmeasured tactic language.

The certified simplifier has the finite ordered database of typed rewrite lemmas and well-founded order in definition 115.1. Its contextual certificate judgment is definition 115.2; its simplification algorithm is definition 115.3. Termination uses strict descent; every successful rewrite and congruence step carries a kernel equality proof, yielding theorem 115.4. The more general respectful-morphism judgment is exactly definition 115.5, definition 115.6, with preservation proved in proposition 115.7. Reflected commutative-monoid normalization is accepted only after the kernel checks the equality certificate; its local soundness theorem is theorem 115.10. The Zombie import concerns its own Coq signature. In particular, its respectful relation is binary, relating $fx$ and $f^{\prime }y$ from a witness of $R_{A}xy$; it is not a pointwise unary relation. Zombie proves neither termination of the local strategy nor any theorem after changing that signature. The Kappa corpus is finite executable evidence, not a kernel or reflection metatheory.

The local macro model distinguishes raw binders $a^{\beta }$, raw references $a_{\beta }^{\omega }$, and expanded references $a^S[o;\mathsf{src}(\omega )]$ or $a^S[o;\mathsf{new}(o_t)]$. Thus binder token, occurrence token, finite scope set, resolved origin, and provenance marker have different roles. Expansion distinguishes substituted nodes from constructed nodes, preserves the former’s caller scopes, and requires every free constructed reference to name a target origin; unresolved, ambiguous, or provenance-mismatched output is rejected. theorem 116.5 proves the resulting capture separation. The source judgment and untrusted macro signature are exactly definition 116.7; checked expansion is the separate boundary in definition 116.11; staged typing is definition 116.6; and phase-indexed substitution and expansion typing are lemma 116.8, theorem 116.10. Checked command expansion returns an ordinary kernel-checkable declaration as in definition 116.12, corollary 116.13. The ${\lambda }^{▴}$ soundness proof theorem 116.15 applies only to the exact source card convention 116.14. Neither it nor the finite Kappa scope model is a theorem about a production macro expander. The Kappa artifact checks eleven finite oracles: caller-reference preservation, locality of an introduced reference, rejection of ambiguity, origin-renaming preservation, constructed-binder provenance, nested-quotation typing, generated normal form, the analytical true branch, rejection of ill-staged syntax, beta-capture avoidance, and absent-target alpha preservation. These runs prove no general expansion theorem.

The principal calculus is the exact first-class-level system of convention 117.1: terms include level values, level abstraction and application, $\mathsf{Lift}$, and the predicate $\mathsf{Below}$, with level equality generated by zero, successor, and join. The book-owned finite-map normalizer definition 117.7 is sound and complete for that level expression fragment and makes its equality decidable lemma 117.8, lemma 117.9, corollary 117.10. The proof of theorem 117.11 supplies reducibility, the listed normalization and canonicity consequences, complete algorithmic equality, the stated restricted typing-decidability result, and extraction only under its graded-source hypotheses. The neighbouring displacement and bounded first-class-universe systems have different signatures and transfer none of those conclusions. The Kappa program checks only the finite-map normalizer.

SortPoly is the prenex sort-polymorphic pCUIC extension fixed in convention 118.1. Sort parameters range over the source’s ground sorts; elimination is governed by the displayed predicate $\mathsf{elim}(I,s)$, not inferred from a general constraint graph. The book-owned finite constraint solver definition 118.5, proposition 118.6 concerns only the finite table used in its examples. Under the source’s exact ground-sort and elimination-policy hypotheses, monomorphization preserves typing and yields the conditional equiconsistency result theorem 118.8, corollary 118.9. Stratified type theory convention 118.11 is an independent comparison card. The other independent comparison is bounded sort polymorphism: definition 118.12, theorem 118.13 fixes its three graph-validity conditions and proves dominant-ground-substitution preservation, elaboration principality, ground monomorphization, and conditional equiconsistency. It is not a system of bounded first-class universe terms, and none of that package holds for an arbitrary edge graph. The Kappa artifact checks the finite table only.

The local source is the subsumptive calculus definition 119.4; the target is the bidirectional explicit-cast calculus of definition 119.6. A finite coercion graph is admitted only with the path-coherence conditions of definition 119.2. Elaboration preserves typing theorem 119.7; synthesis is determined lemma 119.8; and equality of every pair of graph paths yields derivation-independent inserted casts theorem 119.9. Function and record extensions require their displayed fiberwise equalities. The determinacy and coherence results also assume substitution-stable target equality and injectivity of dependent products; path coherence alone does not recover domain and codomain equalities in the application case. The completion proof theorem 119.11 is conditional on Soloviev–Luo’s three coherence conditions and applies only to their logical-framework signature. It proves no coherence result for another target calculus. The Kappa program checks only finite path pairs. The retained Soloviev–Luo source supplies paper proofs and no mechanized companion artifact; the Kappa graph is not a replay of that theorem.

The local generated action is defined structurally for the strictly positive description language of definition 120.2; indexed descriptions are the separate extension definition 120.7. Structural induction proves identity and composition on constructor-headed values before the extension. The exact delta definition 120.5 adds Desc-Map-Id/Desc-Map-Comp for all typed arguments, while only neutral composition is oriented as compaction. Generated action commutes with substitution lemma 120.13, and the whole delta preserves typing and substitution theorem 120.18. Dependent $\mathrm{\Pi }$ and $\mathrm{\Sigma }$ actions use their displayed variance-aware morphisms and prove their laws by beta/eta or pair computation lemma 120.8. The compacted neutral rule definition 120.9 preserves the same action by proposition 120.15; no eliminator-map fusion rule is present. The ${\mathrm{MLTT}}_{\mathsf{map}}$ proof in theorem 120.16 proves normalization, subject reduction, injectivity, canonicity, bidirectional equivalence, and decidability only for its formalized $0,\mathbb{N},\mathrm{\Pi },\mathrm{\Sigma }$, list, and one-universe fragment. AdapTT is the separately source-gated extension fixed in convention 120.19, proposition 120.20; its public repository is not a mechanization of the semantic proofs reconstructed in the chapter or of normalization and decidable checking. The Kappa program checks the finite description interpreter only.

The source declarations are the chapter’s finite ordered dependent pattern matrices over typed frontiers, including variable, constructor, inaccessible, and absurd patterns. Branch-local restricted unification is assumed terminating at each scheduled call. Under that hypothesis the compiler terminates, preserves row/frontier typing, reports symbolic coverage and reachability diagnostics, and simulates the displayed source clauses by its case trees. These results do not extend to arbitrary Agda or Equations coverage languages, unrestricted unification, or recursive/corecursive definition blocks; those mechanisms belong to later signatures.