ch:elaboration: ch:elaboration

Problem and invariant. Build a reusable first-order contextual-unification and finite level-graph slice, then run the six acceptance inputs through it. Every stored assignment must be scoped by its declaration telescope. Before the solver processes an equation, it applies the accumulated substitution to both sides. A successful core is exposed only after the required metavariables are assigned and the independent finite kernel check succeeds. The append case must reconstruct the level, element type, and both length indices and emit the exact metavariable-free spine.

Representation tradeoff. A dependently typed representation could index each term and substitution by its context. That choice prevents many malformed states, but it requires the implementation to carry the chapter’s full typing and renaming infrastructure. The companion uses numeric identifiers and checks declaration arity, spine distinctness, occurrence, and scope dynamically. This keeps every rejection visible while allowing symbols, equations, declarations, and level nodes not named by the public corpus. Its central types are:

data Meta : Type = Meta Nat
data Variable : Type = Variable Nat
data Symbol : Type = Symbol Nat
data Term : Type =
    Bound Variable
  | MetaApp Meta (List Variable)
  | Rigid Symbol (List Term)
data Declaration : Type = Declaration Meta (List Variable)
data Binding : Type = Binding Meta (List Variable) Term
data Equation : Type = Equation Term Term
data Edge : Type = Edge LevelNode Int LevelNode

An ordered list of Binding values is a substitution; a list of Equation values is the worklist. A MetaApp spine contains distinct variables and has the same length as the metavariable’s declaration telescope. The numeric representation admits every finite telescope and every finite rigid tree, rather than one constructor per acceptance record.

First end-to-end version. Implement substitution application, syntactic term equality, and a worklist loop. Equal endpoints are deleted. Equal rigid heads of the same arity add their corresponding children to the worklist; different heads or arities produce RigidClashReject. Orient a flex–rigid equation toward its flexible endpoint. Reject occurrence and scope failure, then store the scoped right-hand side as a binding. Constructor-node weight bounds decomposition; the number of declarations bounds successful assignments.

Use this loop for append-ok. Represent its two vector equations and the equality between the fresh level and u as ordinary terms. Rigid decomposition and flexible assignment derive all four bindings. Look each result up by metavariable and build every AppendCore field from those lookups. Continue only if all four are present. The independent finite kernel checks the expected values before a field-directed renderer prints the exact append spine. A hidden malformed-append guard requires the kernel to reject a core with the wrong element field.

Contextual assignment and remaining cases. Let a declaration carry formal variables $x_1,\dots ,x_k$, where the list length $k$ is unrestricted. At a use $?X[y_1,\dots ,y_k]$, require the $y_i$ to be distinct. A flex–rigid right-hand side may mention only the $y_i$. Replace those variables in parallel by the formal variables before storing the body. Substitution application performs the reverse parallel renaming at a later use spine. Reject flex–flex equations and repeated or wrong-arity spines as non-pattern input. Add a non-public three-variable assignment whose use spine differs from its declaration telescope; substitution must reconstruct the original right-hand side.

Add the level-explicit annotation vnil : Vec[0](Nat, zero) as two equations solving its level and element metavariables. Build VnilCore from the resulting bindings and send it through the same kernel. Bare vnil uses the same declarations with an empty worklist, so its required metavariables remain unsolved. Encode $?\alpha [x]\doteq \mathsf{suc}(?\alpha [x])$ and $?\alpha [x]\doteq y$ as ordinary solver problems; the first fails occurrence and the second fails scope.

For levels, read each edge as $p+c\le q$. Collect every node, initialize its distance to zero, and perform maximum relaxations. After one complete pass per node, the possibility of one further relaxation detects a positive-weight cycle. Test the public two-edge cycle, a three-node positive cycle, an acyclic graph, and a zero-weight cycle. Each rejection retains its own category, so a generic failure cannot stand in for the required diagnostic.

Observable result. The accepted run transcript is exactly

append-ok=ok:append[u]{A}{m}{n} xs ys:Vec(A,n+m)
vnil-annotated-ok=ok:vnil[0]{Nat}:Vec(Nat,zero)
vnil-ambiguous=reject:unsolved-meta
occurs-bad=reject:occurs
scope-bad=reject:scope
level-cycle-bad=reject:level-cycle
All 6 Chapter 112 corpus cases passed.

The six outcome records and owner summary form the seven-line observable interface.

Disabled-scope mutation. In makeAssignment, remove the branch that returns AssignmentFailed ScopeReject when the right-hand side is not scoped by the occurrence spine. The scope problem then produces a substitution. Its case constructs EscapedYCore, and the independent checker changes the fifth record to scope-bad=reject:kernel. The owner summary also reports failure, so the exact-output test fails. Restore the scope check before the final run.

Disabled-kernel mutation. Make the kernel branch for malformed append terms always succeed. The six printed records remain unchanged, but the hidden malformed-append guard changes the owner summary to a failure report. Hence the exact-output test fails. Restore the field checks before the final run.

Acceptance test. Apply the four-stage check, inline-test, run, and audit procedure recorded in Appendix E. Require a silent check, a passing exact-output test, precisely the six records above, and an empty audit. Replay the scope mutation once, require the test to fail, restore the source, and replay the disabled-kernel mutation. After restoring the source a second time, repeat all four stages.

Evidence boundary. The solver accepts arbitrary finite rigid trees and declaration telescopes, but only first-order syntactic equations whose flexible applications are distinct-variable spines. It implements flex–rigid assignment and rejects flex–flex constraints; it has no binders in term syntax, dependent typing, definitional equality, normalization, intersection, postponement, search, or constraint generation from surface programs. The graph checker handles any finite integer-weighted edge list, but it detects inconsistency only by a positive cycle and does not normalize full universe expressions. The independent kernel recognizes only the two successful public core shapes.

These executions illustrate the three solvedness conditions of definition 112.25 and the independent rechecking boundary of lemma 112.28; they do not prove either result. Consequently the companion proves none of theorem 112.24, corollary 112.29, theorem 112.32; those results remain mathematical proofs in the chapter.