ch:soft-linear-logic: proof-net weight oracle

Problem, calculus, invariant, result, and acceptance. Calculate Lafont’s weight polynomial on atoms, additive pairs, exponential boxes, and quantifier boxes, then test one exponential external reduction. The invariant is strict decrease of $W_u(n)$ at the fixed global rank $n$. For two atoms paired inside two boxes, the required result at rank $3$ is weight $31$, box degree $2$, and reduct weight $30$. Acceptance is the four named passes, completion line, and empty audit in appendix E.

Representation choice. A finite algebraic datatype stores the net skeleton. The evaluator takes a rank and implements the three displayed weight equations. A second recursion computes box depth. This tree representation is sufficient for local weight arithmetic but cannot express sharing or arbitrary cut wiring. A port graph would represent real proof nets and redex locations, at the cost of graph well-formedness and correctness checks beyond this supplement.

Minimal end-to-end version. Build a pair of atoms inside two boxes. At rank $3$, require weight $31$, degree $2$, and a strict decrease to the three-copy reduct of weight $30$.

Remaining cases, in metatheory order. Check atomic and additive clauses first, then one box, nested boxes, degree, and finally the external-reduction comparison. Add the rank-$4$ case only after calculating both redex and reduct weights by hand. Quantifier boxes are checked after exponential boxes because they add one without multiplying by rank.

Incorrect version. The supplied bad evaluator omits multiplication by rank. Its redex weight is smaller than the reduct, so the mutation oracle records the failure.

Run and theorem boundary. Execute the four commands for this artifact in appendix E, require its exact transcript and audit [], then run the omitted-rank mutant and restore it after the decrease oracle fails. Lafont’s normalization theorem quantifies over typed proof nets and all external reductions. This evaluator checks one finite skeleton; it is not a proof-net checker, normalization proof, representation theorem, or AARA cost analysis.