This repository is a self-contained, portable research workspace. Copying
the TECT folder to another computer (or git clone) and connecting cowork is
enough to continue all research exactly where it left off. Nothing about the
research state lives in the cowork app; it all lives in tracked files here.
One-line goal: folder copy + connect cowork +
doctor.py→ resume.
-
Install the interpreter and verification dependencies. Python >= 3.10, then, preferably in an external sibling venv such as
TECT.venv:pip install -r requirements.txt
The requirements include
sympyandpython-flint; the latter supplies outward-rounded Arb balls for fail-closed interval certificates. Install either a venv-localtectonicexecutable or a TeX distribution providingpdflatex. Proof-note PDF generation is part of the readiness gate, sodoctor.pyreports NOT READY when neither engine is available. -
Copy the WHOLE folder. The numerical codes in
codes/import constants fromarchive/legacy/scripts/; a partial copy of onlyclaims/will not run.doctor.pychecks this explicitly. -
Connect the collaborator to the
TECTfolder. The canonical session protocol isAGENTS.md.CLAUDE.mdis only a compatibility pointer for clients that discover that filename.
-
Readiness check — confirm the copy is intact and all ledgers are in sync:
python verification/scripts/doctor.py # prints READY / NOT READY + fixesIf it reports a stale generated surface, refresh every one in a single command (the commit watcher enforces the same gate before every commit):
python verification/scripts/regen_all.py # or: doctor.py --fix -
Session-entry prelude (
AGENTS.md§1, performed automatically): run the host-native UTC date command first, then readGOVERNANCE.md,CLAIMS.md, and the boundedmanagement/INDEX.md. Read the compact changelog and negative indexes, query the live task states, and open only ID-targeted portions of the large historical authorities. Emit[ENTRY-OK] <date> | claims: <n> | top priority: <gate>. -
Recover the main-proof continuity state when working on Pre-A or Sector A. This is a pointer-only resume layer and does not replace any existing proof method:
python verification/scripts/check_research_continuity.py
Read
governance/research-continuity.mdand the machine checkpoint instrategy/main-proof-program-v1.json. A failure returns the programme to Research PhaseP0-Rbefore new proof work. After watcher drain and push, use--strict-baselineto verify the clean offsite baseline; that strict mode is intentionally not part of the pre-commit release gate. -
Run the direction-control layer before selecting new work:
python verification/scripts/check_direction_control.py
This derives the active mainline, auxiliary/no-progress streaks, repeated blocker count, review budget, and required route decision from the append-only
strategy/direction-control-log.jsonl. A threshold returnsREVIEW_REQUIRED; it is not an automatic scientific stop. Append a review record with its evidence target, continuation/revisit conditions, and finite budget before continuing. The review may authorize bounded research, return to mainline, require redesign, or park/block the route. The layer never changes a claim tier, closes a scientific gate, or approves physical identity. Record a material route decision withcheck_direction_control.py --add --file <record.json>. -
Pick up the work — the live task ledger:
python verification/scripts/todo.py list --status in_progress python verification/scripts/todo.py list --status next python verification/scripts/todo.py list --status blocked
TODO.mdis the human-readable view;todo/todo.jsonis the source. Manage it withtodo.py add/start/done/block/set(never hand-editTODO.md).For a cross-claim proof route, search the generated evidence map without loading it in full:
rg -n "<claim-or-gate-id>" theory/proof-evidence-map.mdIt links accepted results, failed routes and reasons, current gates/tasks, proof explorations, lineages, and reproduction entrypoints. The linked source remains authoritative. For a precise prior route verdict:
python verification/scripts/exploration.py search --claim <ID>
-
Operator only — start the commit daemon (Windows PowerShell), so the AI's queued commits are recorded with the maintainer signature:
.\verification\scripts\commit_watcher.ps1 # leave running, or .\verification\scripts\commit_watcher.ps1 -Once # drain once per turn
The watcher (v1.2.0+) batch-drains: an accumulated queue is committed as ONE combined commit and empty-diff leftovers move to done/, so accumulation is safe. Draining per turn is still tidier (1:1 commit-to-message) but not required for correctness (
AGENTS.md§4).
python verification/scripts/release_check.py # must reach exit 0release_check runs the ledger/catalog/lineage/todo/exploration-integrity/
proof-evidence-map checks, the English-only and no-overclaim scans, and file hygiene. A session
may not end with it failing.
- The task ledger (
TODO.md/todo.json) carriesownerandstatusper task. Claim a task withtodo.py set T-0NN --owner <name> --status in_progress. - One substantive claim-card change per turn (
AGENTS.md§3); commit one logical change set at a time. This keeps parallel work mergeable. - Status/tier/gate transitions are operator-authorized — do the work, record
it as a dated ADVANCE in
claims/GATES.md, and recommend the flip; the operator confirms it. - All numerical claims ship a reproducible script + self-test asserts + JSON
under
claims/<ID>/runs/(AGENTS.md§3, §6). Anyone can re-run and verify.
| Path | Role |
|---|---|
AGENTS.md |
single binding session protocol |
CLAUDE.md |
compatibility pointer to AGENTS.md |
GOVERNANCE.md |
constitution: tiers, gates, registration rules |
management/INDEX.md |
bounded live task, gate, result, and reader dashboard |
governance/research-continuity.md |
binding pointer-only long-running research resume contract |
strategy/main-proof-program-v1.json |
machine phase, lane, stopped-loop, and next-action checkpoint |
CLAIMS.md / catalog/INDEX.md |
current generated ledgers (root CATALOG.md is frozen compatibility) |
ROADMAP.md |
long-form staged research narrative; use the management index for live priority |
theory/proof-evidence/INDEX.md |
compact proof-evidence entry and targeted lookup commands |
theory/proof-evidence-map.md / verification/proof-evidence-map.json |
complete compatibility maps for deep or issued-verifier lookups |
explorations/log.jsonl |
canonical append-only proof-route decisions; add/search/verify with exploration.py |
TODO.md / todo/todo.json |
live task ledger (this resume system) |
claims/<ID>/ |
per-claim card + status.json + notes/ + runs/ + lineage |
claims/GATES-INDEX.md / claims/GATES.md |
compact current references / complete gate and hypothesis authority |
codes/ |
numerical codes by domain (import archive/legacy/scripts/) |
verification/scripts/ |
doctor.py, lint_claims.py, build_*, todo.py, release_check.py, commit_watcher.ps1 |
governance/ |
binding policies (incl. CODE-DISCIPLINE.md) |
negative-results/ |
failed branches / retractions (trust assets) |
reviews/ |
external adversarial-review archive |
internal/ |
gitignored operator-side scratch (commit queue) — not portable via git, carried only by folder copy |
Note:
internal/is gitignored, so agit clonedoes not carry the commit queue (that is fine — it is operator-side scratch). A full folder copy carries everything.