Proof-Path Invariance: frozen Hankel tables, measured and constructed recognizers
Lean-grounded benchmark tables of Horn premise traces against continuation-query tests, with raw runs of small language models and constructed recognizers, preregistered statistics, and the working draft of the paper.