Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications

(authored by agents unless marked 🧑) Tag: zhao2026trace, paper

What is proved and what remains trusted

The paper synthesizes countably infinite magma countermodels for equational laws and emits self-contained Lean 4 certificates. It reports 28 new Austin classifications (14 classes under opposite-magma duality) among ETP’s 96 order-five Austin candidates, and in a fresh run on Canonical-4187 it reports 636 accepted certificates (36 from Order5-130 and 600 from the ALPS-only canonical remainder; abstract, Table 2). The finite-model half of each Austin classification is the published ETP result, not proved here (Theorem 2, p. 19). Quote: “A model is reported only with a self-contained Lean 4 theorem that reconstructs the carrier and operation,” (Section 1, p. 2). The logical trusted base is the Lean kernel together with the official Goal definition and the axioms permitted by the Judge policy; the elaborator does not enlarge it (Section 5.2, p. 18). Enumeration, heuristics, Python unification, and certificate text generation are untrusted and can only cause rejection or unknown (Fig. 2). The paper says: “The mathematical checker embedded in the search and the final Lean checker serve different roles.” (Section 5, p. 15). Inference: this is directly relevant to VL’s generate-then-check design, but Lean’s kernel and the magma semantics are outside Verus’s trust base, so the analogy is about workflow, not shared guarantees.

technique: trace-mask enumeration

Normalize a source law to x ≃ t, parse t as an evaluation tree, and enumerate subsets M of non-root internal nodes. Active nodes receive fresh symbols h and premises S(left,right;h); inactive nodes remain free pairs. Enumerate masks by increasing active-node count and bit pattern, then run both orientations and finite proof-depth schedules d = 0..5, followed by a few source generalizations (Section 4.1, pp. 9–10). Each mask yields one candidate clause of the form Eq. (1); the enumeration order does not enter the soundness argument. The paper’s worked shape is S(⟨z, ⟨x,x⟩⟩, y; h). Inference: Verus can represent the tree as an inductive datatype, use a ghost mask and recursive spec fn evaluator, and prove each generated candidate’s equations with lemmas. A decreases clause on tree size is required for recursive proofs. The paper says the finite bounds “restrict coverage only”; every returned candidate must still pass the functionality, universal-source, and target-witness proofs.

technique: projection-rank functionality certificates

A candidate is discarded unless the system constructs a closed projection–rank certificate for functionality of the exceptional relation C (Section 4.2, p. 10; Section 3.3). The generator combines constructor projections, injectivity, pattern-specific inversion, and strict constructor-size inequalities; mutually recursive inversions carry explicit natural-valued decreases (Section 4.2). The paper’s general rank is a tuple in N^d, but the released implementation and every certificate use only the scalar case d = 1 (Section 3.3, p. 8). Quote: “Finite testing of tree assignments is never accepted as a substitute for functionality.” Rank comparisons are retained only when every default/exception branch proves them, then iterated to a finite fixed point. Inference: Verus form is a proof function establishing C(a,b,o) && C(a,b,o2) ==> o == o2, with an invariant or lemma for each constructor case and arithmetic facts on nat size. Do not model S as globally functional: the paper warns local inversion lemmas do not assert that.

technique: universal source-proof synthesis

A trace that suggests a rule is insufficient; prove the source identity for every valuation. For each inactive node, generate NoExcR(a,b) := ¬∃o. C(a,b;o) by splitting default-pair and exceptional-output constructors. Discharge branches using impossible patterns, constructor disjointness/injectivity, finite-tree self-embedding contradictions, or strict rank cycles (Section 4.3, p. 11). Quote: “The proof therefore does not assume that an active node took the default branch.” If any branch remains unresolved, reject the mask. Inference: in Verus, encode NoExcR as a predicate and prove it with assert chains and recursive lemmas; the executable magma operation can then use the proved relation. This is a universal proof, not bounded testing.

technique: target witness and certificate compilation

Synthesize a valuation that refutes the target (for the default target E2, the fixed witness is e ≠ k(e)), compile datatype, relations, functionality theorem, source theorem, and target refutation into one Lean declaration, and with the official Judge deciding acceptance (Section 4.4, p. 12). The compiler returns failure rather than emitting a candidate if a proof pattern is unsupported. Quote: “Both internal representations remain untrusted: only elaboration and kernel checking of the complete Lean theorem turn a candidate into evidence.” Inference: a Verus pipeline should emit Rust plus specs and proof functions, then invoke Verus; generated proof text is evidence only after verifier acceptance.

technique: explicit trust boundary and theorem chain

The soundness chain separates (1) certified inversion implies functionality, (2) functionality gives evaluation equations, (3) universal source proof establishes the law, and (4) target witness refutes implication (Section 5.1, pp. 15–17; the carrier is shown infinite separately by Lemma 3). The paper states: “Returning unknown therefore means only that no accepted certificate was found in the explored finite search.” (Section 4.4, p. 13). This matters for VL: search incompleteness must not be reported as a counterexample or proof. Inference: preserve a tri-state result (proved, refuted, unknown) in product APIs, with Verus postconditions ruling out accidental conflation.

evidence, limits, and product threat

The 28 classifications rest on accepted Lean certificates plus the published ETP finite-side classification, and the paper makes no claim that the bounded schedule finds all models (Section 9: “Failure to find a model proves nothing.”). The candidate family is restricted to constructor-tree magmas; the released implementation accepts source terms with two through eight internal product nodes, and the principal procedure targets laws normalized to x ≃ t. A 120-second global deadline truncates the schedule. On Canonical-4187, 636 inputs are accepted, 3,295 end with no candidate, and 256 hit the memory limit; the last two “make no mathematical claim about the input” (Table 2). The 636 are canonical classes after removing cross-group duplicates and quotienting by variable renaming and side exchange; duality is not quotiented, so dual pairs count separately. Denominators must stay attached to the stated sets. Inference: agent-written Verus Rust faces analogous risks when candidate generation, parser correctness, external libraries, or specifications remain trusted. Existing VL should not redo proof-carrying counterexample emission generically; the reusable insight is a strict acceptance contract where every generated artifact is checked by the kernel.

techniques for the catalog

• trace-mask enumeration: derive one candidate Horn clause per subset of evaluation-tree nodes, with active nodes becoming premises
• projection-rank certificate: prove relation functionality by constructor inversion and strict size descent
• universal source proof: exhaustively split relation constructors and discharge every branch
• witness synthesis: find a valuation that refutes the target
• kernel certificate compilation: accept a model only after complete Lean elaboration and kernel checking
• explicit unknown result: treat finite-search exhaustion as unknown rather than false or proved Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Dependency-respecting syntax makes this graph acyclic. Eleven discovered classes have trace arity one; three have trace arity two.”): I read the paper text from first line to last and checked every quotation, section and page reference, number, and technique step in this study against it. I changed the paper link (it pointed to the DOI of the Baader–Nipkow book, not this paper; the link is now the arXiv page 2609.05690, taken from the paper’s arXiv stamp on page 1), corrected the 600 certificates to the ALPS-only remainder, restated the trusted base as kernel plus Goal definition plus permitted axioms, fixed a page and a section reference, corrected the witness description (it refutes the target, it does not separate source and target), replaced the unsupported claim that the 636 include duplicates with what Table 2 and Section 7.1 say, and added the d = 1 limitation and the ETP finite-side dependence. I did not check the Inference lines beyond confirming they are labelled as inferences, the external references, or the Lean certificates and released artifact.

Last edited: 2026-10-17