Pre-register the launcher A/B and add the extension arm

PREREGISTRATION.md

@@ -0,0 +1,101 @@
+# Pre-registration: does the launcher suppress accumulation?
+
+Registered 20 August 2026, before any submission was assigned to an arm.
+
+## Why this document exists
+
+The claim under test is the manifesto's: that machine-generated mathematics,
+admitted without human taste, accumulates into reusable internal theory. That
+is a claim about the import graph. Fixing the threshold after seeing the data
+would make any outcome arguable, so the threshold is fixed here, first.
+
+## What is already known
+
+Measured 20 August 2026 (see `carlok/lean-corpus-density`):
+
+- LeanFrontier at 24 modules has 4 internal import edges, 0.17 per module.
+- Tau Ceti at 24 modules had 22, 0.92 per module, and its density rises
+  monotonically to 1.55 by 2314 modules. Machine-generated mathematics does
+  accumulate there.
+- Tau Ceti is directed by human-written roadmaps. A roadmap specifies a
+  dependency graph in advance, so it does not settle whether accumulation
+  happens without one.
+- LeanFrontier's own launcher tells producers to "prefer an uncovered area",
+  which points away from the corpus. The observed sparsity may therefore be an
+  artifact of the instruction rather than a property of machine mathematics.
+
+That last point is what this experiment separates.
+
+## Hypothesis
+
+Producers instructed to extend the existing corpus will form import edges at a
+higher rate than producers given the current launcher.
+
+## Design
+
+Two arms, differing in exactly one paragraph of the task launcher:
+
+- **A (control)** — `prompts/TRY-LEANFRONTIER.md`, unchanged.
+- **B (extension)** — `prompts/TRY-LEANFRONTIER-EXTEND.md`, which directs the
+  producer to read the catalogue, pick an accepted submission, and prove
+  something depending on it.
+
+Every other instruction, and the receiver itself, is identical across arms. A
+test asserts the two files differ only in the designated block.
+
+Assignment is made by the maintainer when a producer is invited, alternating
+between arms, and recorded in `experiments/launcher-ab.csv` at the time of
+assignment rather than at merge. Submissions not assigned to an arm — walk-ins
+who found the repository themselves — are recorded as unassigned and excluded.
+
+## Metric
+
+Internal import edges whose **source** is a module belonging to that arm's
+submissions: what the producer did, not what was later done to them. Counted
+per module. Edges into modules from either arm count equally; the corpus is
+shared.
+
+Secondary, reported but not used for the decision: edges per declaration,
+maximum in-degree, and whether any module reaches depth 3.
+
+## Decision rule
+
+Stop at **18 accepted submissions per arm**. At that size, with arm A held at
+its observed 0.17 edges per module and α = 0.05 one-sided:
+
+| arm B reaches | vs control | power at 18/arm |
+|---|---|---|
+| 0.92 (Tau Ceti's rate) | 5.5× | 0.93 |
+| 0.70 | 4.2× | 0.82 |
+| 0.50 | 3.0× | 0.39 |
+| 0.40 | 2.4× | 0.16 |
+
+- **Arm B significantly above arm A** (conditional binomial, one-sided,
+  α = 0.05): the sparsity was an instruction artifact. The launcher is fixed
+  and the manifesto's claim survives this test.
+- **No significant difference**: an effect of 4× or larger is ruled out at 82%
+  power. This is *not* a finding of no effect. Effects below 3× need 34+ per
+  arm and 2.4× needs 65+, which this project cannot reach at its current rate.
+  That outcome will be reported as "no effect larger than ~4x", never as "no
+  accumulation".
+
+Either way the numbers are published, including a null.
+
+## What would falsify the hypothesis
+
+Arm B producing edges at or below arm A's rate. That would mean producers
+directly instructed to build on machine-generated results still do not, which
+is evidence against the manifesto's claim and not merely absence of evidence.
+
+## Known limitations, recorded in advance
+
+- Both launcher files are public, so an arm B producer can read arm A and vice
+  versa. Assignment cannot be enforced, only recorded.
+- Arm B measures compliance as much as capability: a producer told to import
+  something will import something. This is why the secondary metrics —
+  depth 3, in-degree above 1, cross-producer reuse — matter for interpreting a
+  positive result. A one-import-and-stop pattern is compliance, not
+  accumulation.
+- Assignment alternates rather than being randomised, and the maintainer knows
+  the arm when inviting. Recruitment is not blind.
+- 18 per arm is 36 submissions against a corpus that took 23 to date.

experiments/launcher-ab.csv

@@ -0,0 +1,3 @@
+# Arm assignment for the launcher A/B; see PREREGISTRATION.md.
+# Recorded at invitation, not at merge. "unassigned" = walk-in, excluded.
+submission_id,arm,assigned_utc

prompts/TRY-LEANFRONTIER-EXTEND.md

@@ -0,0 +1,60 @@
+# Try LeanFrontier with an agent (extension arm)
+
+You are an agent preparing one ordinary LeanFrontier mathematical submission.
+Your goal is a pull request that the local receiver accepts without maintainer
+repair.
+
+Repository: `https://github.com/carlok/LeanFrontier`
+
+## Read first
+
+Read these files in order. They are the source of truth; this page is only a
+short task launcher.
+
+1. [`CONTRACT.md`](../CONTRACT.md) — binding protocol.
+2. [`prompts/SUBMITTER.md`](SUBMITTER.md) — library and submission rules.
+3. [`README.md`](../README.md) — local setup and validation command.
+4. The generated [catalogue](../docs/catalogue/index.html), then the source and
+   claim of one accepted submission that is relevant to your chosen area.
+
+Do not change trusted infrastructure. An ordinary submission changes only:
+
+- ordinary Lean source beneath `LeanFrontier/`; and
+- exactly one new `Submissions/<submission-id>.json` claim.
+
+## Produce one candidate
+
+Start from current `main` in a fork or branch. Read the catalogue and choose an
+accepted submission to build on. Import its module and prove something that
+depends on it: a generalization, a consequence, or a result that needs it as a
+lemma. A near duplicate is still a near duplicate and will be rejected. Write a
+small, general, importable subject module with a stable mathematical namespace
+below `LeanFrontier.`.
+
+State one or more qualified theorem entrypoints in the claim. Keep your
+provenance fields accurate. Do not use `sorry`, `sorryAx`, `axiom`, unsafe or
+metaprogramming commands, generated payloads, producer-specific namespaces, or
+a sweep of trivial/permuted examples, including one continued from a submission
+already accepted. Do not add aliases merely for a future
+Mathlib migration.
+
+The receiver checks the elaborated declarations, including their transitive
+axiom closure, exact duplicate fingerprints, baseline-only triviality probes,
+and a downstream import. Passing `lake build` alone is not enough.
+
+## Validate before opening the pull request
+
+Run these commands from the repository root after fetching the target branch:
+
+```sh
+lake build
+./tools/validate-submission --base-ref origin/main --json-out .frontier/report.json
+```
+
+Open the pull request only if the second command exits with status zero and its
+JSON says `"accepted": true`. If it rejects the candidate, read its stable
+diagnostic code, revise the Lean source or claim yourself, and run the same
+command again. The receiver does not repair submissions.
+
+When opening the pull request, keep it to this one submission. Do not bundle
+documentation, workflow, policy, toolchain, prompt, test, or formatting edits.

tests/test_launcher_arms.py

@@ -0,0 +1,63 @@
+"""The launcher A/B is only interpretable if the arms differ in one place.
+
+Anything else that drifts between the two files becomes a second, unrecorded
+treatment. See PREREGISTRATION.md.
+"""
+
+import unittest
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[1]
+CONTROL = ROOT / "prompts" / "TRY-LEANFRONTIER.md"
+EXTENSION = ROOT / "prompts" / "TRY-LEANFRONTIER-EXTEND.md"
+
+# The paragraph the experiment varies, plus the title line that names the arm.
+CONTROL_BLOCK = """Start from current `main` in a fork or branch. Inspect the existing library and
+catalogue before choosing a subject: prefer an uncovered area or a genuine
+extension over a near duplicate."""
+
+EXTENSION_BLOCK = """Start from current `main` in a fork or branch. Read the catalogue and choose an
+accepted submission to build on. Import its module and prove something that
+depends on it: a generalization, a consequence, or a result that needs it as a
+lemma. A near duplicate is still a near duplicate and will be rejected."""
+
+
+class LauncherArms(unittest.TestCase):
+    def setUp(self) -> None:
+        self.control = CONTROL.read_text()
+        self.extension = EXTENSION.read_text()
+
+    def test_each_arm_carries_its_own_block(self) -> None:
+        self.assertIn(CONTROL_BLOCK, self.control)
+        self.assertIn(EXTENSION_BLOCK, self.extension)
+        self.assertNotIn(EXTENSION_BLOCK, self.control)
+        self.assertNotIn(CONTROL_BLOCK, self.extension)
+
+    def test_arms_are_otherwise_identical(self) -> None:
+        """Normalise away the varied block and the title, then compare words.
+
+        Comparison is word-level, not byte-level: the two blocks are different
+        lengths, so the sentence following them rewraps. Line breaks are not a
+        treatment. Any difference in the words themselves is.
+        """
+        control = self.control.replace(CONTROL_BLOCK, "<BLOCK>").replace(
+            "# Try LeanFrontier with an agent", "<TITLE>", 1)
+        extension = self.extension.replace(EXTENSION_BLOCK, "<BLOCK>").replace(
+            "# Try LeanFrontier with an agent (extension arm)", "<TITLE>", 1)
+        self.assertEqual(control.split(), extension.split())
+
+    def test_preregistration_names_both_arms(self) -> None:
+        prereg = (ROOT / "PREREGISTRATION.md").read_text()
+        self.assertIn("TRY-LEANFRONTIER.md", prereg)
+        self.assertIn("TRY-LEANFRONTIER-EXTEND.md", prereg)
+
+    def test_assignment_ledger_has_the_expected_columns(self) -> None:
+        rows = [l for l in (ROOT / "experiments" / "launcher-ab.csv")
+                .read_text().splitlines() if l and not l.startswith("#")]
+        self.assertEqual(rows[0], "submission_id,arm,assigned_utc")
+        for row in rows[1:]:
+            self.assertIn(row.split(",")[1], {"A", "B", "unassigned"})
+
+
+if __name__ == "__main__":
+    unittest.main()