WIP: import the Regts–Sevenster conjecture formalization

[Vilin97]

Imports the complete Regts–Sevenster formalization at upstream revision bb0a60543d48afac3f36938104b5c85c7c0396c7: all 837 source modules plus the LeanPool entry point remain. The statement-audit module retains 49 signature checks, 13 definition-body checks and three structure-constructor checks as compiled examples.

The port repairs tensor and coend constructions, Day convolution coherence, super-vector braiding, graded carriers, countable descent and skein assembly within the default compiler limits. All 52 oversized proof findings were resolved through mathematical helper lemmas and shared constructions; the recursive static and size audit reports zero errors across 838 files. Compiler warning and declaration cleanup is incorporated.

An earlier complete build passed all 4,348 jobs. The subsequent required module-system migration exposes data used by public interfaces while retaining private lemmas inside proposition-valued proof blocks. Existing remote changes and the full project scope are preserved.

Current checkpoint 3af8182b1 preserves concurrent source/main updates. The earlier three failing skein modules passed a 3,938-job targeted build. The next complete build passed those frontiers and reached two later failures in InterfaceCut and OrientExistence. Their proof-local decision instances and proposition-valued constructor arguments are now repaired; data and theorem statements are unchanged.

All 34 interactive simp sites now use the explicit rewrite sets suggested by the compiler, and two remaining long lines are wrapped. The new 18-file repair passes static checks and awaits compiled verification under the shared bounded-build queue.

All 51 affected public disjoint-union helper interfaces and their documentation remain available through shared declarations. All 838 project files and 65 statement/definition/constructor contract examples are retained. The recursive source, header and size audit is clean. Final warning-free aggregate build, declaration/style/index/metadata checks and compiled axiom/environment audits remain pending. The existing independent review passes faithfulness, novelty, significance and sources at its earlier checkpoint; its advisory quality findings and an updated-head review remain outstanding. No gates, waivers or proof budgets changed.

Part of the requested 42-project import batch. The existing ready-for-review state is preserved. Do not merge.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Changes requested by automated review

Reviewed exact head a30d864c6e388d9111cf5a85c57b4881b3dfab52. The exact-head Regts–Sevenster build emits a large warning set and fails the repository zero-warning gate. The imported closure still has deprecated API/style warnings, and the PR reports 79 declaration-audit issues and 52 proofs needing decomposition. Finish the warning and maintainability repairs and full quality/trust validation before merge.

[Vilin97]

/review

[Vilin97]

Maintenance update at ff335a09f701777788e40039160edb3cd1616c98.

The substantive duplicated block in DisjUnionProduct.lean is now removed: 912 lines, comprising 51 unused public copies of helpers already implemented in DisjUnionFactor/A.lean (12) and B.lean (39). Two independent source audits confirmed identical complete declarations modulo comments, whitespace, and private visibility, and found no in-project consumers outside the copied block and the canonical Factor implementation. The removed block registered no instances or global automation attributes.

The four remaining Product declarations, including EdgeSubset.throughValueC_eq_mixedValue and both boundary-label lemmas used by ClosedIdentify/EdgeTerm, remain byte-for-byte unchanged. The canonical Factor import and the file's remaining source are unchanged. Factor/A's active importer edits were not touched. The earlier dead-local-proof and unused-walk-premise cleanup is included in this head.

The changed-file header, forbidden-construct, file/proof-size, whitespace, and generated-index checks passed. This is source/static validation only: fresh full compiler, linter, and trust checks remain pending. Smaller repeated helpers elsewhere remain advisory maintenance debt; this resolves the identified Product block, not every duplication in the project.

[Vilin97]

Reviewed the 29-file incoming delta ff335a09f701777788e40039160edb3cd1616c98 → 7b5cfd2d9c91395e9e820339752e062ca18dfad7; the earlier mathematical source review carries forward. Fresh full CI is still required.

The canonical disjoint-union factorization now exports its existing 51 shared helpers with documentation. Their mathematical contracts and computational maps are preserved, and the 912-line duplicate block stays removed. The final colouring-sum identity is unchanged. Other changes expose or rename existing implementation helpers, supply explicit proof arguments and local classical decidability, and generalize four permutation lemmas from Fintype to Finite by constructing the enumeration inside the proof. These preserve the intended result and do not add assumptions to its endpoint.

I read the complete remaining 27-file diff; a second reviewer independently checked both factorization modules, including all 51 helper bodies. The pinned generated-index check and delta whitespace check pass. No additional compilation or full-project acceptance is claimed for this incoming head.

[Vilin97]

Reviewed all 13 files changed from 7b5cfd2d9c91395e9e820339752e062ca18dfad7 through 8506caa80f1215829c61322768b0153ee3fc927b. The changes repair sorted-list getter API calls, supply local classical decidability, and wrap proof arguments for module elaboration. The renamed transition_decide_lt_flip retains its original type and proof, with both consumers updated; the independent CutMatching.decide_lt_flip remains present. The theorem contracts, defining computations, project inventory, registry and index are preserved.

This is source-review carry-forward only. The full port still needs a successful complete build, linters and environment/quality audits; no new local compiler result is claimed, and this review does not authorize merging before those checks pass.

[Vilin97]

Reviewed the new project-source delta from 8506caa through 44adb23: three theorem-local elaboration fixes in ColourGlue, DisjUnionProduct, and GlueChord. The added Classical scopes and explicit by classical; exact Finset.mem_filter proof retain the existing theorem statements and computational definitions. No new mathematical assumption or weakened conclusion appears in this delta.

The prior substantive source review carries forward. Full project compilation, Lean linting, and compiled environment/axiom validation are still pending; this source-only follow-up does not establish merge readiness.

[Vilin97]

Changes requested by automated review

Reviewed 89b80c1931a8d41ef0efe4c552d52f6d0ac068a3. The complete graph-parameter characterization remains significant and the shared disjoint-union/skein refactor is useful, but the imported closure still does not build.

The source-identical build fails at LeanPool/RegtsSevenster/RS/Novel/Skein/LedgerRecursion.lean:521: relabel_openCircuitCount proves equality of the open-circuit terms, while the goal also contains the cut-matching unionCount for stepIdent 0. The current-head main merge leaves this project source byte-identical. Prove and apply the missing zero/interface-count identity (or otherwise complete the existing goal), retaining the actual ledger invariant and public characterization statements. Then rebuild the full imported closure and pass its linter, quality and axiom gates. The cardinality/graph predicates must not be weakened to bypass this endpoint dependency.

[Vilin97]

{
"summary": "Focused incoming-source review at 89b80c1, compared with the last substantive reviewed head 44adb23. I read the full 79-file delta: 62 files change only comments/whitespace; the 17 executable deltas finalize 34 simp queries with explicit rewrite lists, add two theorem-local classical scopes, and place the same orientation proofs directly in their record fields. The disjoint-union and fragment-equivalence data, orientation isOut computation, and snake-equation constructions retain their contracts.",
"assessment": {
"scope": "incoming proof maintenance only",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "These bounded changes preserve mathematical statements and constructed data; they do not settle the existing whole-project acceptance requirements."
},
"verdict": "approve",
"findings": [],
"validation": {
"source": "All 838 project files retained, 759 blobs unchanged. All 1,525 declaration headers in changed files are unchanged; no declaration or import changes. Raw and parsed project card, umbrella, and own root-index entries are identical. Full context review covers five definitions with changes confined to proof fields; an independent peer also read the entire StdRigid module and both snake proofs.",
"compiled": "No new build, linter run, profile, or compiled trust audit was performed for this follow-up. No fresh exact-head compiler result is claimed.",
"remaining": "This approves only the incoming source delta. The previous larger quality assessment and required warning-free aggregate build, declaration/style/index/metadata gates, compiled axiom/environment audits, and required CI remain unresolved. The author requests that this PR remain unmerged; this review preserves that disposition."
}
}

[Vilin97]

Focused source repair at 5051613f4d920cee14379c2107df287286f500ed; the author's do-not-merge hold and outstanding project review/validation conditions remain.

The preceding Build pool failure left a relabeled empty-carrier count in ledger_glueData's zero case. The repair supplies proof-local IsEmpty instances for both actual used-label carriers and applies the existing generic DirMatching.unionCount_of_isEmpty; the unchanged relabel-invariance theorem closes the original equation. The successor recursion and construction data are untouched. StdRigid removes exactly the 19 simp arguments identified as unused by that run, preserving the four existing snake-proof rule sets otherwise.

All 51 existing declaration headers, all 838 project files, the registry, root index and compiler configuration are preserved. The four scoped source checks and whitespace check pass. Independent peers read the complete repair and the final two proof-local let declarations.

The bounded local validation attempt stopped at cache certification: 12 of 430 native source hashes differed from their saved traces. No artifact hashing, cache copying or project-module compilation followed. There is no local project-compilation pass to report, and no broader rebuild or retry was started. Fresh current-head compilation, full lint/style/quality/trust checks and the remaining substantive review conditions are still required. No gate, waiver, option or CI queue was changed.

[Vilin97]

{
"reviewed_head": "c95b922e42dff1ddf0f2869b627c2217cf52e5f4",
"verdict": "needs_discussion",
"scope": "Focused follow-up on the remaining LedgerRecursion base-case compiler error; prior substantive review and leave-unmerged hold remain.",
"changes": [
"Moved the existing ledgerOf_isEmpty lemma, including its statement and proof, verbatim before ledger_glueData.",
"The zero case now simplifies both stage ledgers with that generic empty-interface lemma, then uses the original relabel_openCircuitCount theorem. All existing endpoint statements, successor-case proof, recursion data and other project source remain unchanged."
],
"evidence": {
"ci_head": "5051613f4d920cee14379c2107df287286f500ed",
"ci_job": "https://github.com/Vilin97/lean-pool/actions/runs/36231707776/job/108376008693",
"ci_result": "One remaining compiler error: simplification left the relabelled unionCount term in the zero case. This job reported no Lean warning headers.",
"source": "Two independent source reviews passed; the helper has no dependency on the recursion theorem and its complete existing type/proof are unchanged.",
"static": "Existing header, forbidden-text, file-size, proof-size and diff checks pass for the edited file. All 838 project Lean files including the umbrella remain; the other source files, registry, root index and configuration are unchanged."
},
"limitations": [
"No local module compile or full-project acceptance is claimed. The earlier native-cache check found 12 stale source hashes and stopped before project compilation; the build scope was not expanded.",
"Fresh CI on this commit is required. The PR body and its leave-unmerged hold remain unchanged."
],
"findings": []
}

[Vilin97]

{
"reviewed_head": "d4e06ca7ac806e97ab65cd89cfbda214c534e2fc",
"verdict": "needs_discussion",
"scope": "Focused follow-up on the new EdgeTerm relabeling proof failure; prior substantive review and leave-unmerged hold remain.",
"changes": [
"Added one proof-local classical tactic to RS.EdgeSubset.relabel_edgeSum. Both nested if_congr applications can now obtain the proposition deciders already used by edgeSum.",
"The full theorem statement, relabel maps, coloring sums, sign formulas, and all remaining proof steps are byte-identical. No theorem assumption or public computational interface changed."
],
"evidence": {
"ci_head": "c95b922e42dff1ddf0f2869b627c2217cf52e5f4",
"ci_job": "https://github.com/Vilin97/lean-pool/actions/runs/36233559469/job/108381163526",
"ci_result": "LedgerRecursion, including the previous empty-ledger repair, compiled in 2.5 seconds. The build then reported two errors in EdgeTerm: missing Decidable for genEvenBoundaryMatch and a subsequent no-goals diagnostic. This job emitted zero Lean compiler warning headers.",
"source": "Independent source peer passed after checking the full proof, boundary predicates, both callers, and if_congr at Mathlib revision 5ed2965256430c3649e86755f9576b54eca72435, Mathlib/Basic/Logic/Basic.lean:1009.",
"static": "The existing header, forbidden-text, file-size and proof-size checks pass for the edited file, as does git diff --check. All 838 project Lean files including the umbrella remain; the other 837 source files, complete registry, root index, compiler configuration and gates are unchanged."
},
"limitations": [
"No local compiler validation or full-project acceptance is claimed. The prior native-cache check found 12 stale source hashes; no cache or build expansion was performed.",
"The second no-goals diagnostic is treated as a likely cascade, not independently proved fixed. Fresh CI on this commit must establish the repair and remaining project readiness.",
"The PR body, draft state and leave-unmerged hold remain unchanged."
],
"findings": []
}