QECLean CLAUDE.md

CLAUDE.md — agent orientation

This is a Lean 4 / mathlib formalization of the stabilizer formalism for quantum error correction. The active math is in QEC/. Build with lake build.

Two-repo layout

This repo is the library only — polished, sorry-free Lean on main (mathlib/cslib model). The research program behind it lives in the sibling repo qec-lab (shared pre-split git history; tag archive/pre-split-20260718 marks the split point): the BB distance lab (experiments/bb_lab/), the formalization pipeline (pipeline/, catalog/, the four pipeline agent specs), the narrative docs, and the dashboard. Convention: qec-lab tooling expects this repo checked out as a sibling directory (env QECLEAN_ROOT, default ../QECLean). WIP formalization branches live here (in worktrees), can be backed up to the qec-lab remote (git push lab <branch> works thanks to shared ancestry), and merge to main only when sorry-free. Read qec-lab's CLAUDE.md before any pipeline or research work.

Where to look for what

CLAUDE.md is the small must-read on every invocation. It carries codebase-wide orientation, naming/style policy, layering rules, and build/MCP workflow. Volatile or topic-scoped knowledge lives elsewhere:

• qec-lab: docs/lean-patterns.md — tactical patterns by code shape (CSS distance, non-CSS distance, parametric families, mechanical fixes). Reach for this when your current code matches one of its sections; add new patterns there when they're code-shape-specific rather than codebase-wide.
• qec-lab: docs/mathlib-version-quirks.md — mathlib API drift (deprecations, renames, signature changes), grouped by version. Add new entries there when you work around a mathlib version-specific quirk.
• blueprint/README.md — the LeanArchitect blueprint: what is generated vs. hand-written, how to add a node, how to inspect one with #show_blueprint. Read before editing QECBlueprint.lean or blueprint/. See also the "Blueprint" section below.
• QECWidgets/README.md — the ProofWidgets-based infoview widgets (#pauli_strip, #toric_chain, #check_matrix, and the expression presenters): what each renders, how meta-level reduction drives them, and the linter rules for adding widget files. Read before editing QECWidgets/.
• QEC/Stabilizer/Codes/BivariateBicycle/README.md — orientation for the BB family (gross d=12 proof spine, instance dirs, hypothesis-discharge map, engine-vs-analytic status, generated-file manifest). Read before any BB edit. Generated files carry GENERATED FILE — DO NOT HAND-EDIT banners: change the generator (see qec-lab's experiments/bb_lab/GENERATORS.md) and regenerate, landing both repos' changes together — never hand-edit the emitted Lean.