mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00

Brandon Schneider 5ee3b59680 feat: eigensolid convergence proof + QC flagging tool + full pass/fail review

Resolves the convergence_to_fixed_point failure by proving the correct
eigensolid statement: stepExact stabilizes all value components (N_7,
N_8, N_11) in one application. The original theorem was mathematically
false (iteration counter is free-running).

QC cleanup sweep across Physics/ (20 files):
- 3 remaining LOW items fixed: h00/h01 factoring, rD->rd, rdDr1/rdDr2 x100
- 6 of 7 sorry theorems proved; 1 explicitly FAILED (convergence)
- Unused imports removed, naming violations fixed, #eval witnesses added
- 210 -> 144 issues remaining (all WARNING/INFO, zero ERROR)

New tooling:
- scripts/qc-flag/lean_qc_flagger.py implemements 5-point inspection protocol
- Outputs structured JSON + Markdown pass/fail reports

DAG receipts at shared-data/data/stack_solidification/qc_*_dag_2026-05-13.md

2026-05-14 00:04:08 -05:00

1.4 KiB

Raw Blame History

QC Flagger — AGENTS.md

Purpose

Automated code quality inspection for Lean files, implementing the Lean Expert Agent's 5-point inspection protocol.

Usage

# Run on a single file
python3 scripts/qc-flag/lean_qc_flagger.py path/to/file.lean

# Run on a directory (recursive)
python3 scripts/qc-flag/lean_qc_flagger.py path/to/dir/

# Save reports
python3 scripts/qc-flag/lean_qc_flagger.py path/to/file.lean --json report.json --markdown report.md

# Shell wrapper (saves dated reports to scripts/qc-flag/reports/)
bash scripts/qc-flag/run_qc_flag.sh path/to/file.lean
bash scripts/qc-flag/run_qc_flag.sh path/to/dir/ --verbose

Protocol Coverage

#	Check	Implementation
1	Structural Health	theorem/def/eval/sorry counts, empty theorems, tautologies, unused imports, `set_option` suppressions
2	Naming Conventions	PascalCase files/types, camelCase functions/theorems, banned prefixes/suffixes
3	Q16_16 Compliance	Float usage in hot-path code
4	Proof Quality	defs without companion theorems, `.get!` without `.isSome`, native_decide coverage
5	Dependency Analysis	Unused imports, circular and transitive circular dependencies

Output

JSON: structured per-file results with issue details
Markdown: human-readable report with summary table and issue tables
Exit code: 0 if all files pass, 1 if any file has ERROR-severity issues

1.4 KiB Raw Blame History