ch:formalized-graded-erasure: graded erasure and extraction

Use ambient coordinates $(x,u,v)$. The simultaneous substitution keeps $x$ and sends $y$ to a term with demand $(3,1)$, so its row matrix is Consequently $$(1,2)\mathrm{\Psi }=(1,0,0)+2(0,3,1)=(1,6,2).$$ Replacing the application scalar by one changes the result to $(1,3,1)$. It under-counts the $u$-coordinate by three and the $v$-coordinate by one; those are exactly the missing second copy of the substituend’s free-variable demand.

Let the open declaration $x_0:{\mathrm{\Sigma }}_{\otimes }^{0}AB$ supply the scrutinee, assume $\mathsf{Prodrec}(0)$, and choose the constant motive $\mathsf{N}$ and constant branch $\mathsf{zero}$. The weak-product elimination rule derives $$x_0:{\mathrm{\Sigma }}_{\otimes }^{0}AB⊢{\mathsf{prodrec}}_0^0(\mathsf{N};x_0;\mathsf{zero}):\mathsf{N}.$$ The scrutinee is a neutral variable, so no weak-head reduction rule applies. Extraction at grade zero discards the match and gives $\mathsf{zero}$, which is already a target numeral. The first side condition of theorem 101.11 requires either $\mathrm{\neg }\mathsf{Prodrec}(0)$ or an empty context. Both disjuncts fail here; that condition, rather than consistency for empty elimination, rejects the example.

Suppose the last usage rule is U-App. The induction hypotheses give $\gamma \mathrm{\Psi }▸t[\sigma ]$ and $\delta \mathrm{\Psi }▸u[\sigma ]$. Rebuilding the rule is justified on its conclusion by $$(\gamma +p\delta )\mathrm{\Psi }\stackrel{\text{matrix distributivity}}{=}\gamma \mathrm{\Psi }+p(\delta \mathrm{\Psi }).$$ For the successor reduction $$\mathsf{natrec}(A;z;s;\mathsf{suc}n)⟶s{}^{p}n{}^r\mathsf{natrec}(A;z;s;n),$$ the characteristic successor law has the pointwise orientation $${\mathsf{nr}}_{p,r}(q_z,q_s,q_n)\le q_s+p{q}_n+r{\mathsf{nr}}_{p,r}(q_z,q_s,q_n).$$ The rebuilt application rules give the right demand, and U-Sub transports it down along this inequality to the redex demand on the left. Thus the contractum has the same advertised usage context. The exact placement of $p$ and $r$ is the one fixed by the source successor clause; exchanging them would prove a claim for a different recursion rule.

Usage preservation has inputs $\gamma ▸t$ and a typed step $\mathrm{\Gamma }⊢t⟶u:A$; it concludes only $\gamma ▸u$. Operational erasure soundness has a well-behaved zero, its two match restrictions, a natural-number typing, and $0▸t$; it concludes that source and extracted target reach one numeral. Resource correctness instead assumes the recursion calculus, a closed grade-one natural-number term, and its heap/stack invariant; it concludes numeral evaluation, zero-bounded residual heap grades, and, in the linearity instance, exactly one lookup of each allocated linear entry.

On the retained-argument term, preservation tracks the annotation through each source step but supplies no target run. Erasure soundness relates the source and target numerals but does not count target or heap accesses. Resource correctness counts linear heap lookup but concerns a different recursion rule and machine. Hence erasure soundness does not imply resource correctness, and resource correctness does not imply erasure soundness: their signatures use different calculi, while their conclusions respectively omit access counts and omit the extraction relation.