[P1 refactor] Simplify architecture and retire technical debt; treat build speed as a supporting metric

[phasetr]

Objective and priority

Plan and execute a bounded refactoring programme whose primary outcomes are simpler code, coherent abstractions, and retired technical debt. Build-time improvement is supporting evidence and a regression guard, not the reason to accept a design.

Baseline for the initial inventory: main at f23fa1e732d6985a59d305c85e018f06d62b2f88 (2026-08-01 JST). Every child must remeasure at its own start.

Decision order

1. Preserve the mathematical architecture: weakest useful SimpleGraph core, Ambient transport, then concrete lattice capstones.
2. Remove responsibility mixing, dependency inversion, repeated proof/API structure, or incoherent file boundaries only when current consumers demonstrate the replacement boundary.
3. Preserve public/book-facing names unless a citation and consumer audit justifies removal; a one-line semantic alias may be preferable to deletion.
4. Measure import closure, elaboration time, clean/incremental build cost, and RSS only to compare otherwise sound designs and prevent regressions.

Child workstreams

The linked subissues are the complete initial programme. Each begins with an audit gate. A failed gate closes that child as not planned with measurements; it must not turn into speculative infrastructure.

• [P0 refactor] Replace correlationAlongExhaustion case-split boilerplate with first-order family equations #4837 (P0) — correlationAlongExhaustion first-order family equations and bounded A1/A2 migration — completed
• [P1 refactor/audit] Separate finite Gibbs-kernel responsibilities only behind a consumer-proven boundary #4831 — finite Gibbs-kernel responsibility audit and bounded pilot — declined (not planned)
• [P1 refactor/audit] Restore dependency direction around AmbientLattice/Defs/Core #4832 — AmbientLattice/Defs/Core dependency-direction repair — completed
• [P1 architecture] Define and enforce the import-DAG contract before structural pilots #4833 — import-DAG architecture contract — completed
• [P1 refactor/audit] Audit Lee-Yang/Ascoli structure composition and run at most one bounded pilot #4834 — Lee--Yang/Ascoli structure-composition audit and pilot — declined (not planned)
• [P1 refactor/audit] Consolidate derivative abstractions only after a current contract matrix #4835 — derivative abstraction and provider-contract audit — declined (not planned)
• [P2 refactor/audit] Clean up large files and serial micro-modules along concept boundaries #4836 — concept-coherent large-file / serial micro-module cleanup — declined (not planned)

All seven first-wave children are closed (3 completed: #4832, #4833, #4837; 4 declined not planned after
audit gate: #4831, #4834, #4835, #4836).

Common acceptance criteria

• Each child records current declarations, responsibilities, consumers, citations, and import edges before proposing edits.
• Each implementation is a separately reviewable pilot with preserved public entry points and a rollback boundary.
• New records/typeclasses/helpers require demonstrated current consumers; no anticipated-reuse abstraction.
• Targeted module, downstream importer, root build, lake exe GKSTest, repository audit gates, representative #print axioms, and documentation/citation checks pass with zero warnings.
• Any deletion runs escaped/normalised TeX citation checks in addition to ordinary source search.
• Before/after import closure and build measurements are recorded, but no child is accepted solely for speed or line-count reduction.
• Public API break, new axiom/placeholder, warning, build failure, cold-build regression over 5%, RSS regression over 10%, or increased regenerated .olean closure blocks merge.
• The parent closes only after every child is completed or explicitly declined with evidence.

Dependencies and sequencing

• Execute the P0 exhaustion-family-equation child first. Its A1 must precede A2, and both are serialized against other high-fanout ancestor edits and canonical build measurement.
• The import-DAG contract child defines the architectural checks used by implementation pilots, but it does not authorize mechanical import rewriting.
• After P0, record the import-DAG contract, then evaluate finite Gibbs-kernel and AmbientLattice/Defs/Core ownership before derivative-family consolidation.
• Lee--Yang/Ascoli may audit in parallel with Gibbs/Core after the import contract; its implementation pilot must not overlap high-fanout edits.
• Large-file cleanup consumes the other audits' concept boundaries; it must not invent boundaries from file length.
• Changes to near-universal ancestors and canonical build measurements must be serialized.

Non-goals

• Repository-wide mechanical import rewrites, mass file splitting, or line-count quotas.
• Collapsing abstract Ambient results into concrete Z^d specializations.
• Merging finite- and infinite-volume results with different types or hypotheses.
• Deleting compatibility/book-facing wrappers from reference-count evidence alone.
• Reviving the archived [refactor] Refactoring phase tracker — build-speed + simplification #4506 speed campaign or deleted #4786/#4793/#4794 trackers as authority.
• Treating closed [P1 refactor] Track the duplication-cluster consolidation programme (clusters A-D) and its TeX detection defect #4823 as open work; reusable findings must be cited explicitly by a child.

Historical context

docs/plans/4506-refactoring-replan.md is an archived execution record, not current authorization. #4823 is closed not planned after bounded duplication work. GitHub #4786, #4793, and #4794 are deleted; their local mirrors are historical snapshots only.

Second-wave plan (2026-08-02)

The initial seven-child programme is resolved. A current-code re-audit authorized by the user identified five non-duplicate, bounded follow-ups. They inherit this parent’s decision order, common acceptance criteria, and fail-closed audit discipline.

• [P0 refactor] Restore the generic-to-Concrete ownership boundary around extremal configurations #4850 (P0) — restore the generic-to-Concrete ownership boundary around extremal configurations — completed (PR refactor: repoint GKSBoundaryCondition import boundary (#4850) #4856, merge commit ac942a45; AC2 ownership-violation edge tracked separately as [P0/P1 refactor] Restore generic ownership of gibbsExpectationBC_field_mono (MonotonicityBetaBoundaryCondition -> MagnetizationFieldMonotone) #4857)
• [P0 refactor] Re-home sum_spin at its Spin-level owner #4851 (P0) — re-home sum_spin at its Spin-level owner — completed (reduced scope) (PR refactor: retire duplicate Lebowitz.sum_spin declaration (#4851, reduced scope) #4859, merge commit 26132222; retired the duplicate Lebowitz.sum_spin declaration in favour of the general IsingModel.sum_spin. The original AC's full move — relocating sum_spin to Basic.lean and making FourfoldSite.lean transitively GibbsMeasure-independent — is parked as a Non-goals P2 candidate pending explicit user authorization: dev-design found it would force a full-library rebuild for a parallel-schedule-only import-closure benefit, since the downstream FourfoldSystem.lean needs GibbsMeasure regardless)
• [P1 refactor/audit] Unify edge- and vertex-avoidance proofs behind a consumer-proven forbidden-edge core #4852 (P1) — audit a forbidden-edge core shared by edge- and vertex-avoidance proofs — declined (not planned) (edge-avoidance route Gavoid has zero code-level consumers anywhere in the live tree, failing the issue's own ≥ 2-consumer gate; full matrix in the closing comment: [P1 refactor/audit] Unify edge- and vertex-avoidance proofs behind a consumer-proven forbidden-edge core #4852 (comment))
• [P1 refactor/audit] Extract the shared numeric core of spectral-gap certificates #4853 (P1) — audit/extract the shared numeric core of spectral-gap certificates — declined (not planned) (both current capstone consumers of the shared ratio algebra are on the open path, the cyclic/balanced route has zero external consumers after its former capstone was deleted in 109690bd/Post-axiom-free refactoring: build speedup + simplification/abstraction (investigation → execution) #4298 PR-B1, so the issue's own "one cyclic/balanced + one open" ≥ 2-consumer gate cannot be constructed; full matrix in the closing comment: [P1 refactor/audit] Extract the shared numeric core of spectral-gap certificates #4853 (comment). Related new finding tracked separately, not fixed here: tex/proof-guide.tex: 3 dangling citations to deleted layerCylinderSpectralDecay declarations (lines 7561, 7573, 7580) #4866, 3 dangling TeX citations to a declaration cluster deleted by the same 109690bd commit.)
• [P2 refactor/pilot] Canonicalize one identical-statement Patches group with compatibility aliases #4854 (P2) — canonicalize one identical-statement Patches group with compatibility aliases
• [P0/P1 refactor] Restore generic ownership of gibbsExpectationBC_field_mono (MonotonicityBetaBoundaryCondition -> MagnetizationFieldMonotone) #4857 (P0/P1) — restore generic ownership of gibbsExpectationBC_field_mono (MonotonicityBetaBoundaryCondition -> MagnetizationFieldMonotone); spun off from [P0 refactor] Restore the generic-to-Concrete ownership boundary around extremal configurations #4850's AC2 ownership audit (.self-local/reports/research-4850-audit-gate-l2-l4-edges.md row 21), linked as a native sub-issue on 2026-08-02 — completed (PR refactor: move gibbsExpectationBC_field_mono generic block to MonotonicityField (#4857) #4862, merge commit c3bfdc4072cb93ec48b6253b5fa5b640e2111246)

Second-wave progress: 5/6 resolved (#4850, #4851, #4852/#4853 declined not planned, #4857). GitHub sub_issues_summary = 12/13 across both waves.

Second-wave sequencing

1. Execute the ownership-correction children first ([P0 refactor] Restore the generic-to-Concrete ownership boundary around extremal configurations #4850, [P0 refactor] Re-home sum_spin at its Spin-level owner #4851 — both completed — then [P0/P1 refactor] Restore generic ownership of gibbsExpectationBC_field_mono (MonotonicityBetaBoundaryCondition -> MagnetizationFieldMonotone) #4857). They are direct responsibility corrections and must be serialized with other high-fanout ancestor edits.
2. After those ownership boundaries settle, [P1 refactor/audit] Unify edge- and vertex-avoidance proofs behind a consumer-proven forbidden-edge core #4852 and [P1 refactor/audit] Extract the shared numeric core of spectral-gap certificates #4853 may audit in parallel, but their implementation pilots must be separately reviewable and must not overlap canonical build measurement.
3. Execute [P2 refactor/pilot] Canonicalize one identical-statement Patches group with compatibility aliases #4854 last and alone because its normalized statement checks and docs/TeX synchronization are the primary safety boundary.
4. Do not reopen [P1 refactor/audit] Consolidate derivative abstractions only after a current contract matrix #4835’s repository-wide derivative-wrapper consolidation or [P2 refactor/audit] Clean up large files and serial micro-modules along concept boundaries #4836’s mechanical file-layout candidates without their recorded reopen conditions.
5. Close this parent only when every native sub-issue is completed or explicitly declined with evidence (13 as of 2026-08-02: 7 first-wave + 6 second-wave; the count grows if a child's own audit gate spawns a tracked follow-up, as [P0 refactor] Restore the generic-to-Concrete ownership boundary around extremal configurations #4850's AC2 spawned [P0/P1 refactor] Restore generic ownership of gibbsExpectationBC_field_mono (MonotonicityBetaBoundaryCondition -> MagnetizationFieldMonotone) #4857).

Build speed remains a supporting metric throughout this second wave: it can reject a coherent design on regression grounds or break a tie, but cannot create an abstraction boundary or justify deletion.