Gradual source and ground-cast calculus

The source of chapter 11 has only Booleans, natural-number literals, annotated functions, application, and the unknown type $?$. Consistency is the least relation generated by the five displayed rules, which are already closed under symmetry; it is reflexive and symmetric but not transitive. Type precision is ${⊑}_{\mathsf{ty}}$, while the decorated relations ${⊑}_{\mathsf{C}}$ and ${⊑}_{\mathsf{F}}$ compare typed cast terms and frames; none is the domain order of chapter 12. Function matching is defined only for arrows and $?$. There is no source subsumption, recursion, state, polymorphism, effect, object, or dependent type.

The target is a left-to-right call-by-value blame calculus with explicit labeled casts, ground tags $\mathbf{2}$, $\mathbb{N}$, and $?\to ?$, function wrappers, and one-frame-at-a-time blame propagation. Cast insertion is the fixed syntax-directed judgment of definition 23.8. There is no primitive cast composition or wrapper-observation operation.

Source-type uniqueness and typed unique insertion are proposition 23.4, proposition 23.9. Target substitution and canonical forms are lemma 23.11, lemma 23.12; preservation and deterministic progress up to blame are theorem 23.14, theorem 23.15. The polar blame theorem is theorem 23.23. Static precision and the static gradual guarantee are definition 23.26, theorem 23.29. Open target precision and related substitution are definition 23.30, lemma 23.35; frame plugging and value catch-up are lemma 23.37, lemma 23.40. Accounted one-step, finite, and infinite simulation are lemma 23.43, corollary 23.44, theorem 23.46; the terminal result is the dynamic gradual guarantee, theorem 23.48.

The target is not strongly normalizing. The closed typed $\delta d$ cycle preceding theorem 23.46 embeds untyped self-application through $?$. The reverse direction of the dynamic guarantee excludes divergence by infinite simulation, not by a normalization theorem.

The separately named SD card definition 23.53 combines simply and dependently typed components with explicit boundaries, constructor-indexed marshalling, and first-order equality guards. Under the exact Figure 8 conversion hypotheses, its imported preservation and progress boundary is theorem 23.54. This theorem contributes no dependent cast, blame, or gradual-guarantee rule to the principal calculus.

The proved observation distinguishes a related value, labeled blame, and divergence. Wrapper identity, allocation, cost, mutable references, polymorphism, effects, and dependent casts are outside the signature; no theorem transfers to them without a new translation and simulation.

The pinned Kappa corpus in appendix E executes the finite application-insertion calculation, ground-tag comparisons, both higher-order blame directions, and the precise-blame/less-precise-value example. It is implementation evidence only; the printed reductions and proofs do not depend on it.