Add Gradio app + deep-run artifacts (report, charts, 18 PDFs + verdicts)

.gitattributes

@@ -33,3 +33,21 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
+data/pdfs/200_off_run1.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/200_off_run2.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/200_off_run3.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/200_on_run1.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/200_on_run2.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/200_on_run3.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/300_off_run1.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/300_off_run2.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/300_off_run3.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/300_on_run1.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/300_on_run2.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/300_on_run3.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/400_off_run1.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/400_off_run2.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/400_off_run3.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/400_on_run1.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/400_on_run2.pdf filter=lfs diff=lfs merge=lfs -text
+data/pdfs/400_on_run3.pdf filter=lfs diff=lfs merge=lfs -text

README.md

@@ -1,13 +1,36 @@
 ---
-title: Paper Compression Context
-emoji: ⚡
-colorFrom: red
-colorTo: indigo
+title: Paper Compression — Context Experiment
+emoji: 📄
+colorFrom: blue
+colorTo: yellow
 sdk: gradio
-sdk_version: 6.20.0
-python_version: '3.12'
+sdk_version: 4.44.0
 app_file: app.py
 pinned: false
+license: mit
 ---
 
-Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference
+# Paper Compression — Prior-Context Experiment
+
+Interactive visualization of an off-vs-on context experiment: does giving a
+memoryless reconstructor access to a paper's prior reference paper let it recover
+the target theorem from a **shorter** compressed summary?
+
+- **Target:** *On Language Generation in the Limit with Bounded Memory* (arXiv 2605.30324)
+- **Context paper:** Kleinberg & Mullainathan, *Language Generation in the Limit* (arXiv 2404.06757)
+- **Design:** budgets {200, 300, 400} × {OFF, ON} × 3 trials
+
+## Tabs
+
+- **Report** — narrative writeup and headline conclusion.
+- **Results** — pass-rate chart, blinded comparative ranking, per-trial rank spread.
+- **Runs** — browse each reconstruction's PDF alongside the evaluator's verdict.
+
+## Data
+
+All artifacts live under `data/`:
+`scores.jsonl`, `ranking.json`/`.md`, `report.md`, and `pdfs/{budget}_{cond}_run{k}.pdf`
+plus matching `.comparison.md` evaluator verdicts.
+
+Generated by the [paper-compression](https://github.com/) harness. No model calls
+happen in the app — it only visualizes precomputed artifacts.

app.py

@@ -0,0 +1,234 @@
+"""Gradio app to visualize the paper-compression context experiment.
+
+Off-vs-on context experiment on 'On Language Generation in the Limit with
+Bounded Memory'. Shows the report, the pass/fail + blinded-ranking results,
+and a per-run browser with the reconstruction PDF and evaluator verdict.
+"""
+import base64
+import json
+from pathlib import Path
+
+import gradio as gr
+import pandas as pd
+
+DATA = Path(__file__).parent / "data"
+PDFS = DATA / "pdfs"
+
+# validated CVD-safe categorical pair (blue = OFF, orange = ON)
+OFF_C, ON_C = "#2563eb", "#ea7317"
+
+
+def load_scores() -> pd.DataFrame:
+    rows = []
+    for line in (DATA / "scores.jsonl").read_text().splitlines():
+        line = line.strip()
+        if not line:
+            continue
+        r = json.loads(line)
+        rows.append(
+            {
+                "budget": r.get("_exp_budget") or r.get("budget_words"),
+                "condition": (
+                    r.get("_exp_condition")
+                    or ("on" if (r.get("context") or {}).get("has_context") else "off")
+                ),
+                "run": r.get("_exp_run"),
+                "accepted": bool(r.get("accepted")),
+                "mean_score": r.get("mean_score"),
+            }
+        )
+    return pd.DataFrame(rows)
+
+
+def load_ranking() -> pd.DataFrame:
+    p = DATA / "ranking.json"
+    if not p.exists():
+        return pd.DataFrame()
+    return pd.DataFrame(json.loads(p.read_text()).get("ranking", []))
+
+
+def cond_label(c: str) -> str:
+    return "OFF (no PDF)" if c == "off" else "ON (with PDF)"
+
+
+scores = load_scores()
+ranking = load_ranking()
+
+
+def passrate_table() -> pd.DataFrame:
+    agg = (
+        scores.groupby(["budget", "condition"])
+        .agg(passes=("accepted", "sum"), n=("accepted", "count"),
+             mean_score=("mean_score", "mean"))
+        .reset_index()
+    )
+    agg["condition"] = agg["condition"].map(cond_label)
+    agg["pass"] = agg["passes"].astype(str) + "/" + agg["n"].astype(str)
+    agg["mean_score"] = agg["mean_score"].round(2)
+    return agg[["budget", "condition", "pass", "mean_score"]].rename(
+        columns={"budget": "Budget", "condition": "Condition",
+                 "pass": "Pass rate", "mean_score": "Mean score"}
+    )
+
+
+def passrate_plot():
+    import matplotlib
+    matplotlib.use("Agg")
+    import matplotlib.pyplot as plt
+
+    agg = (
+        scores.groupby(["budget", "condition"])
+        .agg(passes=("accepted", "sum"), n=("accepted", "count")).reset_index()
+    )
+    agg["rate"] = agg["passes"] / agg["n"]
+    budgets = sorted(agg["budget"].unique())
+    fig, ax = plt.subplots(figsize=(7, 4), dpi=130)
+    w = 0.38
+    for i, b in enumerate(budgets):
+        off = agg[(agg.budget == b) & (agg.condition == "off")]["rate"]
+        on = agg[(agg.budget == b) & (agg.condition == "on")]["rate"]
+        off = float(off.iloc[0]) if len(off) else 0
+        on = float(on.iloc[0]) if len(on) else 0
+        ax.bar(i - w / 2, off, w, color=OFF_C, label="OFF (no PDF)" if i == 0 else "")
+        ax.bar(i + w / 2, on, w, color=ON_C, label="ON (with PDF)" if i == 0 else "")
+        ax.text(i - w / 2, off + 0.02, f"{off:.0%}", ha="center", fontsize=9)
+        ax.text(i + w / 2, on + 0.02, f"{on:.0%}", ha="center", fontsize=9)
+    ax.set_xticks(range(len(budgets)))
+    ax.set_xticklabels([f"{b} words" for b in budgets])
+    ax.set_ylim(0, 1.1)
+    ax.set_ylabel("Pass rate")
+    ax.set_title("Pass rate by budget × context (n=3 per cell)", loc="left")
+    for s in ("top", "right"):
+        ax.spines[s].set_visible(False)
+    ax.legend(frameon=False, loc="upper left")
+    fig.tight_layout()
+    return fig
+
+
+def rank_spread_plot():
+    import matplotlib
+    matplotlib.use("Agg")
+    import matplotlib.pyplot as plt
+
+    if ranking.empty:
+        fig, ax = plt.subplots()
+        ax.text(0.5, 0.5, "no ranking data", ha="center")
+        return fig
+    rr = ranking.copy()
+    order, yt, ytl = [], [], []
+    y = 0
+    for b in sorted(rr["budget"].unique()):
+        for cond, color in (("off", OFF_C), ("on", ON_C)):
+            ranks = rr[(rr.budget == b) & (rr.condition == cond)]["rank"].tolist()
+            order.append((y, ranks, color))
+            yt.append(y)
+            ytl.append(f"{b}  {cond.upper()}")
+            y += 1
+        y += 0.4
+    fig, ax = plt.subplots(figsize=(7, 4.2), dpi=130)
+    for yy, ranks, color in order:
+        ax.scatter(ranks, [yy] * len(ranks), s=120, color=color,
+                   edgecolor="white", linewidth=1.5, zorder=3)
+    ax.set_yticks(yt)
+    ax.set_yticklabels(ytl, fontsize=9)
+    ax.invert_yaxis()
+    ax.set_xlim(0, 19)
+    ax.set_xlabel("Rank of 18 (1 = best reconstruction)")
+    ax.set_title("Per-trial rank spread (all 18 judged together)", loc="left")
+    ax.xaxis.grid(True, color="#e5e7eb")
+    ax.set_axisbelow(True)
+    for s in ("top", "right", "left"):
+        ax.spines[s].set_visible(False)
+    fig.tight_layout()
+    return fig
+
+
+def rank_table() -> pd.DataFrame:
+    if ranking.empty:
+        return pd.DataFrame()
+    r = ranking.copy()
+    r["Condition"] = r["condition"].map(cond_label)
+    mr = (
+        r.groupby(["budget", "Condition"])["rank"].mean().round(1).reset_index()
+        .pivot(index="budget", columns="Condition", values="rank").reset_index()
+        .rename(columns={"budget": "Budget"})
+    )
+    return mr
+
+
+def pdf_html(trial: str) -> str:
+    p = PDFS / f"{trial}.pdf"
+    if not p.exists():
+        return "<p>No PDF for this run.</p>"
+    b64 = base64.b64encode(p.read_bytes()).decode()
+    return (
+        f'<iframe src="data:application/pdf;base64,{b64}" '
+        f'width="100%" height="820" style="border:1px solid #ddd;border-radius:8px"></iframe>'
+    )
+
+
+def verdict_md(trial: str) -> str:
+    p = PDFS / f"{trial}.comparison.md"
+    return p.read_text() if p.exists() else "_No evaluator verdict for this run._"
+
+
+ALL_TRIALS = sorted(p.stem for p in PDFS.glob("*.pdf"))
+
+
+def filtered_trials(budget: str, cond: str):
+    sel = [
+        t for t in ALL_TRIALS
+        if (budget == "all" or t.startswith(budget + "_"))
+        and (cond == "all" or f"_{cond}_" in t)
+    ]
+    return gr.update(choices=sel, value=(sel[0] if sel else None))
+
+
+def show_run(trial: str):
+    if not trial:
+        return "", ""
+    return pdf_html(trial), verdict_md(trial)
+
+
+REPORT = (DATA / "report.md").read_text() if (DATA / "report.md").exists() else "No report."
+
+with gr.Blocks(title="Paper Compression — Context Experiment") as demo:
+    gr.Markdown(
+        "# 📄 Paper Compression — Prior-Context Experiment\n"
+        "Does giving the reconstructor the prior reference paper lower the compression "
+        "threshold?  *On Language Generation in the Limit with Bounded Memory* "
+        "(arXiv 2605.30324) · context: Kleinberg–Mullainathan (arXiv 2404.06757)."
+    )
+
+    with gr.Tab("📋 Report"):
+        gr.Markdown(REPORT)
+
+    with gr.Tab("📊 Results"):
+        with gr.Row():
+            gr.Plot(passrate_plot(), label="Pass rate")
+            gr.Plot(rank_spread_plot(), label="Rank spread")
+        with gr.Row():
+            gr.Dataframe(passrate_table(), label="Pass rate / mean score", interactive=False)
+            gr.Dataframe(rank_table(), label="Blinded mean rank (lower = better)", interactive=False)
+
+    with gr.Tab("🔬 Runs (PDFs + verdicts)"):
+        gr.Markdown(
+            "Each run: the reconstructor's theorem PDF and the evaluator's verdict. "
+            "OFF = summary only; ON = reconstructor could read the reference PDF."
+        )
+        with gr.Row():
+            budget_dd = gr.Dropdown(["all", "200", "300", "400"], value="all", label="Budget")
+            cond_dd = gr.Dropdown(["all", "off", "on"], value="all", label="Condition")
+            run_dd = gr.Dropdown(ALL_TRIALS, value=ALL_TRIALS[0] if ALL_TRIALS else None,
+                                 label="Run")
+        with gr.Row():
+            pdf_view = gr.HTML(pdf_html(ALL_TRIALS[0]) if ALL_TRIALS else "")
+            verdict_view = gr.Markdown(verdict_md(ALL_TRIALS[0]) if ALL_TRIALS else "")
+
+        budget_dd.change(filtered_trials, [budget_dd, cond_dd], run_dd)
+        cond_dd.change(filtered_trials, [budget_dd, cond_dd], run_dd)
+        run_dd.change(show_run, run_dd, [pdf_view, verdict_view])
+
+
+if __name__ == "__main__":
+    demo.launch()

data/pdfs/200_off_run1.comparison.md

@@ -0,0 +1,45 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 97
+- Proof quality: 88
+- Mean score: 3.67
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Recovers the central positive theorem exactly: countable domain, finite/countable family of infinite languages, deterministic memoryless set-valued generator, finitely repeating texts, eventual subset containment.
+- Recovers the explicit construction via J_n(x), n(x)=max{n<=x: J_n(x) infinite}, and G(x)=J_{n(x)}(x).
+- Main proof uses the same finite-bad-set argument with B_K, implication x in B_K => n(x)<z, construction of finite U_z from finite intersections among first z languages, and finite repetition to conclude eventual success.
+- Recovers the sharp characterization for arbitrary texts by the pointwise infinite intersection condition I_x being infinite for every x in union of languages.
+- Recovers both boundary impossibility statements: no memoryless element-generator for infinite targets under novelty requirement, and an explicit two-language mod-4 family defeating all memoryless index-generators.
+
+## Major Errors
+
+- There is a minor definitional wobble around well-definedness of n(x): the proof text appeals to an n=0 conceptual case / 'sufficiently small n' rather than the cleaner original observation that J_1(x) is infinite; this is harmless but imprecise.
+- The element-generator impossibility proof is not the paper's audited proof and contains some informal or shaky intermediate discussion before giving a workable adversarial construction; proof quality here is weaker than for the main theorem.
+- Languages are defined at one point as arbitrary subsets of X rather than immediately as infinite subsets; the positive theorem later restores infinitude, so this does not materially change the target but is a presentation mismatch.
+
+## Budget Feedback
+
+To improve further, tighten the element-generator impossibility proof into a clean exhaustive argument with no informal detours, and state the well-definedness of n(x) exactly via J_1(x) being infinite (or equivalent).
+
+## Reasoning
+
+Criterion 1 is above threshold because the reconstructed theorem package matches the original theorem almost exactly, including the positive bounded-memory/memoryless set-based result, the explicit generator, the arbitrary-enumeration characterization, and the two impossibility boundaries. There are only minor presentation deviations. Criterion 2 is above threshold because the main theorem proof is sound and closely tracks the original audited argument; the arbitrary-text characterization proof is also sound. The main weakness is that the element-generator impossibility proof is somewhat less clean and not obviously identical to the original architecture, but it still gives a plausible adversarial diagonalization establishing the stated impossibility. Overall the reconstruction is sufficient for the benchmark.
+
+## Critique
+
+The reconstruction is highly faithful to the target theorem. It states the correct setting: countable domain, finite or countable family of infinite languages, deterministic memoryless set-valued outputs, and success defined as eventual containment of infinite outputs in the target on every finitely repeating text. It preserves the key restriction to finitely repeating enumerations and does not drift to full-memory, identification, density, or finite-family-only variants. 
+
+For the positive theorem, the construction is essentially exact: after identifying X with N and enumerating the family as L_1,L_2,..., it defines J_n(x) as the intersection of the first n languages containing x, then n(x) as the largest n<=x with J_n(x) infinite, and outputs G(x)=J_{n(x)}(x). The proof then fixes K=L_z, defines the bad set B_K={x in K: G(x) not subset of K}, proves x in B_K implies n(x)<z, and for x>=z deduces J_z(x) finite, whence x belongs to a finite union U_z of finite intersections among the first z languages. Therefore B_K is finite; finite repetition then yields eventual success. This is the same proof mechanism as the original.
+
+The arbitrary-enumeration theorem is also reconstructed correctly, with the exact iff condition that I_x, the intersection of all languages containing x, be infinite for each x in the union. The sufficiency proof via G(x)=I_x is standard and correct. The necessity proof correctly uses a text for a target K that repeats x infinitely often, forcing G(x) to lie inside every target containing x and hence in I_x; since G(x) must be infinite, I_x must be infinite. This matches the original characterization and the one-example intuition.
+
+The index-based impossibility theorem is faithful and specific: it uses the exact mod-4 pair L_1={0,1 mod 4}, L_2={0,2 mod 4}, observes that one label must occur infinitely often on multiples of 4, and chooses the opposite language as target to force infinitely many failures on a finitely repeating text. That is essentially the original paper's example.
+
+The weakest part is the element-based impossibility proof. The statement itself matches the original target, but the proof meanders: an initial recursive construction is introduced, then partially abandoned, then replaced by a cleaner diagonalization. The final argument is plausible and likely sufficient—at each stage, if g(x_t) is already bad, failure occurs immediately; otherwise choose x_{t+1}=g(x_t), ensuring that stage t's output soon becomes seen and hence cannot witness eventual novelty. However, the exposition could be cleaner about why this yields infinitely many failures and how the completed text still enumerates exactly K while preserving the adversarial stages. Even so, the theorem package requested by the benchmark is recovered, and the central main theorem plus characterization are both accurately proven.
+
+Bottom line: this is a successful reconstruction. It matches the original theorem package under the same assumptions, uses the same main construction and finite-exception argument, and includes the correct boundary theorems. The only notable weakness is some proof untidiness in the element-generator impossibility result, not enough to defeat sufficiency.

data/pdfs/200_off_run1.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:f0b8f4850c811cb1c78e912514726563b47f0d0cb4201b2596269eaa3eafe7a4
+size 186884

data/pdfs/200_off_run2.comparison.md

@@ -0,0 +1,42 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 98
+- Proof quality: 94
+- Mean score: 4.0
+- Proof fidelity: Same
+- Proof completeness: Full
+
+## Major Successes
+
+- Recovers the central positive theorem exactly: every countable family of infinite languages over a countable domain has a deterministic memoryless set-based generator succeeding on all finitely repeating enumerations.
+- Includes the explicit canonical construction with J_n(x), n(x)=max{n<=x: J_n(x) infinite}, and G(x)=J_{n(x)}(x).
+- Proves the key finite-bad-set argument for target K=L_z via x in B_K implies n(x)<z and hence bad x>=z lie in a finite union of finite intersections among L_1,...,L_z.
+- Recovers the exact characterization for arbitrary enumerations: universal memoryless set-generation iff each pointwise intersection I_x is infinite.
+- Recovers both boundary impossibility statements: no universal memoryless element-generator under fresh-element success, and a concrete 2-language counterexample for memoryless index-generators using the mod 4 pair.
+
+## Major Errors
+
+- Minor definitional deviation: n(x) is justified using admissible n=0 and an empty intersection convention, whereas the target presentation used positive naturals and observed J_1(x) infinite; this is harmless.
+- For the arbitrary-text characterization, the theorem states existence on every text for every K in L, and the proof correctly derives G(x)⊆K via arbitrarily late repetitions; no substantive mismatch, but it phrases the witness text as x,y1,x,y2,... rather than an abstract repetition argument.
+
+## Budget Feedback
+
+Very little needs repair. To make it fully airtight, align the indexing convention for n(x) exactly with the target presentation (avoid introducing 0 unless explicitly redefining N) and explicitly note that the collection listing should contain every language at least once.
+
+## Reasoning
+
+Criterion 1 is well above pass because the reconstruction matches the benchmark theorem package almost exactly: same countable-domain/countable-family setting, same memoryless set-based model, same finitely repeating restriction, same explicit generator, same arbitrary-enumeration iff characterization, and same element/index impossibility boundaries. The only small discrepancy is a harmless indexing convention around n(x). Criterion 2 is above pass because the proof is logically sound and essentially complete. Part (1) reproduces the original finite-obstruction argument correctly. Part (2) gives both directions of the characterization using the standard repeated-x adversarial text. Part (3) supplies a valid impossibility proof for memoryless element-generators; it is not the same case-split proof as described in the audit, but it correctly proves the stated theorem. Part (4) correctly uses the mod-4 pair and an infinite pigeonhole argument on multiples of 4. The proof is complete enough to support the theorem package.
+
+## Critique
+
+The reconstruction is faithful both in theorem content and in the positive-proof mechanism. It correctly sets up the model: countable X, finite or countable family of infinite languages, texts/enumerations, finitely repeating condition, deterministic memoryless set-generators G:X->[X]^infty, and success as eventual subset containment. It then states the explicit construction J_n(x)=intersection of listed languages up to n containing x, defines n(x) as the largest depth <=x with J_n(x) infinite, and sets G(x)=J_{n(x)}(x). The proof of the main positive result closely matches the paper: for K=L_z, define bad points B_K, show any bad point must satisfy n(x)<z), then for x>=z deduce J_z(x) is finite, so x lies in one of finitely many finite intersections among the first z languages; hence B_K is finite. Finitely repeating texts then eliminate bad points after finitely many stages. This is exactly the target mechanism.
+
+For the boundary under arbitrary repetitions, the reconstruction states the exact iff condition that every I_x be infinite and provides the standard proof. The necessity argument via a text with arbitrarily late occurrences of x is fully valid and accurately captures why memorylessness plus arbitrary repetition forces G(x) to be contained in every target containing x. The sufficiency argument G(x)=I_x is exact.
+
+For the necessity of set-based output, the reconstruction fully recovers both negative results. The element-generator impossibility is proved by a different but valid construction: choose an increasing sequence a_s with a_{s+1}>g(a_s), let K={a_s}, and enumerate K without repetition. Then each output g(a_s) is either outside K or among previously seen elements, so freshness fails at every stage. This proves an even stronger adversarial statement for the fresh-element criterion and is fully acceptable because it establishes the same theorem under the same assumptions. The index-generator impossibility uses the exact two-language mod-4 example from the target and a clean infinite-case split over common points. 
+
+The only nits are presentational. The reconstruction introduces 0 as an admissible depth in n(x), while the target theorem described n(x)=max{n<=x: J_n(x) infinite} with positive indexing and justified existence through J_1(x) being infinite. This is a notational harmlessness, not a model change. Also, it could have explicitly said the enumeration of the family contains every language at least once, though repetitions are allowed and this is implicit in calling it an enumeration of the family. These are not substantive enough to affect correctness.
+
+Overall, this reconstruction clearly meets the benchmark: same theorem package, same setting, same core proof for the positive result, exact characterization under arbitrary repetitions, and the right impossibility boundaries.

data/pdfs/200_off_run2.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:eecb6b8e91bc2c8099d7727924e89f8a3716b219eff53840f754552c8d577969
+size 186666

data/pdfs/200_off_run3.comparison.md

@@ -0,0 +1,40 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 88
+- Proof quality: 72
+- Mean score: 3.3
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Accurately recovers the central positive theorem for countable families of infinite languages on a countable domain under finitely repeating enumerations, including the explicit construction via J_n(x), n(x), and the finite-bad-set argument.
+- Correctly recovers the sharp characterization for arbitrary enumerations using the one-point intersections I_x and gives the natural sufficiency construction G(x)=I_x.
+- Correctly states and proves the two boundary impossibility claims: no memoryless element-based generator under the unseen-element success notion, and a two-language counterexample for memoryless index-based generators using the mod-4 pair.
+- Uses the same core proof architecture as the paper: identify bad points, show they lie in finitely many exceptional finite intersections, and exploit infinite repetition to force necessity in the arbitrary-enumeration characterization.
+
+## Major Errors
+
+- The converse proof of the arbitrary-enumeration characterization is flawed: it proposes a 'text' beginning with infinitely many copies of x and then enumerating the rest of K, which is not a valid infinite sequence enumerating all elements of K. The intended adversarial construction should instead repeat x infinitely often interleaved with the rest of K.
+- The positive theorem section has a definitional inconsistency: J_n(x) is defined for n in N with language indices starting at 1, and the proof appeals to J_0(x)=N although J_0 was not included in the displayed definition. This is repairable but is still a proof/presentation gap.
+- Because of the invalid text construction in the necessity direction, the provided proof as written does not fully establish the stated iff theorem, even though the theorem itself is the right one.
+
+## Budget Feedback
+
+Repair the necessity proof for the arbitrary-enumeration characterization: use a valid enumeration that repeats x infinitely often while still listing every element of K at least once (e.g. interleave x with an enumeration of K). Also clean up the J_0/J_1 indexing in the positive construction so existence of n(x) is formally correct.
+
+## Reasoning
+
+Criterion 1 is below pass threshold because the stated theorem package is essentially the correct one, but there is a small mismatch in the arbitrary-text proof presentation and a slight strengthening/shift in one negative theorem statement ('for every infinite target language K subset X') compared with the paper's family-based formulation, though this strengthening is harmless for theorem content. Criterion 2 is below pass because one of the three main proofs contains a genuine invalid construction: an infinite sequence cannot both be constantly x forever and later enumerate the rest of K. The rest of the proofs are good and paper-faithful, but the package as a whole is not fully supported at the required rigor level.
+
+## Critique
+
+The reconstruction does an excellent job recovering the paper's actual target theorem package. It gets the model right: countable domain, finite/countable family of infinite languages, deterministic memoryless set-valued outputs, finitely repeating texts, and eventual subset containment. It also reproduces the explicit generator G(x)=J_{n(x)}(x) with the correct dependence on the largest n<=x such that the relevant intersection remains infinite. The proof of the main positive theorem is essentially the original argument and is well presented: define B_K, show bad points must satisfy n(x)<z, then for x>=z force J_z(x) finite and place x in a finite union of finite intersections among the first z languages. That is faithful and mathematically sound apart from the J_0 indexing hiccup.
+
+The arbitrary-enumeration characterization is also the right theorem. The sufficiency direction G(x)=I_x is correct. However, the necessity direction contains a real error: the text 'x_0=x_1=x_2=...=x' is not an enumeration of K unless K={x}, which is impossible here since languages are infinite. The proof text then says it 'continues with an arbitrary enumeration of the rest of K', but an infinite prefix of copies of x leaves no later positions. The paper's intended argument is easy to repair by taking any valid enumeration in which x appears infinitely often, e.g. x, y_1, x, y_2, x, y_3, ... where (y_n) enumerates K. Because the submitted proof does not do this, the theorem package is not fully proved as written.
+
+The negative results are recovered well. The element-based impossibility is stated in a stronger but compatible way and supported by a diagonal construction of an infinite target K and repetition-free text on which g never outputs a fresh unseen element in K. This is not the paper's exact case-split proof but it proves the claimed impossibility under the same model. The index-based impossibility for the mod-4 pair is also correct; the case analysis is a bit different in style from the paper's pigeonhole-on-common-core presentation but establishes the same result.
+
+Overall: theorem recovery is strong and highly specific, proof mechanism recovery is strong, but the benchmark is strict about proof support. Since one companion theorem is not actually proved as written, this should be marked insufficient and fail.

data/pdfs/200_off_run3.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:409ddf53e2178301d3046dd017d01c275bb927f487af215e6d002816c49070a4
+size 185844

data/pdfs/200_on_run1.comparison.md

@@ -0,0 +1,41 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 88
+- Proof quality: 60
+- Mean score: 3.2
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Correctly reconstructs the central positive theorem for memoryless set-based generation on finitely repeating enumerations, including the explicit construction via J_n(x), n(x), and the finite-bad-set argument.
+- Correctly reconstructs the characterization for arbitrary enumerations via infinitude of I_x.
+- Includes the intended negative boundary for memoryless element-based generation and identifies the two-language mod-4 family for index-based impossibility.
+- Uses essentially the same proof architecture as the original for Theorem 1.1 and Theorem 3.1.
+
+## Major Errors
+
+- The reconstruction's stated index-generator impossibility theorem is only about finitely repeating texts, but the proof uses a text where 0 occurs infinitely often, so it does not prove the stated theorem.
+- Because the target benchmark includes the precise companion impossibility/characterization statements, the broken proof of the index-based boundary theorem is a material failure.
+- The theorem package is therefore not fully supported as written; one boundary statement is misstated/proved under inconsistent assumptions.
+- There is a minor indexing/presentation deviation (using J_0 and naturals starting at 0) that is harmless, but it departs from the paper's formulation.
+
+## Budget Feedback
+
+Repair the index-based impossibility boundary theorem. Either state the theorem under arbitrary repetitions if using the repeated-common-point proof, or supply the correct finitely-repeating adversarial enumeration argument for the mod-4 two-language class. Since the benchmark requires the companion boundary statements too, this fix is the highest-value next repair.
+
+## Reasoning
+
+Criterion 1 is below pass threshold because the reconstruction gets the main theorem and characterization essentially right, but one of the required sharp boundary statements is not faithfully recovered: the index-based impossibility is stated for finitely repeating texts yet proved using infinite repetition of 0, which changes the model/assumption. Criterion 2 is substantially lower because the proof package does not actually establish all stated results; the index-based theorem's proof is invalid for its statement. The main theorem proof itself is strong and close to the original, and the arbitrary-text characterization proof is sound. Proof fidelity is 'Same' because the key construction and finite-bad-set mechanism match the original. Completeness is only 'Partial' because one important companion theorem is unsupported.
+
+## Critique
+
+The reconstruction is impressively specific and paper-faithful on the core positive result. It identifies the exact memoryless set-based model, the finitely repeating enumeration restriction, the explicit construction G(x)=J_{n(x)}(x), and the key bad-set proof with U_z. This is enough to show strong recovery of Theorem 1.1. It also correctly states and proves the unrestricted-enumeration characterization using I_x, with the standard necessity argument based on making x recur infinitely often within a valid text.
+
+However, the benchmark's target is not just Theorem 1.1 in isolation; it explicitly includes the companion impossibility/characterization results that sharply delimit the positive result. The reconstruction includes both boundary theorems, but the index-based one is defective in a way that matters under the benchmark. The statement says impossibility on finitely repeating texts, matching the original target. But the proof considers a text for L_2 (or L_1) in which the common element 0 appears infinitely often. Such a text is not finitely repeating, so the argument does not prove the theorem as stated. This is not a cosmetic issue: it changes the adversarial power and exactly collapses the distinction that the paper is careful about. Since the original theorem package requires the precise boundary under finitely repeating enumerations, this mismatch prevents a full pass.
+
+The element-generator impossibility is directionally correct, though its proof is somewhat looser than the audited original combinatorial case split. Given the note that established cited results need not be reproved from scratch, that part is acceptable. The main blocker is the unsupported index-based theorem.
+
+So: excellent recovery of the main theorem and much of the surrounding architecture, but not sufficient for benchmark success because one required boundary theorem is not validly recovered under the correct assumptions.

data/pdfs/200_on_run1.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:51db977218570ef7645af77130f3e749bcc7c1afb81e140dda6e6f3c6139e2e8
+size 185855

data/pdfs/200_on_run2.comparison.md

@@ -0,0 +1,41 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 97
+- Proof quality: 91
+- Mean score: 3.83
+- Proof fidelity: Same
+- Proof completeness: Full
+
+## Major Successes
+
+- Accurately states the central positive theorem for countable families of infinite languages on countable domains with deterministic memoryless set-valued output under finitely repeating enumerations.
+- Recovers the exact explicit construction using J_n(x), n(x)=max{n≤x: J_n(x) infinite}, and G(x)=J_{n(x)}(x).
+- Provides the same finite-bad-set proof architecture for Theorem 1.1: define B_K, show bad points force n(x)<z, then for x≥z derive J_z(x) finite and hence membership in a finite union of finite intersections.
+- Recovers the exact characterization for arbitrary enumerations via infinitude of I_x=⋂{L:x∈L}.
+- Includes the boundary impossibility statements for memoryless element-based and index-based output, including the same 2-language mod-4 witness for the index case.
+
+## Major Errors
+
+- The element-based impossibility theorem is stated/proved only as a universal impossibility across all families by diagonalizing to a single adversarial language, rather than the paper's stronger per-language statement that no infinite language is generable by any memoryless element-based generator.
+- The index-generator theorem is phrased for arbitrary h:X→N while simultaneously referring to a two-language indexed family; the proof informally restricts outputs to the two named languages, so the formal statement should have specified codomain {1,2} (or success/failure convention for out-of-range indices).
+- Includes external citation/contextual framing not needed for the benchmark, though this does not affect theorem recovery.
+
+## Budget Feedback
+
+To improve further, tighten the negative boundary statements to exactly match the paper: state the element-based impossibility as 'for every infinite language K, no memoryless element-generator generates K under finitely repeating texts,' and formalize the index-generator codomain/output semantics so the two-language counterexample is watertight even if indices outside {1,2} are allowed.
+
+## Reasoning
+
+Criterion 1 is very high because the reconstruction captures the same main theorem, the same model, the same finitely-repeating condition, the same success notion, and the same exact characterization under arbitrary repetitions. It also includes the intended necessity-of-set-based-output boundary. I dock a few points because the element-generator impossibility is not stated in the same strongest form as the original companion theorem, and the index-generator statement has a small formalization issue about output range. Criterion 2 is above threshold because the proof of the main positive theorem is essentially complete and correct, and the arbitrary-enumeration characterization proof is sound. The proof style and mechanism match the original closely. The negative proofs are mostly sound, though the index-based statement could be cleaned up formally, and the element-based proof proves a somewhat different impossibility statement than the paper's exact one.
+
+## Critique
+
+The reconstruction is benchmark-sufficient. For Theorem 1.1, it gets both the statement and proof almost verbatim in substance: countable domain, countable/finite family of infinite languages, deterministic memoryless set-valued generator, eventual subset containment, finitely repeating enumerations, reduction to N, J_n(x), n(x), G(x), bad set B_K, and the finite exceptional-set argument. This is exactly the core paper contribution. The proof is not merely generic; it recovers the paper-specific combinatorial mechanism that makes bounded memory possible.
+
+The companion characterization for arbitrary repetitions is also recovered correctly. The sufficiency argument uses G(x)=I_x, and the necessity argument uses texts that repeat x infinitely often to force G(x) into every candidate language containing x. This matches the original theorem and underlying adversarial amplification principle.
+
+On the negative side, the reconstruction clearly understands that set-valued output is essential and that element-based and index-based memoryless generation fail. It correctly recovers the mod-4 two-language witness for index-based output. However, the element-based theorem stated here is weaker/different in quantification from the paper's statement summarized in the answer key: the paper says no infinite language is generable by a memoryless element-based generator under finitely repeating enumerations, while the reconstruction proves no single memoryless element-generator can universally succeed across all families because one can diagonalize an adversarial K against it. That still supports the claimed boundary intuitively but is not the exact companion theorem. Also, the index-based theorem should formally constrain the output indices to the two-language family or specify what happens for indices not naming a language in the family.
+
+Despite these caveats, the benchmark target explicitly centers on the positive bounded-memory generation theorem together with the sharp boundary statements; the reconstruction substantially recovers all of them, with the main theorem and Theorem 3.1 recovered faithfully and rigorously. Therefore it passes.

data/pdfs/200_on_run2.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:34f3de5267b7410a199ccc0703d12fac7780c5da39f8e129bd1153eb1b9d1068
+size 184455

data/pdfs/200_on_run3.comparison.md

@@ -0,0 +1,41 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 78
+- Proof quality: 72
+- Mean score: 2.5
+- Proof fidelity: Similar
+- Proof completeness: Partial
+
+## Major Successes
+
+- Correctly reconstructs the central positive memoryless set-based theorem for finitely repeating texts, including the explicit construction via J_n(x), n(x), and the finite bad-set argument.
+- Correctly states and proves the characterization for arbitrary texts via infinitude of I_x.
+- Recovers the negative element-based boundary in a strong form.
+
+## Major Errors
+
+- The index-based impossibility theorem is reconstructed incorrectly: the proof only inspects h(0) and then assumes the same output on all multiples of 4, which is false for a memoryless function h(x) depending on x. The original requires an infinite-subsequence/pigeonhole argument over the infinite overlap C=4N.
+- Because the target theorem package explicitly includes the precise companion impossibility statements, the faulty proof of the index-based boundary means the full benchmark target is not recovered.
+- Minor setting drift: introduces external citation and comparison material not part of the target theorem package, though this is not central.
+
+## Budget Feedback
+
+Repair the index-based negative theorem. You must use the infinite overlap C=4N and argue that one of the two indices is chosen on infinitely many points of C; then choose the opposite target and a finitely repeating enumeration hitting exactly those overlap points infinitely often (or all of them once) before the rest. Do not argue from h(0) alone.
+
+## Reasoning
+
+Criterion 1 is below pass because the reconstruction gets the main theorem and arbitrary-text characterization essentially right, but the required theorem package includes the sharp necessity/characterization statements, and the index-based impossibility is not correctly established. Criterion 2 is below pass because the positive proof is sound, the arbitrary-text proof is sound, and the element-based negative proof is sound, but the index-based negative proof has a decisive logical flaw: memoryless means dependence on the current datum, not constancy across all common points. Thus the stated proposition is unsupported. Proof fidelity is Similar because the main positive and characterization proofs use the same core construction and bad-set mechanism, but the index-based impossibility deviates into an invalid simplification. Completeness is Partial because most parts are fully argued, but an essential companion theorem is not.
+
+## Critique
+
+The reconstruction closely matches the paper on the core positive bounded-memory result. Definitions are largely faithful: countable domain, finite/countable family of infinite languages, memoryless set-generator G:X->[X]^infty, success as eventual subset containment, and finitely repeating texts. The explicit construction J_n(x)=∩{L_j:j≤n and x∈L_j}, n(x)=max{n≤x:J_n(x) infinite}, G(x)=J_{n(x)}(x) is exactly the right mechanism. The proof of the main theorem mirrors the audited argument: define B_K, show x in B_K implies n(x)<z, then for bad x≥z infer J_z(x) finite and therefore x lies in a finite union U_z of finite intersections among the first z languages; conclude B_K is finite, hence finitely repeating texts eventually avoid it. This is faithful and essentially complete.
+
+The arbitrary-text characterization theorem is also correctly reconstructed. Sufficiency via G(x)=I_x is immediate and correct. Necessity properly uses the constant text x,x,x,... for any target containing x to force G(x)⊆K for every such K, hence G(x)⊆I_x; since G(x) is infinite, I_x must be infinite. This matches the original theorem and proof idea.
+
+The element-based impossibility is acceptable, even slightly stronger than the paper's qualitative statement, because it shows for any memoryless element map there is an infinite language and repetition-free text on which the output is always outside the target. This is under the same fresh-element success criterion and is compatible with the target.
+
+The decisive problem is Proposition  index-negative. The original theorem only claims existence of a two-language class not generable by any memoryless index-based generator, with the mod-4 pair as witness. But the proof here is invalid. From h(0)=1 or 2, the reconstruction concludes that on every multiple of 4 the rule outputs the same index as on input 0. That does not follow: a memoryless index-generator is a function of the current input x, so h(4), h(8), ... may differ from h(0). The correct argument must examine the infinite common set C=4N and use that, since h maps C to {1,2}, one of the two indices is chosen on infinitely many elements of C. Then selecting the opposite target and enumerating those overlap points yields infinitely many failures. Because this exact companion impossibility is part of the benchmark target, the package is not fully recovered.
+
+Thus the submission is strong on the central theorem and one boundary theorem, but it falls short of the strict benchmark due to a nontrivial proof failure on the second boundary statement.

data/pdfs/200_on_run3.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:f20ca97b4adae28cb39f72e10c9928986e2f0a467e60dd753438508833eb4e05
+size 184824

data/pdfs/300_off_run1.comparison.md

@@ -0,0 +1,42 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 98
+- Proof quality: 90
+- Mean score: 3.83
+- Proof fidelity: Same
+- Proof completeness: Full
+
+## Major Successes
+
+- Correctly states the central positive theorem for countable families of infinite languages over a countable domain under finitely repeating enumerations.
+- Recovers the explicit construction J_n(x), n(x), and G(x)=J_{n(x)}(x), with the same finite-bad-set proof structure via B_K and U_z.
+- Correctly states and proves the arbitrary-repetition characterization using the one-point intersection condition I_x being infinite.
+- Correctly includes the boundary impossibility results for memoryless element-based and index-based generators, including the specific two-language mod-4 counterexample.
+
+## Major Errors
+
+- Minor indexing mismatch in the positive proof: the theorem states n,x in N with J_n defined for 1<=j<=n, but well-definedness is justified using J_0(x)=N; this is harmless if N includes 0, but the statement should have clarified that n may be 0.
+- The element-generator impossibility proof is reconstructed rather than matching the original combinatorial case split, and its enumeration-of-all-of-K argument is the least secure part, though the conclusion is plausible and likely correct.
+- The index-generator proof is stronger/simpler than the paper's infinite-common-core adversarial argument; while valid, it does not mirror the original proof mechanism.
+
+## Budget Feedback
+
+Mostly successful. To make it fully airtight, repair the small indexing inconsistency around n(x) (explicitly allow n=0 in the definition of J_n) and tighten the element-generator impossibility proof so the construction of an admissible enumeration of all of K is completely rigorous without relying on a delicate minimal-counterexample argument.
+
+## Reasoning
+
+Criterion 1 is very high because the reconstruction matches the target theorem package almost exactly: same model, same finitely-repeating restriction, same explicit generator, same sharp characterization for arbitrary repetitions, and same negative results for element/index outputs. Criterion 2 is above threshold because the main theorem and Theorem 3.1 are proved soundly and in essentially the original way, and the index-output impossibility is valid. The one area with some proof fragility is the element-generator impossibility proof, which departs from the original summary's case-split argument and contains a somewhat delicate justification that the constructed sequence enumerates all of K. Still, the central benchmark theorem is rigorously supported, and the companion results are adequately established for benchmark purposes.
+
+## Critique
+
+The reconstruction is a strong match to the original theorem package. For the main positive result, it preserves all essential assumptions: countable domain, finite or countable family, all languages infinite, deterministic memoryless set-valued output, success meaning eventual subset containment, and the crucial finitely-repeating-enumeration restriction. It also preserves the explicit construction almost verbatim: define J_n(x) as the intersection of the first n indexed languages containing x, choose n(x) as the largest n<=x with J_n(x) infinite, and output G(x)=J_{n(x)}(x). The proof strategy is the same as the original audited proof: fix K=L_z, define the bad set B_K, show x in B_K implies n(x)<z, then for x>=z deduce J_z(x) is finite and x lies in a finite union U_z of finite intersections of subfamilies of {L_1,...,L_z}. This yields finiteness of B_K and therefore eventual success under finitely repeating enumerations. This is exactly the paper's mechanism.
+
+There is only a small presentational defect in the setup of n(x): the theorem text defines J_n(x) with 1<=j<=n and n(x)=max{n<=x: J_n(x) infinite}, but then the proof of well-definedness appeals to J_0(x)=N. Since the reconstruction takes N={0,1,2,...}, this is easily repaired by explicitly allowing n=0. It does not affect the substance.
+
+The arbitrary-repetition characterization is also matched faithfully. The reconstruction states the same iff condition that for every x in the union of the family, the intersection I_x of all languages containing x is infinite. The sufficiency proof chooses an infinite subset of I_x and observes that I_{x_t} is contained in the target at every round. The necessity proof uses an enumeration returning to x infinitely often and the memorylessness of G to conclude G(x) must be contained in every target containing x, hence in I_x, forcing I_x to be infinite. This is fully aligned with the original.
+
+For the negative results, the reconstruction correctly states that no infinite language is generable by a memoryless element-generator under finitely repeating enumerations, and that memoryless index-generators fail already for the explicit two-language family L1={0,1 mod 4}, L2={0,2 mod 4}. The index-generator proof actually gives a clean direct contradiction: for any shared point x in L1∩L2, eventual correctness for target L1 implies the fixed response h(x) must index a language contained in L1, forcing h(x)=1; similarly target L2 forces h(x)=2. This is a valid stronger simplification, though not the same proof as in the paper. The element-generator proof is the weakest part: it constructs a repetition-free enumeration designed to avoid previous outputs and then argues that if g(x_t) is in K it cannot appear later, so it must already have appeared, violating freshness. The broad idea is sound, but the argument that the construction enumerates all of K is more delicate than the original paper's summarized case split and is not as crisp. Even so, this issue does not undermine the central benchmark theorem, and the impossibility claim is plausibly established.
+
+Overall, the reconstruction should pass: it recovers the theorem package nearly exactly, under the same assumptions, with essentially the same main proof and the correct boundary statements.

data/pdfs/300_off_run1.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:7ab3bbfd3171ade126ba26a8fa500a5e3b02ec0bd5a67934ee702d2dc46bf7b3
+size 183042

data/pdfs/300_off_run2.comparison.md

@@ -0,0 +1,39 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 93
+- Proof quality: 78
+- Mean score: 3.7
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Accurately reconstructs the main positive theorem for countable families of infinite languages over a countable domain under finitely repeating enumerations.
+- Gives the explicit original construction with J_n(x), n(x)=max{n≤x: J_n(x) infinite}, and G(x)=J_{n(x)}(x).
+- Main proof follows the original bad-set argument via B_K, shows x in B_K implies n(x)<z, then for x≥z places x in a finite exceptional set U_z, concluding B_K is finite.
+- Correctly reconstructs the arbitrary-repetition characterization via the one-point intersections I_x and proves both directions using the same adversarial/repetition idea.
+- Correctly states the necessity of set-based output and reproduces the specific two-language mod-4 counterexample for index-based generators.
+
+## Major Errors
+
+- The proof of the element-based impossibility theorem is explicitly incomplete and not rigorous enough to establish the stated theorem; it contains a marked GAP and only a heuristic/outline adversarial argument.
+- Because one of the companion boundary theorems is not actually proved, the reconstructed theorem package does not fully support the claimed sharp boundary statements required by the benchmark.
+- Minor indexing/presentation differences (starting at 0, using J_0(x)=N) are harmless, but they do not affect the main issue that one proof obligation is unmet.
+
+## Budget Feedback
+
+Repair the element-generator impossibility theorem with a complete formal adversarial proof. That is the main missing discriminator: the main theorem and Theorem 3.1 are essentially exact, and the index-based counterexample is fine, but the package fails the benchmark because Boundary 2(i) is only sketched and explicitly admits a gap.
+
+## Reasoning
+
+Criterion 1 is high because the reconstruction matches the original theorem package closely: same model, same finitely repeating assumption, same explicit generator, same arbitrary-repetition iff characterization, and same set-vs-element/index boundary claims. Criterion 2 falls below pass because the proof support is uneven: Theorem 1.1 and the arbitrary-repetition theorem are proved well, and the index-based impossibility is broadly sound, but the element-based impossibility theorem is not established rigorously and is explicitly marked with a GAP. Since the benchmark target includes the precise companion impossibility/characterization statements, this missing proof is material. Therefore sufficient=false and overall pass=false despite strong theorem recovery.
+
+## Critique
+
+Compared with the target, the reconstruction is very faithful on theorem content. The main theorem is essentially identical: countable family of infinite languages on a countable domain, memoryless deterministic set-valued generator, finitely repeating enumerations, eventual subset containment, and the concrete construction through J_n(x), n(x), and G(x). The proof mirrors the original audited proof almost line by line, including the finite bad set B_K and the finite exceptional union U_z. The characterization under arbitrary repetitions is also recovered exactly, with the same condition I_x infinite for every x and the same necessity/sufficiency mechanism. The index-based impossibility theorem uses the correct mod-4 pair and gives the right adversarial tension on common points.
+
+The decisive weakness is the element-based impossibility theorem. The target theorem package requires this companion statement, and the reconstruction states it correctly but does not prove it. The argument presented is a mixture of a recursive attempt and an informal diagonal observation, then explicitly concedes that the formal adversarial scheduling is not recovered. That is not enough under the strict benchmark, where the proof must support the stated theorem. So the result is a near-match on theorem recovery but an insufficient proof package overall.
+
+In short: theorem match is excellent; proof package is incomplete in one required boundary component, so the reconstruction does not meet the benchmark success criterion.

data/pdfs/300_off_run2.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:59c36269a8f5ae31563f467c8b65ddc8a804e60bf7a3de40046c1a0b441d97bf
+size 183413

data/pdfs/300_off_run3.comparison.md

@@ -0,0 +1,36 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 92
+- Proof quality: 76
+- Mean score: 3.5
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Accurately reconstructs the main positive theorem for countable families of infinite languages over a countable domain under finitely repeating enumerations.
+- Gives the explicit original construction via J_n(x), n(x), and G(x)=J_{n(x)}(x).
+- Main proof follows the paper's bad-set argument: define B_K, show x in B_K implies n(x)<z, derive J_z(x) finite for x>=z, use finite union U_z to conclude B_K finite.
+- Correctly states the unrestricted-enumeration characterization using I_x and provides a sound necessity/sufficiency argument.
+- Includes the paper-specific negative results distinguishing set-based from element-based and index-based output, including the mod-4 two-language example.
+
+## Major Errors
+
+- The reconstructed proof of the element-generator impossibility is not sound as written: it explicitly abandons one attempted construction and then presents a 'cleaner' block construction without proving that suitable y_t always exist or that the process yields a full enumeration of K.
+- The index-generator success notion is stated as eventual exact equality L_{h(x_t)}=K, which is stronger than the original benchmark's eventual subset-containment requirement for the output language; while the supplied counterexample still works, this changes the formal model.
+- There are minor indexing/convention mismatches (e.g. switching between J_0 and earlier 1-based formulations, x_0 vs x_1), harmless for the main theorem but indicative of reconstruction looseness.
+- Because one companion theorem is supported only by an incomplete/incorrect proof, the overall theorem package is not fully substantiated at the benchmark standard.
+
+## Budget Feedback
+
+Keep the main theorem and Theorem 3.1 as is, but repair the negative boundary theorem proofs. Most importantly, replace the unsound element-generator impossibility argument with a complete adversarial case split or another rigorous construction that guarantees a finitely repeating enumeration of the whole target language and infinitely many freshness violations. Also align the index-generator success definition with eventual subset containment rather than exact equality.
+
+## Reasoning
+
+Criterion 1 is high because the reconstruction recovers the central positive result essentially exactly, including the explicit generator, and also includes the sharp boundary theorems that delimit it. I scored below perfect because the index-based success criterion is strengthened from eventual containment to eventual exact identification, which is a model change, though in this specific negative example the contradiction still goes through. Criterion 2 falls below pass because the main theorem proof is good and the Theorem 3.1 proof is sound, but the element-generator impossibility proof contains a clear gap: the proposed block construction does not establish existence of the needed sequence in all cases nor that all elements of K are eventually enumerated. Under the strict rubric, a proof that does not actually support a stated companion theorem prevents full proof-quality credit. Since pass requires theorem match >=90, proof quality >=85, and overall sufficiency, this reconstruction fails.
+
+## Critique
+
+Comparison to target: The reconstruction matches Theorem 1.1 very closely. It keeps the correct setting (countable domain, finite/countable family of infinite languages, memoryless deterministic set-valued generator), the finitely repeating enumeration restriction, the same explicit J_n/n(x)/G construction, and essentially the same proof with the finite bad set B_K and exceptional finite union U_z. This is faithful and paper-specific. It also correctly states the unrestricted-enumeration characterization in terms of I_x being infinite, and the proof is standard and valid: sufficiency by choosing an infinite subset of I_x, necessity by repeating x infinitely often. For the output-model boundary, the reconstruction includes the right qualitative claims: no memoryless element-generator for any infinite language under finitely repeating enumerations, and a two-language counterexample for memoryless index-generators with the exact mod-4 languages from the target. However, the element-generator proof is not adequate. It starts a case split, notices a flaw in one branch, and then substitutes a block construction that is only asserted, not rigorously justified. In particular, it does not prove that one can indefinitely choose fresh y_t with the required properties while still producing an enumeration containing every element of K at least once. The original theorem package requires this impossibility statement as one of the precise companion delimiters, so this gap matters. The index-generator theorem is also formulated under a stronger success requirement (eventual equality to the target language rather than eventual output language contained in the target), which is not faithful to the original formalization even if the specific impossibility example remains valid. Overall: excellent theorem recovery and mechanism recovery for the core result; insufficient proof recovery for the full target package.

data/pdfs/300_off_run3.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:3fc8244b965f8beb46622155d36dfe23b87c1224caa1ee6677890d5f0560660a
+size 187721

data/pdfs/300_on_run1.comparison.md

@@ -0,0 +1,43 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 92
+- Proof quality: 78
+- Mean score: 3.5
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Correctly states the central positive theorem for countable families of infinite languages on a countable domain under finitely repeating enumerations.
+- Recovers the explicit construction G(x)=J_{n(x)}(x) with the same J_n(x), n(x), bad-set B_K argument, and finite-exception set U_z mechanism.
+- Correctly includes the sharp characterization for arbitrary repetitions via infinitude of I_x.
+- Correctly includes the index-based impossibility example with the mod-4 languages.
+- Definitions of memoryless set/element/index generators and success criteria match the target setting.
+
+## Major Errors
+
+- The proof of the element-generator impossibility is not sound as written: the recursive construction does not establish the claimed invariant, and the fallback argument using forward chains and the ordering z_2,z_1,z_4,z_3,... has the direction reversed, so the image has not already appeared at the asserted bad stages.
+- Because one of the companion boundary theorems is unsupported by a valid proof, the reconstructed theorem package is not fully proved to the benchmark standard.
+- Minor indexing/presentation differences (starting from 0 rather than 1) are harmless but do not affect the above proof defect.
+
+## Budget Feedback
+
+Repair the proof of the element-based impossibility theorem. Either cite the prior paper explicitly for that theorem or give a correct exhaustive case split showing infinitely many failures under a finitely repeating enumeration. The main theorem and the arbitrary-repetition characterization are already good; the decisive missing discriminator is a valid proof/support for Boundary 2(i).
+
+## Reasoning
+
+Criterion 1 is high because the reconstructed statements essentially match the target theorem package: same central positive result, same characterization under arbitrary repetitions, and same impossibility boundaries for element- and index-based outputs. Criterion 2 falls below pass because although the main theorem proof and the arbitrary-repetition characterization are sound and closely track the original, the element-generator impossibility proof contains substantive logical flaws and does not actually prove the theorem as stated. Under the strict rubric, a package theorem with an invalid companion proof does not meet benchmark sufficiency. Proof fidelity is 'Same' because the main theorem uses the same J_n/n(x)/finite-bad-set strategy, but completeness is only 'Partial' because one major component is not rigorously established.
+
+## Critique
+
+Main theorem: faithful and well proved. The reduction to X=N, definition of J_n(x), choice of n(x)=max{n<=x:J_n(x) infinite}, and generator G(x)=J_{n(x)}(x) are exactly the paper's construction up to harmless 0/1-based indexing. The proof for a target K=L_z is the same: define B_K={x in K:G(x) not subset K}; if x is bad then n(x)<z; if also x>=z then J_z(x) is finite; encode finite intersections among the first z languages in U_z; conclude B_K subseteq {x<z}∪U_z, hence finite; finitely repeating enumerations eventually avoid B_K. This is benchmark-quality.
+
+Theorem on arbitrary repetitions: also faithful. The condition I_x infinite for every x in the union is exactly the target characterization. Sufficiency via G(x)=I_x (or any infinite subset) is correct. Necessity via repeating a point x infinitely often and noting any successful memoryless output must lie in every language containing x is also correct. This matches the original mechanism.
+
+Index-based impossibility: the mod-4 example is exactly the target example, and the proof is fine.
+
+Element-based impossibility: statement matches the target, but the proof does not. The argument attempts to recursively build distinct y_m with g(y_m) among previous y_i. However, in the branch where no previous fiber is infinite, choosing y_m from the complement gives no reason that g(y_m) is previous, and the text's 'replace y_m by this new element and continue one step later' does not preserve the invariant or complete a valid induction. The subsequent graph-theoretic fallback is too sketchy and the concrete enumeration z_2,z_1,z_4,z_3,... does not show failure at the claimed stages: if g(z_i)=z_{i+1}, then when z_{2r-1} appears, z_{2r} has not already appeared in that ordering. So the displayed witness enumeration is incorrect. Since the benchmark asks for proof quality, this gap is fatal unless the theorem is explicitly cited as established from the prior paper.
+
+Overall: theorem recovery and paper-specific details are excellent; the only substantial issue is proof validity for Boundary 2(i). That prevents a pass under the strict benchmark.

data/pdfs/300_on_run1.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:4265a493a32f07f746f858566b21f6ccef2f9eacef8dfc67b7c951a1bad5eae5
+size 189320

data/pdfs/300_on_run2.comparison.md

@@ -0,0 +1,43 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 92
+- Proof quality: 78
+- Mean score: 3.7
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Correctly recovers the main positive theorem for countable families of infinite languages on a countable domain under finitely repeating enumerations.
+- Gives the explicit original construction J_n(x), n(x), and G(x)=J_{n(x)}(x), with the same finite-bad-set proof strategy via B_K and U_z.
+- Correctly recovers the arbitrary-repetition characterization using I_x and the iff condition.
+- Correctly recovers the two-language index-based impossibility example L1={0,1 mod 4}, L2={0,2 mod 4}.
+- Appropriately flags uncertainty about the element-based impossibility proof rather than overstating recovery.
+
+## Major Errors
+
+- The proof of the element-based impossibility theorem is not rigorous and contains unsupported claims ('this can be done infinitely often', 'that latter alternative would force... one again creates infinitely many stages...').
+- Because the benchmark targets the theorem package including the companion impossibility/characterization statements, the unsupported element-based proof leaves the package insufficiently proved.
+- There is a harmless notation shift to N starting at 0 with J_0(x)=N rather than the paper's J_1-based presentation, but this does not affect the main theorem.
+
+## Budget Feedback
+
+Repair the element-based impossibility result (Theorem 3.2(i)) with a complete adversarial case split or cite the source paper explicitly for that theorem. The main positive theorem and the arbitrary-repetition/index-based boundaries are already strong; the missing discriminator is a rigorous proof or established attribution for the no memoryless element-generator claim.
+
+## Reasoning
+
+Criterion 1 is high because the reconstructed statements match the target package closely: same model, same countable-family scope, same finitely repeating restriction, same explicit generator, same arbitrary-repetition characterization, and same index-based counterexample. Criterion 2 is below pass because although the main theorem proof and the arbitrary-repetition/index-based proofs are sound, the element-based impossibility proof is only a sketch with significant logical gaps. Under the strict benchmark, the theorem package includes that companion impossibility statement, so the proof package is not sufficient. Proof fidelity is 'Same' since the positive theorem uses the same J_n/n(x)/finite-bad-set mechanism; completeness is 'Partial' because one major component is not fully established.
+
+## Critique
+
+The reconstruction is faithful on the central positive result. It states the exact memoryless set-based model, the finitely repeating enumeration condition, generation-in-the-limit as eventual subset containment, and the countable-family scope. The concrete construction J_n(x)=∩{L_j:j≤n and x∈L_j}, n(x)=max{n≤x:J_n(x) infinite}, G(x)=J_{n(x)}(x) is exactly the right one up to harmless indexing differences (using N={0,1,2,...} and J_0=N). The proof for K=L_z mirrors the original audited proof: define B_K, show x∈B_K implies n(x)<z, then for x≥z infer J_z(x) finite, package exceptional points into a finite union U_z of finite intersections among the first z languages, conclude B_K is finite, and then use finite repetition to eventually avoid B_K. This is a high-quality recovery.
+
+The arbitrary-repetition boundary theorem is also correctly stated and essentially correctly proved. The sufficiency direction chooses G(x)=I_x (or any infinite subset), and the necessity direction uses the adversary's ability to repeat x infinitely often, forcing G(x) to be simultaneously safe for every target containing x. That matches the original mechanism.
+
+The index-based impossibility theorem is likewise faithful. The two-language family is the correct one, and the argument from shared samples in 4N forcing one index to be wrong for one of the two targets is sound.
+
+The main deficiency is Theorem 3.2(i), the impossibility for memoryless element-based generators. The statement is correct, and the author openly marks proof uncertainty, which is good calibration. But the actual proof offered is not a valid complete proof: after handling the case A={x:g(x)∉K} infinite, it moves to a graph argument and makes several non sequiturs. In particular, the construction of infinitely many y_i with distinct g(y_i) is not justified under arbitrary out-degree structure; the subsequent adversarial scheduling argument is heuristic rather than deductive; and the claims about 'unless all but finitely many points map to unseen future points' and 'that latter alternative would force ... one again creates infinitely many stages...' are not proved. Since the benchmark explicitly includes the companion impossibility statements delimiting the main theorem, this gap matters. The user also notes that citation to the prior paper counts as established, but here the theorem is not simply cited as established; instead a flawed proof reconstruction is given. If the author had cleanly invoked the prior paper for this theorem, proof completeness might have been acceptable.
+
+Overall: theorem recovery is strong and paper-specific, but benchmark success requires both theorem match and proof support for the targeted theorem package. The unsupported element-based impossibility proof prevents a pass.

data/pdfs/300_on_run2.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:fcd9c54dadc9c94ed5b0dd9ab57ce708fd6f2c83d953040907409906a27cd478
+size 182067

data/pdfs/300_on_run3.comparison.md

@@ -0,0 +1,36 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 92
+- Proof quality: 78
+- Mean score: 3.5
+- Proof fidelity: Similar
+- Proof completeness: Partial
+
+## Major Successes
+
+- Correctly states the central positive theorem for memoryless set-based generation on countable families of infinite languages under finitely repeating enumerations.
+- Recovers the explicit construction via J_n(x), n(x), and G(x), and the bad-set strategy for proving success.
+- Includes the exact characterization for arbitrary repetitions using I_x being infinite iff unrestricted memoryless set-generation is possible.
+- Includes the sharp negative boundary for memoryless element-based and index-based generators, with the correct two-language mod-4 counterexample for the index-based case.
+- Setting, quantifiers, and success notion are essentially faithful to the original benchmark.
+
+## Major Errors
+
+- The proof of the main positive theorem contains a substantive mistake: from n(x)<z it infers J_{n(x)+1}(x) is finite and treats it as an intersection of a subfamily of {L_1,...,L_z}; but when n(x)+1<z, L_z need not appear among the intersectands, so this does not justify x∈U_z. The original uses J_z(x), not J_{n(x)+1}(x).
+- Because of that error, the finiteness of B_K is not actually established by the written proof, so the main theorem is not fully supported as proved.
+- The element-generator impossibility proof is only a loose sketch with a non-rigorous case split and an unsupported 'block' argument; it does not cleanly prove the stated theorem, though the theorem itself is correct.
+- The notes explicitly hedge that the element-generator proof may differ and is reconstructed from summary-level intuition, confirming incompleteness.
+
+## Budget Feedback
+
+Repair the positive theorem proof exactly at the bad-point argument: when x∈B_K and x≥z, derive that J_z(x) is finite (since z is admissible but cannot be ≤n(x)) and conclude x lies in the finite union U_z of finite intersections among {L_1,...,L_z}. Also replace the element-generator impossibility sketch with a rigorous exhaustive combinatorial proof (or clearly cite it if inherited from prior context).
+
+## Reasoning
+
+The reconstruction matches the target theorem package very closely in statement, model, and boundary results. It gets the right domain assumptions, countable family scope, finitely repeating restriction, explicit generator construction, unrestricted-repetition characterization, and necessity of set-based outputs. So theorem match passes. However, the proof quality falls below pass threshold. The main theorem proof deviates at the critical step: instead of using J_z(x) finite, it uses J_{n(x)+1}(x) finite and incorrectly claims this is an intersection from the first z languages that includes L_z whenever z≤n(x)+1; but from n(x)<z one gets n(x)+1≤z, not z≤n(x)+1, and generally n(x)+1 can be much smaller than z. Thus the argument for x∈U_z is invalid as written. Since this is the central proof, this is a significant gap. The arbitrary-repetition characterization is proved soundly. The index-generator impossibility is also sound. The element-generator impossibility is not rigorous enough to count as a full proof. Therefore criterion 2 does not reach 85 and the overall benchmark should fail.
+
+## Critique
+
+Comparison to target: (1) Main theorem statement: faithful. The reconstruction correctly requires a countable domain, a finite or countable family of infinite languages, deterministic memoryless set-valued output, and eventual subset containment on every finitely repeating enumeration. (2) Explicit construction: almost exact. J_n(x), n(x), and G(x) are correctly reconstructed, modulo indexing from 0 instead of 1, which is harmless. (3) Main proof strategy: mostly recovered, but the key finite-bad-set argument is mis-executed. The target proof shows that if x∈B_K and x≥z, then J_z(x) is finite; since x∈L_z, J_z(x) is one of the finite intersections among the first z languages containing x, so x∈U_z. The reconstruction instead uses J_{n(x)+1}(x), which need not involve L_z and need not be among the intersections defining U_z in the intended way. This is not a cosmetic issue: it breaks the formal deduction that every sufficiently large bad x lies in a fixed finite exceptional set. (4) Boundary theorem under arbitrary repetitions: correctly stated and proved, essentially matching the original necessity/sufficiency mechanism. (5) Element-based impossibility: statement matches, but proof is only outline-level and contains unsupported adversarial claims. It gestures at the right mechanism (freshness impossible without memory) but does not rigorously establish the exhaustive case analysis referenced in the answer key. (6) Index-based impossibility: good recovery, with the exact mod-4 example and a valid contradiction argument. Overall, this is a strong semantic recovery of the theorem package, but not a proof-complete recovery: the central positive proof has a nontrivial logical error, and one negative theorem is underproved.

data/pdfs/300_on_run3.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:9ef2d023955ba63c580300c9a7ebac4bb310be89a97e4106ae88c8025e06230c
+size 194859

data/pdfs/400_off_run1.comparison.md

@@ -0,0 +1,54 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 82
+- Proof quality: 78
+- Mean score: 3.2
+- Proof fidelity: Same
+- Proof completeness: Partial
+
+## Major Successes
+
+- Recovers the central positive theorem for countable families of infinite languages on a countable domain under finitely repeating enumerations, with the same explicit construction via J_n(x), n(x), and G(x).
+- Recovers the exact characterization for arbitrary repetitions using the pointwise intersections I_x and gives the correct necessity/sufficiency idea.
+- Recovers the negative element-output theorem with essentially the same three-case combinatorial argument.
+- Recovers the two-language mod-4 counterexample showing failure of memoryless index-based generation in general.
+
+## Major Errors
+
+- The index-based model is changed: success is defined as eventual exact identification L_{h(x_t)}=K, whereas the target theorem only requires eventual output of an index whose language is contained in the target. This is a non-harmless strengthening/change of model.
+- The main theorem construction mishandles empty intersections by first saying the intersection is empty and then setting J_n(x)=N; this is a presentation inconsistency.
+- The proof of the arbitrary-text necessity theorem uses a purported positive text that 'lists every element of K at least once and then repeats x forever', which is not a valid enumeration/text under the given definition because infinitely many elements cannot all appear before an infinite tail of repeated x. The adversarial construction needed in the original audit is therefore misstated.
+- The necessity proof for arbitrary texts therefore has a genuine logical gap as written, even though the intended result is correct.
+- Because of the altered index-based success notion, the claimed theorem package is not under exactly the same assumptions/model as the target.
+
+## Budget Feedback
+
+Keep the same set-based positive theorem and explicit G, but repair the boundary proofs/models exactly: (i) define index-generator success as eventual containment L_{h(x_t)}⊆K, not exact equality; (ii) fix the arbitrary-repetition necessity argument by using a genuine text that enumerates K while repeating x infinitely often, rather than 'enumerate all of K then repeat x forever'.
+
+## Reasoning
+
+The reconstruction is very close to the target theorem package and clearly paper-specific. It gets the main positive theorem essentially exactly, including the explicit J_n/n(x) construction and the finite bad-set proof. It also states the right iff characterization under arbitrary repetitions and the right impossibility phenomena for element- and index-based outputs. However, the benchmark requires matching the same model and assumptions. The reconstruction changes the index-based success criterion from eventual containment to eventual exact equality, which is not a harmless restatement. Although the supplied counterexample still witnesses impossibility under the stronger criterion, it does not recover the original theorem under the original model. In addition, the necessity proof for the arbitrary-text characterization relies on an invalid text construction ('list every element once and then repeat x forever'), so the proof as written is unsound. These issues push theorem match below the strict pass threshold and proof quality below the pass threshold.
+
+## Critique
+
+Comparison to target:
+
+1. Main positive theorem (Theorem 1.1):
+The reconstruction matches the setting (countable domain, finite or countable family of infinite languages, deterministic memoryless set-valued generator, finitely repeating positive texts) and the success criterion for the set-based model. It reproduces the explicit construction J_n(x)=∩{L_j:j≤n and x∈L_j}, n(x)=max{n≤x:J_n(x) infinite}, G(x)=J_{n(x)}(x). The proof follows the original mechanism exactly: define B_K, show x∈B_K implies n(x)<z, then for x≥z infer J_z(x) finite, gather all finite intersections among the first z languages into a finite exceptional set U_z, conclude B_K finite, and use finite repetition to eventually avoid bad points. This is faithful and strong.
+
+2. Characterization under arbitrary repetitions (Theorem 3.1):
+The statement matches the target exactly: existence iff every I_x is infinite. Sufficiency is correct. Necessity contains a proof bug: the text 'list every element of K at least once and then repeat x forever' is not a valid positive text, since after the tail begins no unseen elements can appear. A correct proof would interleave infinitely many repeats of x with a full enumeration of K. So the theorem recovered is right, but the written proof is not fully correct.
+
+3. Element-based impossibility (Theorem 3.2, first bullet):
+This is recovered extremely well, including the intended freshness criterion and the three-case split. The proof is detailed and sound.
+
+4. Index-based impossibility (Theorem 3.2, second bullet):
+The reconstruction uses the correct mod-4 two-language example and the same adversarial idea on C=4N. However, it changes the model by defining success as eventual exact identification L_{h(x_t)}=K. The original benchmark defines success only via eventual output of an index whose language is contained in the target. Since exact equality is stricter, this is not the same theorem/model. Under the benchmark's strictness, this mismatch is material.
+
+5. Definitions/presentation:
+There is a minor inconsistency in the empty-intersection convention for J_n(x): it first says the intersection is empty and then sets J_n(x)=N. The intended meaning is clear, so this is not a major issue.
+
+Overall:
+This is a high-quality near-reconstruction, but not a strict pass. The main positive theorem is excellent. The exact-boundary theorem has a proof gap in necessity, and the index-based theorem is stated in a changed model. Because the benchmark demands theorem equivalence under the same assumptions and a supporting proof, these prevent acceptance.

data/pdfs/400_off_run1.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:d61fc03bd539e08d7b491c4ce7084de8b267bae3560806c80e733824f16db2f9
+size 185206

data/pdfs/400_off_run2.comparison.md

@@ -0,0 +1,40 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 97
+- Proof quality: 95
+- Mean score: 4.0
+- Proof fidelity: Same
+- Proof completeness: Full
+
+## Major Successes
+
+- Recovers the central positive theorem with the correct setting: countable domain, finite/countable family of infinite languages, deterministic memoryless set-valued generator, finitely repeating texts, and eventual subset containment.
+- Gives the paper's explicit construction via J_n(x), n(x)=max{n<=x : J_n(x) infinite}, and G(x)=J_{n(x)}(x).
+- Proves success by defining the bad set B_K and showing B_K is finite using the key implication x in B_K => n(x)<z and the finite-union-of-finite-intersections argument.
+- Recovers the exact characterization for arbitrary repetitions via the one-point intersections I_x being infinite, with both necessity and sufficiency arguments.
+- Recovers both impossibility boundary statements: no memoryless element-based generator for any infinite target, and a concrete two-language family defeating all memoryless index-generators.
+
+## Major Errors
+
+- Very minor presentational deviation: uses indexing from 0 and notes J_0(x)=N, whereas the target statement used positive indexing and observed J_1(x) is infinite; this is harmless.
+- In the arbitrary-text necessity proof, the phrase 'first lists every element of K at least once and then repeats x forever' informally presumes a staged positive text over an infinite set; mathematically this just means choose any positive text with x repeated infinitely often after each element appears, so no substantive issue.
+
+## Budget Feedback
+
+Already sufficient. If compressing further, preserve the discriminator that the positive result requires finitely repeating texts and set-based outputs, plus the exact arbitrary-repetition characterization by infinite one-point intersections I_x.
+
+## Reasoning
+
+Criterion 1 is well above pass because the reconstruction matches the target theorem package essentially exactly: same model, assumptions, success notion, explicit generator, and companion boundary/impossibility statements. Criterion 2 is also above pass because the proofs are complete and sound, following the original mechanism closely. The main theorem proof includes all essential steps, the arbitrary-repetition theorem is proved in both directions, and the two negative results are substantiated with the right constructions. Minor notation/indexing differences do not alter the theorem.
+
+## Critique
+
+The reconstruction closely tracks the original answer key. For the main positive theorem, it correctly fixes a countable family of infinite languages over a countable domain, defines J_n(x) as the intersection of the first n languages containing x, sets n(x) to be the largest n<=x with J_n(x) infinite, and outputs G(x)=J_{n(x)}(x). The proof for target K=L_z uses the same bad-set strategy: define B_K={x in K: G(x) not subseteq K}, prove x in B_K implies n(x)<z, then for x>=z infer J_z(x) is finite and hence x belongs to a finite union U_z of finite intersections among L_1,...,L_z. Therefore B_K is finite, and finitely repeating texts eventually avoid B_K. This is exactly the original proof architecture.
+
+For the unrestricted-text boundary theorem, the reconstruction states the correct iff characterization: such a memoryless set-generator exists for all positive texts iff every I_x=intersection of all languages containing x is infinite. The necessity argument via repeating x indefinitely is the right one; the sufficiency argument choosing an infinite subset of I_x is also exactly right.
+
+For the necessity of set-based output, the reconstruction recovers both required statements. The element-based impossibility is not merely asserted; it gives the intended exhaustive case split (infinitely many immediately bad points, an infinite fiber, or infinitely many distinct images) and constructs a repetition-free text causing infinitely many failures in each case. The index-based impossibility uses the same two-language mod-4 example and the same argument based on infinitely many common points where one index is chosen infinitely often and is wrong for the other target.
+
+The remaining differences are cosmetic: 0-based indexing, a slightly different but equivalent definition of the finite exceptional union U_z, and some expository examples/intuition not needed for correctness. None changes the model, quantifiers, or proof obligations. This meets the benchmark cleanly.

data/pdfs/400_off_run2.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:649bb4314c6f0efb636d69c3b2250ee6c338aa876b01b3c1c6106ccf86f6d31e
+size 186302

data/pdfs/400_off_run3.comparison.md

@@ -0,0 +1,43 @@
+# Target vs Reconstruction Comparison
+
+- Pass: False
+- Sufficient: False
+- Theorem match: 88
+- Proof quality: 72
+- Mean score: 3.3
+- Proof fidelity: Similar
+- Proof completeness: Partial
+
+## Major Successes
+
+- Correctly reconstructs the main positive theorem for countable families of infinite languages on a countable domain under finitely repeating texts, including the explicit construction via J_n(x), n(x), and the finite bad-set argument.
+- Correctly reconstructs the exact characterization for arbitrary repetitions using the one-point intersections I_x and the repeat-x adversary.
+- Correctly includes the necessity of set-based output: impossibility for memoryless element-based generators and a two-language impossibility for index-based generators using the mod-4 example.
+
+## Major Errors
+
+- The index-generator notion is changed: the reconstruction requires eventual exact identification L_{h(x_t)}=K, whereas the target benchmark only requires eventual output of an index whose language is contained in the target. This alters the model/proof obligation, even though the supplied counterexample still witnesses failure.
+- The necessity proof for arbitrary repetitions informally uses a text that 'first enumerates every element of K at least once, and then repeats x forever', which is not literally a standard ω-sequence with a stage after all elements have appeared; this is a presentation flaw in a key argument, though fixable.
+- The element-generator impossibility proof's Case 3 contains a shaky combinatorial argument ('injective self-map... cannot satisfy s(t)>t for all sufficiently large t when restricted to all integers in an infinite initial block') that is not rigorously justified as written.
+
+## Budget Feedback
+
+Keep the theorem package, but repair proof rigor and model fidelity: (1) state the index-based success criterion exactly as eventual containment/subset, not eventual exact equality to the target; (2) tighten the arbitrary-repetition necessity proof by using a bona fide text with infinitely many x's interleaved after an initial covering stage argument, or simply argue that if x occurs infinitely often then eventual success forces G(x)⊆K; (3) replace the element-generator Case 3 with a clean diagonal/counting argument matching the paper’s exhaustive split. These fixes would likely move this to a pass.
+
+## Reasoning
+
+The reconstruction is very close to the target package. It gets the central theorem, assumptions, explicit generator, and the sharp arbitrary-repetition characterization essentially right. It also includes the intended negative results and even the specific two-language mod-4 example. However, the benchmark is strict about preserving the exact model and proof obligations. The reconstruction changes the index-based model from eventual output of a language contained in the target to eventual exact identification of the target language; that is not harmless. On proof quality, the main theorem proof is solid, and the characterization proof is directionally correct, but there are notable rigor problems: the necessity proof for arbitrary texts is awkwardly phrased with an impossible 'after every element has appeared, repeat x forever' sequencing, and the element-generator impossibility's third case is not convincingly established as written. Thus theorem match falls just short of pass threshold, and proof quality is below threshold.
+
+## Critique
+
+Comparison to target theorem:
+
+1. Main positive theorem (Theorem 1.1): The reconstruction matches the target essentially exactly. It works over a countable domain identified with N, takes a finite or countable family of infinite languages with an enumeration in which each language appears at least once, defines J_n(x)=∩{L_j:j≤n and x∈L_j}, lets n(x)=max{n≤x:J_n(x) infinite}, and sets G(x)=J_{n(x)}(x). The proof via the finite bad set B_K and the finite exceptional union U_z is faithful and complete. This is a strong success.
+
+2. Characterization under arbitrary repetitions (Theorem 3.1): The statement is correct and equivalent to the target. The proof idea is also the same: necessity by infinitely repeating a bad x, sufficiency by choosing G(x)⊆I_x. The only issue is expository rigor in the necessity direction: a positive text cannot literally have a finite prefix containing every element of an infinite K and then continue with only x forever. The underlying argument is recoverable, but the proof as written is loose.
+
+3. Element-based impossibility: The theorem statement matches the target in substance and is even slightly stronger by producing a repetition-free text. The proof follows the summary’s three-case split. Cases 1 and 2 are fine. Case 3 has the right high-level mechanism but the final combinatorial contradiction is not rigorously established. It is plausible but not fully sound as presented.
+
+4. Index-based impossibility: The reconstructed example is the correct one and the diagonal idea on the common core C=4N is faithful. However, the reconstruction changes the definition of success for an index-generator to eventual exact equality L_{h(x_t)}=K. In the target benchmark, success only requires eventual output of an index whose language is contained in the target (hence eventual containment of the output language in K). Since model changes are disallowed, this counts against theorem match. The given counterexample still works for the stronger exact-identification notion, but the statement is no longer the same theorem.
+
+Overall: excellent recovery of the paper-specific theorem package and proof mechanism, but not enough for a strict pass because one companion theorem is stated in a different model and one negative proof remains materially shaky.

data/pdfs/400_off_run3.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:32059b975c058fd74e6586ccde4aac3de87d33fb96aa4fad67f928f4c6335a58
+size 190937

data/pdfs/400_on_run1.comparison.md

@@ -0,0 +1,45 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 98
+- Proof quality: 93
+- Mean score: 3.83
+- Proof fidelity: Same
+- Proof completeness: Full
+
+## Major Successes
+
+- Correctly states the central positive theorem for memoryless set-based generation on finitely repeating texts over any finite/countable family of infinite languages on a countable domain.
+- Recovers the explicit construction using J_n(x), n(x)=max{n≤x: J_n(x) infinite}, and G(x)=J_{n(x)}(x).
+- Proof of the main theorem matches the paper's mechanism: define the bad set B_K, show bad points imply n(x)<z, then for x≥z force x into a finite exceptional union U_z, hence B_K finite and finitely repeating texts eventually avoid it.
+- Correctly includes the exact characterization under arbitrary repetitions via the infinitude of I_x=⋂{L:x∈L}.
+- Correctly includes both necessity results for weaker output models: impossibility for memoryless element-output and a two-language mod-4 counterexample for index-output.
+
+## Major Errors
+
+- Minor indexing/convention difference: the reconstruction uses ℕ={0,1,2,...} and allows n=0 with J_0(x)=ℕ, whereas the target phrasing used positive integers and observed J_1(x) is already infinite. This is harmless.
+- The index-generator impossibility theorem is stated for failure on all positive texts rather than explicitly under finitely repeating texts, but the provided adversarial text is repetition-free, so it still implies the target boundary statement.
+- A few expository references to prior context paper are extraneous to the benchmark, though they do not alter the theorem or proof.
+
+## Budget Feedback
+
+Already sufficient. If tightening were needed, remove the external citation/context remarks and state Theorem 3.2 explicitly with the finitely-repeating qualifier for the index-based impossibility to match the paper's wording exactly.
+
+## Reasoning
+
+Criterion 1 is very high because the reconstruction recovers the exact main theorem, the explicit generator, the arbitrary-repetition characterization, and the necessity of set-based output. The few differences are not substantive: shifting to 0-based indexing is harmless, and the impossibility statements are at least as strong as required. Criterion 2 is also high because the proofs are sound and largely complete. The main theorem proof follows the original line-by-line. The boundary theorem proof is correct. The element-based impossibility uses the same three-case architecture indicated in the summary and gives a workable ordering argument in the final case; while somewhat reconstructed, it is logically adequate. The index-based mod-4 argument is correct. Therefore the reconstruction meets the strict benchmark.
+
+## Critique
+
+Detailed comparison:
+
+Main theorem: The original target requires a countable domain, finite or countable family of infinite languages, memoryless set-valued output, finitely repeating enumerations, eventual subset containment, and the explicit construction via J_n(x), n(x), G(x). The reconstruction includes all of these exactly. It identifies X with ℕ, allows repeated languages in the enumeration, defines positive text and finitely repeating text correctly, and states success as eventual containment G(x_t)⊆K. The explicit formulas match. The proof mirrors the original audit: well-definedness of n(x), fix K=L_z, define B_K, show x∈B_K implies n(x)<z, then if x≥z deduce J_z(x) finite, place x in a finite union U_z of finite intersections among L_1,...,L_z, conclude B_K finite, and use finite repetition to get eventual avoidance. This is essentially the same proof.
+
+Boundary theorem under arbitrary repetitions: The target states iff every I_x is infinite. The reconstruction states exactly that and proves necessity by enumerating K once then repeating x forever, and sufficiency by choosing any infinite subset of I_x. This is faithful both in theorem and mechanism.
+
+Necessity of set-based output: For element-based generators, the target asks that no infinite language is generable by a memoryless element-based generator under finitely repeating enumerations. The reconstruction proves a slightly stronger statement: no memoryless element-generator succeeds on all repetition-free texts of a fixed infinite K, hence not on all finitely repeating texts. This is fully compatible and stronger. The proof follows the summary's three-case split: infinitely many immediately bad points; else an infinite fiber causing repeated already-seen outputs; else infinitely many distinct good images with an ordering argument ensuring outputs are earlier in the text infinitely often. This is sufficiently rigorous for the stated theorem.
+
+For index-based generators, the target asks for existence of a two-language family not generable by any memoryless index-generator under finitely repeating enumerations. The reconstruction uses the exact mod-4 pair and the same intersection argument on C=4ℕ. Although the theorem statement says 'all positive texts' rather than explicitly 'finitely repeating texts', the adversarial text chosen begins with infinitely many distinct c∈C and is thus repetition-free/finitely repeating, so it indeed proves the target impossibility.
+
+Specificity and calibration: The submission is highly specific to the paper and does not invent incompatible details. It even flags some reconstruction choices. The only mild overreach is the unnecessary mention of a prior paper/context, but this does not affect theorem recovery.

data/pdfs/400_on_run1.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:969f704ee6360d6acc7ff02b87f888ee06df6ae162c061e0474f3ed5b8796d32
+size 208725

data/pdfs/400_on_run2.comparison.md

@@ -0,0 +1,45 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 98
+- Proof quality: 94
+- Mean score: 3.83
+- Proof fidelity: Same
+- Proof completeness: Full
+
+## Major Successes
+
+- Recovers the central positive theorem exactly in the memoryless set-based model for finite or countable families of infinite languages over a countable domain under finitely repeating texts.
+- Includes the explicit construction via J_n(x), n(x)=max{n≤x: J_n(x) infinite}, and G(x)=J_{n(x)}(x).
+- Reproduces the finite-bad-set proof structure using B_K, the implication x in B_K => n(x)<z, and the finite exceptional union U_z of finite intersections among L_1,...,L_z.
+- Recovers the exact iff characterization for arbitrary repetitions using I_x and the repeat-x-forever adversary.
+- Recovers the necessity of set-based outputs with both impossibility statements: no element-based memoryless generator for infinite targets and a two-language counterexample for index-based generation.
+
+## Major Errors
+
+- Minor indexing/notation drift: uses ℕ starting at 0 and J_0(x)=ℕ instead of the original's 1-based presentation; harmless but not identical.
+- The arbitrary-repetition necessity proof phrases the contradiction via a text that first enumerates K once then repeats x forever; this is fine, but the sentence 'therefore G(x)⊆K for every language K containing x' compresses the per-target argument slightly.
+- The notes mention minimal contextual reading of a prior paper even though the benchmark asks for reconstruction from the compressed summary; this does not materially affect theorem recovery but weakens calibration a bit.
+
+## Budget Feedback
+
+Main benchmark is already met. If tightening further, remove extraneous contextual claims and make explicit that the unrestricted characterization is equivalent to one-example generation in the full-memory/set-based sense, to match the paper's framing even more closely.
+
+## Reasoning
+
+Criterion 1 is very high because the reconstruction states the same central theorem under the same model and assumptions: countable domain, finite/countable family of infinite languages, deterministic memoryless set-valued generator, finitely repeating positive texts, and eventual subset containment. It also includes the explicit construction and both companion boundary results from Theorems 3.1 and 3.2. The only reason not to assign 100 is minor presentational drift (0-based indexing, some wording differences, and extra contextual remarks). Criterion 2 is also high because the proofs are logically sound and substantially complete. The main theorem proof closely follows the paper's audited argument and correctly shows the bad set is finite. The arbitrary-repetition characterization is proved in both directions with the right adversarial mechanism. The impossibility results for element- and index-based generators are supported by full arguments, not mere sketches. I saw no fatal gap or assumption change. Hence the reconstruction satisfies the strict pass criterion.
+
+## Critique
+
+The reconstruction is faithful to the original theorem package.
+
+Main theorem: The statement matches the original benchmark target almost exactly. It preserves the setting (countable domain identified with ℕ, countable family of infinite languages, memoryless deterministic set-based generator, finitely repeating positive texts, eventual containment G(x_t)⊆K). It also reproduces the explicit generator J_n(x), n(x), G(x). The proof uses the same mechanism as the original: fix K=L_z, define the bad set B_K, show x∈B_K implies n(x)<z, then for x≥z deduce J_z(x) is finite and therefore x lies in a finite union U_z of finite intersections from the first z languages. Conclude B_K is finite and finitely repeating texts eventually avoid it. This is essentially the paper's proof.
+
+Arbitrary repetitions boundary: The theorem is the same iff characterization. Sufficiency chooses any infinite subset of I_x; necessity uses the 'enumerate K then repeat x forever' adversarial text to force G(x) to be simultaneously safe for every target containing x, yielding G(x)⊆I_x and contradiction if I_x is finite. This is the correct boundary statement and proof idea.
+
+Necessity of set-based outputs: The reconstruction correctly states both impossibility results required by the benchmark. For element-valued generators, it gives a complete case split aligned with the summary: infinitely many immediately bad points, or an infinite fiber, or infinitely many distinct good images; each case produces a repetition-free text with infinitely many failures. For index-valued generators, it uses the exact two-language mod-4 example and the correct shared core C=4ℕ argument. These are specific and faithful.
+
+Differences: The reconstruction adds some exposition, examples, and a note referencing a prior paper. None of this changes the theorem or proof obligations. There is minor indexing drift (starting ℕ at 0 and using J_0(x)=ℕ), but the construction is equivalent. The note about minimal contextual reading is potentially awkward from a benchmark perspective, but because the mathematics recovered is correct and specific, it does not undermine sufficiency.
+
+Overall, this is a passing reconstruction: same theorem package, same assumptions, same core proof mechanisms, and sufficiently complete proofs.

data/pdfs/400_on_run2.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:ab6f1cb1ecc4799339fc092fba464594f16e59249b8d3e35f2a846785db8c293
+size 184913

data/pdfs/400_on_run3.comparison.md

@@ -0,0 +1,39 @@
+# Target vs Reconstruction Comparison
+
+- Pass: True
+- Sufficient: True
+- Theorem match: 99
+- Proof quality: 95
+- Mean score: 4.0
+- Proof fidelity: Same
+- Proof completeness: Full
+
+## Major Successes
+
+- Recovers the exact main positive theorem for memoryless set-based generation over countable families of infinite languages on countable domains under finitely repeating texts.
+- Includes the explicit construction J_n(x), n(x), and G(x) with the same bad-set/U_z proof mechanism as the original.
+- Recovers the exact characterization under arbitrary repetitions via infinitude of I_x, with both directions proved.
+- Recovers both necessity results for element-based and index-based memoryless generators, including the same two-language mod-4 counterexample.
+
+## Major Errors
+
+- Minor convention shift: defines J_0(x)=X and allows 0 in the maximization, whereas the original audit phrases n(x)=max{n≤x: J_n(x) infinite} with indices starting at 1; this is harmless and equivalent.
+- Necessity proof for arbitrary repetitions informally constructs a text by 'after every element has appeared once, repeat x forever'; phrasing is slightly awkward but mathematically clear.
+
+## Budget Feedback
+
+No major repair needed. If tightening further, align indexing conventions exactly with the original statement (start at 1 rather than introducing J_0) and trim ancillary exposition.
+
+## Reasoning
+
+Criterion 1 is essentially perfect because the reconstruction states the same central theorem under the same model and assumptions: countable domain, finite or countable family of infinite languages, deterministic memoryless set-valued generator, finitely repeating texts, and eventual subset containment. It also includes the precise boundary theorems: the iff characterization for arbitrary repetitions and the impossibility of element-based/index-based memoryless generation. Criterion 2 is high because full proofs are given and they are sound. The main theorem uses exactly the intended finite bad-set argument via n(x)<z and the finite union U_z. The unrestricted-repetition characterization is proved correctly in both directions. The element-based impossibility uses the intended exhaustive case split, and the index-based impossibility uses the correct explicit mod-4 family. Any deviations are merely notational/conventional and do not alter the theorem.
+
+## Critique
+
+The reconstruction is extremely close to the target answer key. On the main theorem, it identifies the same setting and success notion, fixes an enumeration of the language family with duplicates allowed, defines J_n(x) as the intersection of languages among the first n containing x, defines n(x) as the largest admissible index up to x for which J_n(x) is infinite, and sets G(x)=J_{n(x)}(x). The proof then fixes K=L_z, defines the bad set B_K, proves x in B_K implies n(x)<z, then for x≥z derives J_z(x) finite and hence x lies in U_z, a finite union of finite intersections among the first z languages. This yields finiteness of B_K and eventual avoidance on finitely repeating texts. That is exactly the original mechanism.
+
+For the arbitrary-repetition boundary theorem, the reconstruction matches the original iff statement using I_x and correctly explains necessity by repeating x forever after a complete initial enumeration, and sufficiency by choosing G(x) as an infinite subset of I_x. This preserves the sharp boundary of the main theorem.
+
+For necessity of set-based output, the reconstruction includes both parts required by the benchmark. The element-generator impossibility is not merely stated abstractly; it uses the same combinatorial trichotomy described in the answer key: infinitely many immediately bad points, an infinite fiber over some y, or infinitely many distinct images from good points. The index-generator impossibility uses exactly the two languages L1={0,1 mod 4} and L2={0,2 mod 4} and the common core C=4N, with the standard pigeonhole argument on which index appears infinitely often on C.
+
+The proof fidelity is therefore 'Same' rather than merely 'Similar': it reproduces the same construction and argument structure, not just an equivalent theorem. Completeness is full: all relevant steps are supplied, and there are no material proof gaps. The only differences are harmless indexing conventions (introducing J_0) and some extra pedagogical remarks/examples. These do not weaken or alter the theorem. This reconstruction clearly meets the benchmark.

data/pdfs/400_on_run3.pdf

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:d1c02e53633dd099af64a06c0b135edadd620e0a01029ef7f3b1e7d35755f642
+size 200532

data/ranking.json

@@ -0,0 +1,203 @@
+{
+  "ranking": [
+    {
+      "id": "R01",
+      "rank": 1,
+      "tier": "pass",
+      "score": 96,
+      "one_line": "Most faithful overall: exact main theorem and characterization, plus rigorous element- and index-impossibility proofs.",
+      "budget": 400,
+      "condition": "off",
+      "run": 3,
+      "trial": "400_off_run3"
+    },
+    {
+      "id": "R04",
+      "rank": 2,
+      "tier": "pass",
+      "score": 95,
+      "one_line": "Very strong and complete; matches the target closely with solid proofs of all three boundary results.",
+      "budget": 400,
+      "condition": "on",
+      "run": 2,
+      "trial": "400_on_run2"
+    },
+    {
+      "id": "R09",
+      "rank": 3,
+      "tier": "pass",
+      "score": 94,
+      "one_line": "Accurate statements and rigorous proofs throughout, including a clean correct three-case element-generator impossibility.",
+      "budget": 400,
+      "condition": "off",
+      "run": 2,
+      "trial": "400_off_run2"
+    },
+    {
+      "id": "R15",
+      "rank": 4,
+      "tier": "pass",
+      "score": 93,
+      "one_line": "Faithful package with correct main/boundary theorems and a solid element-generator impossibility proof.",
+      "budget": 400,
+      "condition": "on",
+      "run": 3,
+      "trial": "400_on_run3"
+    },
+    {
+      "id": "R11",
+      "rank": 5,
+      "tier": "pass",
+      "score": 92,
+      "one_line": "Excellent reconstruction; only minor formulation blemishes, but proofs substantially recover the target package.",
+      "budget": 400,
+      "condition": "on",
+      "run": 1,
+      "trial": "400_on_run1"
+    },
+    {
+      "id": "R06",
+      "rank": 6,
+      "tier": "pass",
+      "score": 91,
+      "one_line": "Strong on the main theorem and arbitrary-repetition characterization, with a convincing correct element-generator diagonal.",
+      "budget": 300,
+      "condition": "off",
+      "run": 1,
+      "trial": "300_off_run1"
+    },
+    {
+      "id": "R02",
+      "rank": 7,
+      "tier": "borderline",
+      "score": 85,
+      "one_line": "Main theorem and arbitrary-text characterization are excellent, but the arbitrary-text necessity proof wrongly uses an invalid 'starts with infinitely many copies of x' text.",
+      "budget": 200,
+      "condition": "off",
+      "run": 3,
+      "trial": "200_off_run3"
+    },
+    {
+      "id": "R03",
+      "rank": 8,
+      "tier": "borderline",
+      "score": 82,
+      "one_line": "Main positive theorem and characterization are good, but the element-generator proof is reconstructed with a genuine gap in the hard case.",
+      "budget": 300,
+      "condition": "on",
+      "run": 1,
+      "trial": "300_on_run1"
+    },
+    {
+      "id": "R13",
+      "rank": 9,
+      "tier": "borderline",
+      "score": 80,
+      "one_line": "Gets the package mostly right, but the element-generator impossibility proof is incorrect as written despite strong positive parts.",
+      "budget": 200,
+      "condition": "off",
+      "run": 2,
+      "trial": "200_off_run2"
+    },
+    {
+      "id": "R14",
+      "rank": 10,
+      "tier": "borderline",
+      "score": 79,
+      "one_line": "Main and arbitrary-text set-generator theorems are good, but the element-generator proof has unresolved repetition/distinctness issues.",
+      "budget": 200,
+      "condition": "off",
+      "run": 1,
+      "trial": "200_off_run1"
+    },
+    {
+      "id": "R12",
+      "rank": 11,
+      "tier": "borderline",
+      "score": 76,
+      "one_line": "Positive theorem is faithful, but it uses exact-identification rather than subset-correctness for index-generators and the element proof is not rigorous.",
+      "budget": 300,
+      "condition": "off",
+      "run": 3,
+      "trial": "300_off_run3"
+    },
+    {
+      "id": "R05",
+      "rank": 12,
+      "tier": "borderline",
+      "score": 74,
+      "one_line": "Main theorem and arbitrary-repetition theorem are correct, but it explicitly leaves a gap in the element-generator impossibility proof.",
+      "budget": 300,
+      "condition": "off",
+      "run": 2,
+      "trial": "300_off_run2"
+    },
+    {
+      "id": "R18",
+      "rank": 13,
+      "tier": "borderline",
+      "score": 72,
+      "one_line": "Main theorem and arbitrary-text boundary are solid, but the element-generator proof is acknowledgedly non-rigorous.",
+      "budget": 300,
+      "condition": "on",
+      "run": 2,
+      "trial": "300_on_run2"
+    },
+    {
+      "id": "R10",
+      "rank": 14,
+      "tier": "fail",
+      "score": 66,
+      "one_line": "Good positive theorem, but arbitrary-text necessity wrongly uses the constant text x,x,x,... for infinite K, and the index proof mishandles memorylessness.",
+      "budget": 200,
+      "condition": "on",
+      "run": 3,
+      "trial": "200_on_run3"
+    },
+    {
+      "id": "R17",
+      "rank": 15,
+      "tier": "fail",
+      "score": 62,
+      "one_line": "Omits the element-generator theorem statement/proof entirely from the main theorem package despite good positive/set-based results.",
+      "budget": 200,
+      "condition": "on",
+      "run": 2,
+      "trial": "200_on_run2"
+    },
+    {
+      "id": "R07",
+      "rank": 16,
+      "tier": "fail",
+      "score": 58,
+      "one_line": "Main theorem proof is flawed (uses J_{n(x)+1}(x) and incorrectly claims it includes L_z), and element impossibility is only sketched.",
+      "budget": 300,
+      "condition": "on",
+      "run": 3,
+      "trial": "300_on_run3"
+    },
+    {
+      "id": "R16",
+      "rank": 17,
+      "tier": "fail",
+      "score": 54,
+      "one_line": "Main set-based theorem is fine, but it misstates index-generator success as eventual equality K rather than eventual subset containment, changing the theorem package.",
+      "budget": 400,
+      "condition": "off",
+      "run": 1,
+      "trial": "400_off_run1"
+    },
+    {
+      "id": "R08",
+      "rank": 18,
+      "tier": "fail",
+      "score": 38,
+      "one_line": "Although the main theorem is good, the index-generator counterexample illegally uses infinitely repeated 0 under a finitely repeating requirement and the element proof is not rigorous.",
+      "budget": 200,
+      "condition": "on",
+      "run": 1,
+      "trial": "200_on_run1"
+    }
+  ],
+  "notes": "The top candidates precisely matched the target statements, especially the subset-based notion for index generators, and gave genuinely complete proofs of the main theorem, the arbitrary-repetition characterization, and the two impossibility results. Middle candidates usually had the main theorem right but stumbled on one delicate proof, most often the element-generator impossibility or the arbitrary-repetition necessity argument. The bottom candidates changed a theorem statement (especially the index-generator criterion), used inadmissible texts, or left major gaps."
+}

data/ranking.md

@@ -0,0 +1,36 @@
+# Blinded comparative ranking of reconstructions
+
+Judge: `openai/azure/gpt-5.4` — one call, 18 candidates, shuffled (seed 7), OFF/ON hidden until after ranking.
+
+| rank | budget | condition | run | tier | score | reason |
+|---:|---:|:--|---:|:--|---:|:--|
+| 1 | 400 | off | 3 | pass | 96 | Most faithful overall: exact main theorem and characterization, plus rigorous element- and index-impossibility proofs. |
+| 2 | 400 | on | 2 | pass | 95 | Very strong and complete; matches the target closely with solid proofs of all three boundary results. |
+| 3 | 400 | off | 2 | pass | 94 | Accurate statements and rigorous proofs throughout, including a clean correct three-case element-generator impossibility. |
+| 4 | 400 | on | 3 | pass | 93 | Faithful package with correct main/boundary theorems and a solid element-generator impossibility proof. |
+| 5 | 400 | on | 1 | pass | 92 | Excellent reconstruction; only minor formulation blemishes, but proofs substantially recover the target package. |
+| 6 | 300 | off | 1 | pass | 91 | Strong on the main theorem and arbitrary-repetition characterization, with a convincing correct element-generator diagonal. |
+| 7 | 200 | off | 3 | borderline | 85 | Main theorem and arbitrary-text characterization are excellent, but the arbitrary-text necessity proof wrongly uses an invalid 'starts with infinitely many copies of x' text. |
+| 8 | 300 | on | 1 | borderline | 82 | Main positive theorem and characterization are good, but the element-generator proof is reconstructed with a genuine gap in the hard case. |
+| 9 | 200 | off | 2 | borderline | 80 | Gets the package mostly right, but the element-generator impossibility proof is incorrect as written despite strong positive parts. |
+| 10 | 200 | off | 1 | borderline | 79 | Main and arbitrary-text set-generator theorems are good, but the element-generator proof has unresolved repetition/distinctness issues. |
+| 11 | 300 | off | 3 | borderline | 76 | Positive theorem is faithful, but it uses exact-identification rather than subset-correctness for index-generators and the element proof is not rigorous. |
+| 12 | 300 | off | 2 | borderline | 74 | Main theorem and arbitrary-repetition theorem are correct, but it explicitly leaves a gap in the element-generator impossibility proof. |
+| 13 | 300 | on | 2 | borderline | 72 | Main theorem and arbitrary-text boundary are solid, but the element-generator proof is acknowledgedly non-rigorous. |
+| 14 | 200 | on | 3 | fail | 66 | Good positive theorem, but arbitrary-text necessity wrongly uses the constant text x,x,x,... for infinite K, and the index proof mishandles memorylessness. |
+| 15 | 200 | on | 2 | fail | 62 | Omits the element-generator theorem statement/proof entirely from the main theorem package despite good positive/set-based results. |
+| 16 | 300 | on | 3 | fail | 58 | Main theorem proof is flawed (uses J_{n(x)+1}(x) and incorrectly claims it includes L_z), and element impossibility is only sketched. |
+| 17 | 400 | off | 1 | fail | 54 | Main set-based theorem is fine, but it misstates index-generator success as eventual equality K rather than eventual subset containment, changing the theorem package. |
+| 18 | 200 | on | 1 | fail | 38 | Although the main theorem is good, the index-generator counterexample illegally uses infinitely repeated 0 under a finitely repeating requirement and the element proof is not rigorous. |
+
+## Mean rank by cell (lower = better)
+
+| budget | OFF mean-rank (tiers) | ON mean-rank (tiers) |
+|---:|:--|:--|
+| 200 | 8.7 (b,b,b) | 15.7 (f,f,f) |
+| 300 | 9.7 (b,b,p) | 12.3 (b,b,f) |
+| 400 | 7.0 (f,p,p) | 3.7 (p,p,p) |
+
+## Judge notes
+
+The top candidates precisely matched the target statements, especially the subset-based notion for index generators, and gave genuinely complete proofs of the main theorem, the arbitrary-repetition characterization, and the two impossibility results. Middle candidates usually had the main theorem right but stumbled on one delicate proof, most often the element-generator impossibility or the arbitrary-repetition necessity argument. The bottom candidates changed a theorem statement (especially the index-generator criterion), used inadmissible texts, or left major gaps.

data/report.md

@@ -0,0 +1,59 @@
+# Does a prior reference paper lower a theorem's compression threshold?
+
+**Case:** *On Language Generation in the Limit with Bounded Memory* (arXiv 2605.30324)
+**Reference (context) paper:** Kleinberg & Mullainathan, *Language Generation in the Limit* (arXiv 2404.06757)
+**Judge / all roles:** `gpt-5.4` · **Design:** budgets {200, 300, 400} × {OFF, ON} × 3 trials.
+
+## The question
+
+A compressor writes an *N*-word summary of a paper's main theorem; a fresh,
+memoryless reconstructor rebuilds the full theorem + proof from **only** that
+summary. **OFF** = summary alone. **ON** = the reconstructor may also page through
+the prior reference paper as a tool. Does having the ancestor paper let a *shorter*
+summary succeed — i.e. lower the compression threshold?
+
+## Pass/fail results
+
+| Budget | OFF (no PDF) | ON (with PDF) |
+|---:|:--|:--|
+| 200 | 2/3 — mean 3.66 | 1/3 — mean 3.18 |
+| 300 | 1/3 — mean 3.68 | 0/3 — mean 3.57 |
+| 400 | 1/3 — mean 3.50 | **3/3 — mean 3.89** |
+
+## Blinded comparative ranking (all 18 judged at once)
+
+Because per-trial pass/fail is noisy near the acceptance bar, all 18 reconstructions
+were re-judged in **one call**, shuffled behind neutral IDs with OFF/ON hidden until
+after ranking. Mean rank of 18 (lower = better):
+
+| Budget | OFF mean rank | ON mean rank |
+|---:|:--:|:--:|
+| 200 | 8.7 | 15.7 |
+| 300 | 9.7 | 12.3 |
+| 400 | **7.0** | **3.7** |
+
+## What it shows
+
+- **400 with the reference paper is the clear winner** — 3/3 passes, and the top of
+  the blinded ranking is dominated by 400 trials (mean rank 3.7 for 400-ON). This is
+  the one robust, reproducible signal.
+- **The context sign flips with budget** (OFF ranks better at 200, ON better at 400),
+  so there is **no consistent context effect** across budgets.
+- **Variance dominates budget below 400.** Identical prompts and conditions produce
+  0/3–2/3 swings; 200 and 300 cells are statistically indistinguishable. Which
+  reconstruction happens to nail the one hard lemma (the **element-generator
+  impossibility proof**) decides the outcome — not the budget or the context paper.
+
+## Caveats
+
+- **n=3 per cell, one paper, one context paper** — a pilot, not a significance claim.
+- Below 400 the result is close to a coin-flip on a single lemma.
+- Ranking is one judge at one shuffle (seed 7); top/bottom robust, mid-order may vary.
+- ON was genuinely used: all ON reconstructions actually read the reference PDF
+  (verified via tool calls), so a null/negative effect is not an "ignored the file"
+  artifact.
+
+**Bottom line:** the reference paper reliably helps only at 400 words; below that,
+reconstruction quality is governed by per-trial variance on one hard proof, which
+the prior paper does not stabilize. Explore the individual reconstructions and
+evaluator verdicts in the **Runs** tab.

data/summary.md

@@ -0,0 +1,9 @@
+# Off-vs-on context experiment — acceptance by budget
+
+Cell = pass-rate (accepted / trials), mean of mean_score.
+
+| budget | off (no PDF) | on (with PDF) |
+|---:|:---|:---|
+| 200 | 2/3 pass, mean 3.66 | 1/3 pass, mean 3.18 |
+| 300 | 1/3 pass, mean 3.68 | 0/3 pass, mean 3.57 |
+| 400 | 1/3 pass, mean 3.50 | 3/3 pass, mean 3.89 |

requirements.txt

@@ -0,0 +1,3 @@
+gradio>=4.44
+pandas>=2.0
+matplotlib>=3.7