# v0.11 search-redundancy design Status: active development Baseline release: v0.10.0 ## Purpose v0.11 answers the project's founding question instead of extending the library: does a proof-net representation reduce proof-search redundancy for a proof assistant? The v0.10 experiments answered it only for matched MLL tasks with a supplied connective skeleton, a budget unit that the methods do not share, and a toy sequent baseline; their reports say so. v0.11 states the question as three falsifiable measurements, each preregistered before its data is produced and reported whichever way it comes out. A negative answer closes the program; it is not a failure of the program. ## Step 1: measure the redundancy Redundancy has an exact meaning here: distinct cut-free sequent derivations that differ only in the order of rule applications denote the same proof net. For a task, a one-sided sequent `⊢ F₁, …, Fₖ` of unit-free MLL formulas, fix the occurrence forest of the formulas and count, treating every occurrence as distinct and absorbing exchange: - `D_all`: derivations in the plain calculus (axiom, tensor with every context split, par, any rule order); - `D_weak`: derivations of the committed focused baseline (`scripts/focused_search.py`): the par phase is one deterministic step, then a tensor is chosen and its context split; - `D_foc`: derivations of the strictly focused calculus, where the focus persists through the positive subformulas of the chosen tensor; - `N`: correct proof nets of the sequent, the axiom linkings of the forest accepted by `Certificate.check`. The ratios `D_all / N`, `D_weak / N`, and `D_foc / N` are the redundancy factors of the three search spaces relative to the net space; `D_all / N` is the mean number of sequentializations of a net of the task. The counts are exact, by memoized recursion over sub-sequents with atom-balance pruning, and are cross-checked on the small tasks by an independent brute-force enumerator. Every count is a whole number; no sampling. Corpus: the 1,000 committed matched tasks (`experiments/matched-v0.1`) and the 180 held-out model tasks (`experiments/model-v0.2`), each with its depth, atom count, conclusion count, and repeated-name flag. A task whose exact count exceeds the preregistered state budget is reported as excluded with its partial bound; exclusions are counted, never silently dropped. Preregistered hypotheses: - H1: `D_foc / N > 1` on more than half of the tasks: focusing does not remove all rule-order redundancy; - H2: the median of `D_all / N` grows with the atom count faster than linearly across the three size classes; - H3: `D_foc / D_weak < 1` on more than half of the tasks: strict focusing removes redundancy the committed baseline keeps. The result is the distribution of the ratios by size class, with medians, quartiles, and the fraction of tasks where each ratio equals 1. Success is a correct number; no advantage is claimed from it. ## Step 2: equal-information matched search Three arms run on the same input, the sequent alone, in one Lean process under one wall-clock budget of five seconds per arm per task: - `focused`: the committed focused sequent search of `scripts/focused_search.py`, reproduced in Lean step for step (identical outcomes and operation counters on 86 sequents) so that both search families run in the same language on the same machine; - `focusedBalanced`: the same search with per-name atom-balance pruning of states and splits, so the comparison does not rest on a baseline that lacks an obvious cut; - `nets`: net-space search, enumerating the axiom linkings of the forest in the committed generator's order and deciding each with `Certificate.unificationCheck`, stopping at the first accepted linking. Each arm ends in `found`, `refuted` (exhausted without a proof), or `timeout`, and reports its elapsed time and its own operation counts. Corpus: 120 held-out bases from fresh seeds, forty per depth at 8, 16, and 32 atoms, each collapsed to unique, two-label, and one-label atom names, and one connective-flip negative per positive wherever exhaustive net-space search refutes the flip within twenty seconds; strata without a certifiable negative are reported as such, never filled by an unverified label. Preregistered hypotheses, written so that either search family can win: - H4: on unique-label tasks, where the linking is forced, `nets` decides at least as many tasks as `focusedBalanced` in every size stratum and is faster at 32 atoms; - H5: on one-label 32-atom positives, where the linking space explodes, `focusedBalanced` finds more proofs within the budget than `nets`; - H6: `focusedBalanced` decides at least as many tasks as `focused` in every stratum. The report is the outcome table per stratum and arm with the hypotheses answered as stated. If H4 and H5 both hold, the MLL answer is that proof nets remove rule-order redundancy and add linking redundancy, and which dominates depends on label repetition; a method for a proof assistant would have to combine both prunings. Step 3 runs only if the net-space search wins somewhere that matters. A second run (`experiments/matched-search-v0.2`) prunes both families: Andreoli focusing with balance and tensor-count conditions on every branch, and linking search with Danos's contraction after every axiom. It adds count-preserving negatives certified by a Lukasiewicz countermodel or by the focused search, never by the net arms; every connective-flip negative violates the tensor count, so the first run's negatives did not test search. Strict focusing decides all 983 tasks; the net search proves 21 of the 40 one-label 32-atom positives and refutes none of their negatives. ## Step 3: representation as the model's target The v0.10 model study already gave the model the sequent (the "skeleton" is its connective structure), so the correction is not to remove it but to vary the output representation alone. The same local model, at temperature zero without thinking, receives one rendering of the sequent (formula positions and numbered atom occurrences) and is asked in one arm for a top-down sequent-calculus proof and in the other for a proof-net linking; each system prompt carries the same worked example. Proofs are verified by conversion to `CutFreeDerivation` and `infer?` equality, nets by `Certificate.check` (`proofnet_ir_representation_verify`); an unparseable answer is wrong, and on negatives only an explicit unprovable answer is correct. Corpus: the 180 held-out tasks of `experiments/model-v0.2`. Preregistered hypotheses: H7, the net arm's verified rate on positives exceeds the proof arm's; H8, verified net outputs use fewer completion tokens than verified proofs; H9, the arms' negative-detection rates are within ten points. A pilot on development sequents showed both arms returning parseable JSON before registration; no corpus task had been run. ## Beyond MLL Proof nets exist cleanly for multiplicative linear logic only. After Step 3 the founding question was taken to Lean's scale in a separate repository, [proof-graphs](https://github.com/fushanbobfan/proof-graphs), with the goal-dependency graph of a tactic proof as the object. Rule-order redundancy is as explosive in real Lean proofs (up to about 10^652 orderings; ProofNet-IR's own proofs and a Mathlib slice agree), but Lean's convention of acting on the first goal already fixes one ordering: a real tactic search spends 2 to 4 percent of its expansions on it, and searching over goals proves no more at equal budget, even at eight times the budget. In a resource logic the graph quotients a factorial; in Lean the goal stack has already absorbed it. ## Release gates - [x] Step 1 preregistration committed before any count is produced; - [x] exact redundancy counts on the matched and model corpora, with the brute-force cross-check and the exclusion report, artifact-hash gated in CI; - [x] Step 1 report with the hypotheses answered; - [x] Step 2 preregistration with the frozen corpus and arms, then its run and report; - [x] Step 3 registered after a positive Step 2, then run and reported; - [ ] the linear whole-program bound (D6-linear) stays optional and outside these gates.