Problem, calculus, invariant, result, and acceptance. The finite calculus is 𝑡 ::=𝐹 ∣𝑋 ∣𝖠𝗉𝗉𝗅𝗒 𝑟 𝑡 𝑢. Evaluate its two-coordinate context demand and compare it with the direct translation’s unchanged annotations. The invariant is 𝗎𝗌𝖺𝗀𝖾(𝖠𝗉𝗉𝗅𝗒 𝑟 𝑡 𝑢)=𝗎𝗌𝖺𝗀𝖾(𝑡)+𝑟⋅𝗎𝗌𝖺𝗀𝖾(𝑢). The concrete result is 𝗎𝗌𝖺𝗀𝖾(𝑓(𝑓𝑥)) =(3,4) at 𝑟 =2, with the same translated pair and Boolean pair (𝗍𝗋𝗎𝖾,𝗍𝗋𝗎𝖾). Acceptance means the four named passes, the completion line, and audit [] printed in appendix E.
Representation choice. The constructors 𝐹, 𝑋, and 𝖠𝗉𝗉𝗅𝗒 𝑟 𝑡 𝑢 retain exactly the data needed for the Graded Base application rule. A pair of naturals stores the demands for 𝑓 and 𝑥. The separate Linear Base datatype has application and an explicit 𝑟-graded box; its evaluator scales at the box, not at application. These trees make the correspondence oracle discriminating, but adding a third variable changes the demand representation. A finite map from variable names to grades scales to arbitrary contexts, at the cost of normalization and equality code that obscures the calculation.
Minimal end-to-end version. Variables contribute unit demand in one coordinate. Application adds the function demand to 𝑟 times the argument demand. Check 𝑓(𝑓𝑥) =(1 +𝑟,𝑟2) at 𝑟 =2. Translate each application to an application whose argument is an explicit box carrying the same grade, evaluate the Linear Base tree by scaling at boxes, and compare both results with (3,4).
Remaining cases, in metatheory order. First check the direct translation equality. Second add the Boolean semiring evaluator and re-run the source syntax. Third compare 𝑓 𝑥, with natural usage (1,1), against 𝑓(𝑓𝑥), with usage (3,4): their Boolean usages coincide. Only after those oracles pass should another term be added.
Incorrect version. Replace multiplication at application by addition. The code typechecks, but the nested grade at 𝑟 =2 is no longer 4. As a separate mutation, omit the argument box in translation and require the translation oracle to fail.
Run and theorem boundary. Execute the four commands for this artifact in appendix E and compare accepted-output.txt with the named transcript. Restore the multiplication and replay after the mutant fails. The chapter’s correspondence theorem is proved by induction on typing and source reduction; this program checks only finite arithmetic and does not prove that theorem, combined-grading soundness, or fractional borrow safety.