Research-Stack/0-Core-Formalism/lean/Semantics/Semantics/Physics
Brandon Schneider 7d2180f8e7 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
..
AdjacentCoprimeClassification.lean chore: QC cleanup — create Q16Utils, remove dead code, consolidate proofs 2026-05-13 22:18:13 -05:00
BindPhysics.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
Boundary.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
ClusterBHAnchors.lean chore: QC cleanup — create Q16Utils, remove dead code, consolidate proofs 2026-05-13 22:18:13 -05:00
Conservation.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
DESIInvariant.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
DESIModelProjection.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
Examples.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
H0ValveTest.lean chore: QC cleanup — create Q16Utils, remove dead code, consolidate proofs 2026-05-13 22:18:13 -05:00
Interaction.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
NBody.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
ParticleDomain.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
Projection.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
Q16Utils.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
QCLEnergy.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
StringStarConstants.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
SuperpositionalBoundaryLayers.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
Tests.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
UniversalBridge.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00
ValveTestSuite.lean feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 2026-05-14 00:04:08 -05:00