ch:contextual-modal-tt: ch:contextual-modal-tt
Problem and result. Model the pinned Beluga type-uniqueness example’s lambda-case context invariant. The schema block pairs a term variable with its typing assumption. The recursive call succeeds only when it supplies both block projections; omitting the typing projection leaves the expected contextual family
Representation. Beluga’s schema keeps a term declaration and its typing evidence in one dependent block, so projection types enforce their connection. The portable Kappa preflight uses finite object, type, declaration, and projection constructors; its checker searches for evidence indexed by the same object and type. This makes the scope oracle executable without Beluga but deliberately erases LF terms, substitutions, and recursive coverage.
First complete version. Inspect the pinned source’s xtG schema declaration and lambda recursive call. The schema block contains a term declaration followed by typing evidence indexed by that term. The two contextual arguments of the recursive call both extend their context by the corresponding term and typing projections. Represent those dependencies with Kappa constructors for declarations and projections; the checker searches for the term projection and its matching typing projection.
Remaining cases. Model the application branch, where the recursive call keeps the same context, and the lambda branch, where schema inversion recovers the paired typing projection. Then replace the lambda call’s typing projection by evidence for a different term. The altered call must be rejected because its body derivation requires the typing assumption paired with b.x; the missing family is
Portable preflight. The Kappa corpus in artifacts/ch63-beluga-context-scope/ models this two-projection invariant. It validates the declaration dependency, accepts same-context and extended-context calls, and rejects the mismatched typing projection. The run does not execute or parse Beluga.
Acceptance test and boundary. Require the four named PASS lines, the exact recorded summary, silent checking, and audit result [] under the appendix E Kappa commands. Appendix E owns the pinned-source locator and records the absent Beluga toolchain. These observations are finite scope evidence. They do not prove CMTT subject reduction, normalization, hereditary-substitution termination, or decidability.