Repository navigation
Conversation
There was a problem hiding this comment.
Draft intake review at 4fc0ab7e543f68ab62c471f2780b05e3bd8f2974.
The exported statements have the advertised finite loopless multigraph scope. LooplessMultigraph assigns an unordered endpoint pair to each independent edge identity, so parallel edges remain distinct. Proper full colorings assign every edge a color in Fin k; ChromaticIndex is the least such k. The density ranges over odd vertex sets of size at least three and counts internal edges with multiplicity. GeneralHighIndexElementary concludes the stated density equality, and the public bound follows without an additional graph or coloring hypothesis. These are statement and definition checks, not a completed review of the entire port.
The complete public inventory is 729 Lean files and one project card, all additions within the content allowlist. Final acceptance remains pending: the final-head aggregate build and warning/linters/trust checks, preservation of the upstream theorem contracts through the final cleanup, the independent project reviews, and normal protected integration. The earlier build, axiom-audit, contract and timing checkpoints in the description are historical author reports and do not establish those final-head results. Profiling remains advisory.
Keep this draft while its published validation work finishes. No queue or auto-merge action is appropriate at this stage.
Additional maintainability feedback at the same head:
In AbsentOwnerReplacement.lean, helperHNcard363Conditions carries the hierarchy, counterexample, prefix constructions and NineN hypotheses into a bound on the union of two optional colors. Its proof uses only the two optional values and generic finite-set/list cardinality bounds, but the caller must supply the larger proof state. This couples a generic fact to unrelated hierarchy details and makes later changes require unnecessary contract and caller edits. Please express the two-Option cardinality bound as a generic lemma and instantiate it here; check the neighboring suffix-membership helper for the same unnecessary context coupling. This is advisory maintainability feedback.
All 730 published bodies and the complete 729-module import graph are now available and checked for identity, coverage and acyclicity. Full proof-port, semantic and current-head validation acceptance remains pending.
|
/review Please review current head |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] No blocking defect was established in the latest update, but this partial review does not establish that the whole import is safe to merge. SummaryThe PR imports the Goldberg–Seymour bound for finite loopless multigraphs. The latest changes share component-color proofs and extract walk-region facts into a general API.
Reviews (37) · Last reviewed commit: "refactor(GoldbergSeymour): share compone..." · Reviewed by Greptile |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed published head f1f8c0a82cccbfb8a5ebb4a64bbd14d80c2a1ed3. The PR is now ready for review, so the earlier draft-readiness note is superseded.
The mathematical scope and provenance review is favorable: the finite loopless multigraph model retains independent edge identities and multiplicity, and the final colouring statement uses the full edge domain. I traced the port against the licensed upstream dependency closure, including the explicit-context and hierarchy-predicate reformulations; I found no added mathematical premise that weakens the claimed theorem.
I also reviewed the complete latest two-file delta. The two new Preamble lemmas prove the natural-number bounds already used by the Fin indices. Replacing the arithmetic proof witnesses preserves the index values and assumptions; the other edits rename unused binders to _ while retaining their types. This does not resolve the separate maintainability suggestion in the earlier review, which remains advisory.
This is a source review, with current-head compilation, trust/quality checks and the configured independent review still to qualify. Author-reported local audits and timing results have not been counted as independent validation. Integration must also wait for the applicable current-main checks and normal protected queue.
|
/review Please run the configured project-rubric review for current published head |
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 25,187,305 maxHeartbeats units across 815 valid files (347,177 added LOC). Sum of Count-heartbeats wall-clock total: 4098.20 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.GoldbergSeymour.AbsentOwnerReplacement |
28.00 s |
LeanPool.GoldbergSeymour.SplitSwapPreparation |
27.00 s |
LeanPool.GoldbergSeymour.HierarchySituationThreeClaimJMinusOneEmpty |
26.00 s |
LeanPool.GoldbergSeymour.HierarchySituationThreeClaimJMinusOneNonempty |
25.00 s |
LeanPool.GoldbergSeymour.ScheideOrderNineRebasingPreparation |
23.00 s |
LeanPool.GoldbergSeymour.ExtensionRulesTerminalEarlierAppearance |
20.00 s |
LeanPool.GoldbergSeymour.HierarchySituationTwoSubcaseTwoOneNonexceptional |
20.00 s |
LeanPool.GoldbergSeymour.HierarchySituationTwoSubcaseOneOneNonexceptional |
20.00 s |
LeanPool.GoldbergSeymour.HierarchySituationTwoSubcaseOneOneStoredException |
19.00 s |
LeanPool.GoldbergSeymour.EligibleIndexBoundPreparation |
17.00 s |
LeanPool.GoldbergSeymour.HierarchySituationThreeDisjointThetaUnstoredOutsideImpossible |
17.00 s |
LeanPool.GoldbergSeymour.OneDividerRefresh |
17.00 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 816 files; the per-file table shows only the 416 hottest by heartbeats. The full table and raw
lean --profileoutput for every file are in the run's step summary andproof-profileartifact.
Advisory only — never blocks merge.
|
/review Please review exact current head The hierarchy-coupled utility finding and neighboring cases are repaired: the two-Option cardinality and final-pair membership facts are generic; the first-missing-position fact is generic; duplicate first-position bounds are shared, with an unnecessary finite-vertex assumption removed. The module shrank from 2,877 to 2,193 lines. Controlled focused runs measured 18.310→16.324 s and 2,293,184→2,013,008 KiB peak RSS. The new Mathlib graph interface converts actual vertex/edge sets to types, proves incidence correspondence, preserves parallel-edge identities and isolated vertices, and exposes the bound without requiring finite ambient types. All 730 modules pass the full public aggregate build without warnings, all 15 native linters, compiler diagnostic export (zero), style, static quality/index/card checks, both complete trust audits, and all 506 original upstream theorem contracts. These local observations are tied to the current source hashes. The exact-head clean timing rerun and CI are pending; independent review and protected integration remain separate requirements. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed published head 95be6b219559f04be188eba96aeb4a49bf033052.
The new generic two-Option cardinality, final-two-position membership and first-missing-position lemmas address the context-coupling advice in my earlier review. Their callers now supply the facts those lemmas use. The public absent-owner replacement theorem remains unchanged; removing an unused finite-vertex assumption generalizes a private helper.
The Mathlib graph adapter uses the graph’s actual vertex and edge sets, preserving isolated active vertices and distinct parallel-edge identities. Its endpoint/link and incidence correspondence proofs support applying ThmGS to that conversion. The exported bound is stated for the converted graph’s invariants. I also checked the facade, regenerated aggregate and card changes against the complete current source inventory and dependency graph. My source verdict is favorable.
Current-head compilation, trust/quality checks and the configured independent review remain separate requirements. The existing /review request already names this head; older-head checks and author-reported local measurements have not been credited as independent validation. Protected integration still requires the applicable current-main checks and the normal native queue.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Conclusion: approve the source/content at 95be6b219559f04be188eba96aeb4a49bf033052. This is the importing agent’s separate thorough review; it does not replace the configured independent GPT rubric review or authorize integration before that review completes.
The review used the complete local source rather than a truncated patch: all730 files are covered by module/declaration inventories, endpoint signatures, the complete dependency graph, and bounded implementation slices. Foundational graph/coloring/degree/density definitions and176 original data-definition contracts received a separate semantic comparison. All506 original theorem contracts are kernel-proved using the ported declarations. The new graph bridge and the final generic-helper changes were inspected in full.
- Faithfulness:
goldbergSeymourquantifies over arbitrary finite vertex and edge types and every loopless endpoint map. Distinct edge identities retain parallel edges; proper full colorings cover the complete edge domain. Density uses rational division over odd sets of size at least three, with zero included for the empty eligible family.GeneralHighIndexElementarystates the advertised high-index equality. Empty graphs and two-vertex parallel-edge graphs fall within the stated regime. The headline has no undisclosed hierarchy, algorithmic or external-result hypothesis. - Mathlib interface:
graphEndpointPair_eq_iffcharacterizes actual links, andofGraph_incidentproves incidence correspondence. Conversion uses the actual vertex/edge subtypes, including isolated active vertices, so it preserves multiplicity and does not require finite ambient types. The facade exports the bridge and the bound uses the converted graph’s explicitly defined invariants. - Novelty and fit: no existing headline was found in the searched pool cards/source/history/PRs, pinned Mathlib/Tau Ceti combinatorics, or refreshed public code searches. Mathlib’s existing multigraph model motivated the bridge; it is not an existing Goldberg–Seymour proof. Search absence is bounded evidence, not an exhaustive theorem-of-absence. This is completed research-level graph theory with substantial reusable coloring, Kempe, critical-subgraph and Tashkinov infrastructure.
- Sources/license/provenance: the mathematical statement matches Chen–Jing–Zang, arXiv1901.10316v2. The author’s page dates completion October12,2026. Licensed commit88d98c1 explicitly covers Tablet/ under Apache-2.0 and excludes paper/, which is not imported. Wesley Pegden/Trellis attribution and AI provenance are explicit; the new adapter credits Lean Pool contributors.
- Engineering and trust: the hierarchy-coupled Option/cardinality/suffix/first-position helpers are now general facts, and the duplicate first-position bound is shared without an unnecessary finite-vertex assumption.105 repeated arithmetic type witnesses use proved shared bounds. Source budget overrides, diagnostic searches and unstable generated proof references were removed. The full730-module aggregate, all15 native linters, compiler diagnostics (zero), style/index/card/quality checks, both complete trust audits, and506 original contracts pass on matching source hashes. The fixed pool root and all gate/configuration files are unchanged. CI’s Build pool and protected Build project also pass on this head.
Measured cost / quality: 3 of5. The final clean command was LEAN_NUM_THREADS=2 lake build LeanPool.GoldbergSeymour, with private project artifacts removed and exact pinned dependencies warm. Baseline→final:1240.430→1782.543s wall,2019.936→2605.654s child user CPU,282.813→895.614s system CPU,2165628→3407352KiB peak RSS. Whole-project speedup is not established. The shared host was busier;706 modules with identical source and complete project dependency closures had a median1.435 wall-time ratio against the preceding clean checkpoint. That control is descriptive, not a normalized speedup estimate. Focused repairs have measured gains, including39.704→16.457s and6850648→1399832KiB for the shared-index-witness change.
The426,989-line footprint (compatibility baseline224,728) and explicit generated contract plumbing remain real maintenance costs. The interfaces, default-limit proofs, source-strength regression checks and isolated Mathlib adapter make the present source maintainable at the pool’s competent-project bar; this is not a claim of Mathlib-level polish. No further concrete source-blocking finding remains after the repairs. Greptile’s current advisory review reports incomplete full-source coverage, so its green check is not counted as full approval. Independent GPT review and every normal protected native-queue requirement still have to complete.
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
Both card headlines match the Lean; exact-head CI remains pending, and local recompilation was blocked by a Mathlib-fetch HTTP 403. |
| Novelty | ✅ pass |
No duplicate of either headline was identified in the inspected Mathlib, Tau Ceti, or pool declarations. |
| Significance | ✅ pass |
The full Goldberg–Seymour theorem and its supporting critical-subgraph, Kempe and Tashkinov theory merit inclusion despite the substantial source footprint. |
| Sources | ✅ pass |
Both headline results match Chen–Jing–Zang, Theorem 1.1 and §2.2, and the pinned Trellis formalization is explicitly credited. |
| Code quality (advisory) | 🤔 discuss |
Two recurring infrastructure proof families warrant consolidation; semantic inspection was targeted, and exact-head assembly/lint and minimal-file verification remain pending. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Finite vertex and edge types and looplessness; the equality theorem additionally assumes MaximumDegree G + 2 ≤ ChromaticIndex G, as disclosed. Criticality, removal of isolated vertices and induction certificates are established internally. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | graph theory |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: The Lean gives the stated bound for arbitrary finite loopless multigraphs and equality with the density ceiling under the stated high-index condition, using independent edge identities and the claimed coloring and density definitions.
GoldbergSeymour.goldbergSeymour establishes ChromaticIndex G ≤ max (MaximumDegree G + 1) (DensityCeil G) for finite loopless multigraphs, with high-index density equality and substantial supporting theory for this named research result (paper).
Novelty findings (1)
- prompt-injection — PR-wide
The description and discussion repeatedly assert earlier review passes and approval, risking substitution of prior verdicts for independent declaration comparison; these assertions were excluded from this novelty assessment.
Evidence: The description states ‘Its configured review passed the four mathematical/source dimensions’; discussion comment 6699440899 states ‘The exact-head configured review2379 passes faithfulness, novelty, significance and sources.’ Comment 6710897958 asserts ‘APPROVE for source inclusion’.
Significance findings (1)
- prompt-injection — PR-wide
Contributor-supplied discussion asserts previous rubric passes and approval, creating a risk of anchoring this independent assessment; those assertions were disregarded.
Evidence: Comment 6699440899 states: ‘The exact-head configured review2379 passes faithfulness, novelty, significance and sources.’ Similar prior-pass claims occur in comments 6701508672, 6703249492, 6705695531, 6707145960, 6727481707 and 6733819011 and the PR body. Comment 6710897958 states: ‘APPROVE for source inclusion (engineering 3/5).’
Code quality findings (2)
- duplicate-proof —
LeanPool/GoldbergSeymour/ScheideReplacementBoundaryParity.lean:113
Sixteen finite-union counts repeat an insert induction after obtaining pairwise disjointness and fiber cardinalities. Copies occur in CriticalGraphElementaryWitness:127/415, DensityLowerBound:50, ElementaryClosedMissingColorOdd:109, ScheideMaximalOddOrder:112, StronglyClosedWitnessElementary:812, ScheideGlobalMaximumBoundaryFacts:69/151, ScheideBalancedCandidateMaximumOrder:350/444, ScheideDefectiveThirdBoundaryEdge:466/567, ScheideReplacementBoundaryParity:113/155 and ScheideEnlargedBoundarySelection:481/572 (all .lean). Replace these with Finset.card_biUnion and the supplied cardinality facts, directly or through one constant-cardinality corollary. This removes sixteen independently maintained versions of elementary finite-set bookkeeping.
Evidence: private theorem helper_hinternal_union_287.{u_1, u_2} :
Body excerpt:
have aux : ∀ s : Finset E, s ⊆ internal →
(s.biUnion fun e => (G.ends e).toFinset).card = 2 * s.card := by
intro s hs
induction s using Finset.induction_on with
| empty => simp
| @insert e s hes ih =>
rw [Finset.biUnion_insert]
have hd : Disjoint (G.ends e).toFinset
(s.biUnion fun f => (G.ends f).toFinset) := by
rw [Finset.disjoint_left]
intro v hev hvs
obtain ⟨f, hf, hvf⟩ := Finset.mem_biUnion.mp hvs
have hh := hinternal_disjoint
(hs (Finset.mem_insert_self e s))
(hs (Finset.mem_insert_of_mem hf)) (by
intro heq
exact hes (by simpa [heq] using hf))
exact (Finset.disjoint_left.mp hh) hev hvf
rw [Finset.card_union_of_disjoint hd, hendcard]
rw [ih (fun x hx => hs (Finset.mem_insert_of_mem hx))]
rw [Finset.card_insert_of_notMem hes]
omega
exact aux internal (by intro e he; exact he)
- duplicate-proof —
LeanPool/GoldbergSeymour/ExtensionBaseClaim43TreeEdges.lean:96
TwoColorComponent.edge_colors already supplies this conclusion without series or finiteness data, but seventeen vertex-rooted extraction blocks still rebuild reachability, support and neighbor analysis. Copies remain in ExtensionBaseClaim43MissingColors:54, ExtensionBaseClaim43Stability:180, ExtensionBaseClaim43TreeEdges:99, ExtensionBaseClaim45Singleton:100, ExtensionBaseClaim46:535, ExtensionRulesTerminalLastAppearance:103, HierarchyClaimNineFirstUseSeed:1441, HkuIncidentColorPreserved:203/280, HkuParallelBoundaryStructure:627, HkuUnsupportedVertexColors:180, ScheideDefectiveSecondTerminalComponent:411, ScheideDefectiveSwitchEffect:144/169, ScheideEnlargedSwitchTransport:711, ScheideReplacementPairFixed:170 and StableSwapComponentEdgeUnique:66 (all .lean). Reuse edge_colors and share the recurring incidence-to-endpoint consequence, so component implementation changes do not require parallel proof repairs.
Evidence: theorem ExtensionBaseClaim43TreeEdges {V E : Type*}
Body excerpt:
have activeColor : trace.coloring b.castSucc f = some (trace.gamma b) ∨
trace.coloring b.castSucc f = some (trace.delta b) := by
have edgeSupport : Sum.inr f ∈ H.support := by
apply SimpleGraph.mem_support_of_reachable
(G := H) (u := Sum.inr f) (v := Sum.inl (trace.support b))
· simp
· exact SimpleGraph.ConnectedComponent.eq.mp edgeMem
obtain ⟨neighbor, adjacency⟩ := H.mem_support.mp edgeSupport
cases neighbor with
| inl v => exact adjacency.2
| inr e => simp [H, TwoColorIncidenceGraph] at adjacency
The existing general provider is:
theorem TwoColorComponent.edge_colors {V E : Type*} {G : LooplessMultigraph V E} {k : ℕ}
{phi : PartialEdgeColoring E k} {alpha beta : Fin k} {vertex : V} {edge : E}
(member : Sum.inr edge ∈ TwoColorComponent G phi alpha beta (Sum.inl vertex)) :
phi edge = some alpha ∨ phi edge = some beta := by
Tokens: 7,723,623 in / 71,003 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $31.9595 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
CI was not green for this commit at review time; this review does not replace CI.
|
/review Please review exact current head The complete734-module public aggregate builds warning-free; all15 native linters pass22,345 declarations, compiler diagnostics are zero, text style/static quality/generated indexes/card checks pass, both full trust audits pass, and all506 original theorem contracts pass. These records match current source hashes. Focused before/after measurements are in the PR body. A new whole-project clean measurement and exact-head CI remain pending; prior-head CI is not claimed for this revision. No queue or auto-merge action has been taken. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source review at 8b8bd48522f16d020e364500412cd608536aec36 is favorable.
I checked all 22 changed source bodies against 95be6b2, with independent reviews of the shared coloring facts, their callers, and the assembly and terminal-data changes. The concrete maintenance findings from review job2350 are addressed: six certificate-case proofs reuse the existing coloring API; the B/C swap proofs retain their weaker hypotheses through shared present-color lemmas; prefix/minimum-position and component facts replace the repeated local arguments; and the four assembly copies now use one transparent constructor.
The existing public theorem headers and structure fields remain unchanged. The 734-module import graph is closed and acyclic, and the project facade, card, dependency pins and checks are unchanged. The retained source, licensing, provenance, significance and scope decisions still apply; no new mathematical or source-quality finding remains from this delta.
This review does not reproduce the author’s local build, trust audit, environment counts or timings. Current-head compiler, lint, style, quality and other required validation remain separate. The completed CI qualification for 95be6b2 is retained only for that older revision. The existing /review request for this new head needs no duplicate.
|
/review Please review exact current head All ten additionally cited certificate analyses use TashkinovSeries.coloringProperties. A generic first-position membership theorem needs only arbitrary tree/coloring/color data, Fintype E and a strict bound; six coupled membership helpers and neighboring bound helpers were removed. The two coupled disjointness helpers were replaced by general Finset facts.61 import headers shed205 imports and added91 narrower imports, preserving private/import-all flags and non-import text; follow-up analysis found no further suggestions. Six new naming-linter findings were fixed without waivers. Current scope:770 modules,418389 physical lines,3301 imports;762 modules in the root closure. This repair cuts5464 net lines. All local checks pass on identical source hashes: complete aggregate1915 jobs with zero warnings,15 native linters over22354 declarations, compiler diagnostics zero, style/static/generated indexes/card resolution, full axiom/option audits and all506 original theorem contracts in17 batches. No checks/configuration changes, waivers or theorem weakening. The final clean two-thread root build passed in1418.949s, user/system CPU2457.981s /305.856s, peak child RSS3,430,692KiB. The compatibility baseline was1240.430s /2,165,628KiB with4341 warnings and source budget overrides, not acceptable content. Both use clean private project artifacts and warm exact dependencies on the same shared16-CPU VM. Raw changes and host-load limitations, all seven focused before/after profiles (including neutral/regressed observations), and scope growth are disclosed in the PR body. No isolated whole-project speedup is claimed. CI on this exact head remains a separate requirement; individual current-head contexts are inspected. The previous8b green CI is not assigned to this revision. Current-head Greptile established no new blocking defect and explicitly reports incomplete coverage. No queue or auto-merge action has been taken. |
|
Partial-port advisory resolution for
The short This resolves the completeness concern represented by this filename/LOC heuristic. No gate, threshold, waiver or challenge statement was changed. Current-head CI and the fresh five-rubric review remain separate requirements; no queue or auto-merge action has been taken. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed exact head 45810e743d89ee3d7340b11f426cd9bc57a3a655.
The source review is favorable. I reviewed the complete 94-path refactor, including all 36 new shared-fact modules, with independent checks of contracts, moved proofs, constructors, imports and callers. The card, headline theorems and foundational mathematical structures retain the previously reviewed scope and provenance.
The two quality findings from the 8b8bd485 review are addressed across the cited families: the mixed-change, disjoint-theta and extension branches share proved interfaces; certificate branches use the existing coloringProperties; first-position membership now has an arbitrary-tree lemma without the hierarchy reconstruction premises; and the elementary disjointness cases use general Finset facts. Expanded statement aliases and retained callers preserve the original assumptions and conclusions. The two removed public generated helpers are unused and superseded by the general first-position facts.
I found no remaining source blocker in these changes. This is a source judgment, not a build or performance result: the current-head Lean workflow and canonical check remain pending. The existing current-head five-rubric request is retained; older-head CI and review results do not qualify this revision. Protected integration still requires the independent current-head review, complete applicable CI and current-main/native-queue checks.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
At 45810e743d89ee3d7340b11f426cd9bc57a3a655, I checked the published review’s remaining quality findings against the actual source. The four core rubric passes remain separate from the advisory quality result.
The remaining repair is concrete: remove six private TwoTwo forwarders and three private prefix helpers; consolidate ten copied segment, missing-leaf, root-swap and adjoin proofs; and replace broad restoration-context arguments in elementary shared facts with narrow premises. The missing-leaf fact must continue to work without assuming distinct colors, and the root-swap fact must not acquire a proper-coloring assumption. Existing public theorem statements and compatibility wrappers must remain available.
I have prepared this bounded cleanup in an isolated worktree based on this exact head. Independent source checks preserve the existing public contracts; compiler and lint validation is still pending, and the published branch has not been changed. The current head’s complete authored checks are qualified, but queue admission remains pending this source repair and the repaired head’s normal checks and review.
|
The filename/LOC advisory on exact head
Descriptive renames, imported preparation modules and shared proof facts account for the observations. The full775-module aggregate, native linters, style, quality, axiom/option audits and original contracts pass locally on matching source hashes. Fresh CI remains pending. No missing theorem was found and no waiver was added. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed published head b3795278cbdd83738da8e985c700590383ba4fc6.
The complete source delta resolves the earlier quality findings: forwarding layers and copied tree/Kempe/adjoin proofs are replaced by shared facts, and prefix/augmentation transport now uses the data it actually needs. I traced the removed helper interfaces to their replacements and checked the surviving consumers. Port-only helper names have been retired; this is not a claim that every old exported helper name remains available.
The forward missing-neighbor fact still needs no distinct-color hypothesis, and the root-color swap fact adds no proper-coloring hypothesis. Removing the unused finiteness premise from augmentation initial-segment transport strengthens that result. The original mathematical statements, graph bridge, project scope, attribution and provenance remain intact. The complete 775-module aggregate is acyclic and contains all project modules.
My source verdict is favorable for this exact revision. Its current-head hosted validation, configured project review and normal protected integration remain separate requirements. The earlier-head checks and my unpublished targeted repair build are not credited to this head.
|
/review Please run the configured project-rubric review for current published head |
|
The filename/LOC advisory on exact head
Descriptive renames, imported preparation modules and shared proof facts account for the observations. The full775-module aggregate, native linters, style, quality, axiom/option audits and original contracts pass locally on matching source hashes. Fresh CI remains pending. No missing theorem was found and no waiver was added. |
|
Independent source review of
The full target bodies and existing structural providers were inspected. License, provenance, trust, and mathematical-fidelity blocking rubrics pass; these engineering findings remain actionable. All13 fresh pre-edit profiles and the published-source clean baseline are preserved before source changes. The previous endpoint/generalized API contracts remain part of validation. No merge or queue action is requested. |
Factor closure transport, ladder restrictions and first appearance, and terminal series/correspondence construction at actual consumers. Preserve all public contracts and remove obsolete private continuation telescopes. Validation: eleven exact-source local phases, kernel contracts and supplemental private trust/reachability; controlled clean and focused measurements.
|
/review Review exact current head |
|
REQUEST CHANGES at Source inspection confirms two engineering findings from review 2404:
Fresh profiles are being captured on this clean published source before repair. Public statements and definitions must retain their strength; all applicable validation and independent review must be assessed again after the changes. This comment performs no queue or merge action. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source review at bc74c9245d10b7dac1f411e956cbcc9d21e26368: the three families in the previous amended review are resolved. The new closure transport preserves vertex-set containment and incident-edge/missing-color agreement; the shared certificate constructors preserve distinct SE/PE/RE and zero-prefix one-round cases; the ladder/first-appearance transport retains its display equality, finite bounds and actual correspondence data.
After independently inspecting the new findings in configured review 2404, two further maintenance repairs remain. These concern pre-existing code unchanged from 9a4535e159…; they do not undo the three completed repairs:
- Replace the five private augmentation-transport proofs (
helper_transportStep_1463,helper_transportSeedStep2_2940,helper_transportSeedStep_5350,helper_transportSeedStep_6612, andhelper_transportStep_335) at their actual callers withTashkinovAugmentation.transportBeforeVertex. The callers already supply the stability and strict-prefix vertex-before witnesses. The repeated attachment-index casts, incidence and missing-color argument belong in that provider; the private proofs do not need restoration-trace, component-path or candidate-minimum arguments. Preserve existing public wrapper headers and Conditions, includinghelper_transportSeedStep2_6201; change their augmentation leaf or forwarding proof. - Remove the 393-line
helperHless4484Conditionscontract around the elementary comparison inhelper_hless_4484. Its sole caller already constructs the genuine hierarchy/counterexample and provespathLeandtailLess. Inline the comparison there, or extract the existing four-number lexicographic lemma into an appropriate common dependency. Keep the actual hierarchy certificates and minimality argument at the caller. The sibling three-line inline comparisons do not themselves require a broader refactor.
These are concrete, bounded maintenance requests, independent of the advisory numeric grade. The mathematical statements, provenance, significance and bounded novelty assessment remain favorable. The complete 13-file delta preserves the 1,877 existing public headers and 426 public non-proof values; the 815-module import graph remains acyclic.
Changes remain requested for these two families. The existing owner repair plan is sufficient; repairs stay author-owned. Required hosted CI remains independent, and the completed checks at 9a4535e159… apply only to that earlier head.
Reuse augmentation transport at five actual consumers and share hierarchy-independent lexicographic comparison across four change-lemma branches. Preserve all public contracts and remove repeated private proofs and the obsolete private numeric telescope. Validation: eleven exact-source local phases, kernel contracts and supplemental private trust/reachability; controlled clean and focused measurements.
|
/review Review exact current head |
|
REQUEST CHANGES for I inspected the complete general route-transport provider, all six repeated route proofs, the public forwarding adapters, and their actual callers. Each route proof already has the callback accepted by I also read the complete types and proofs of These are actionable maintenance findings in the current source. The six fresh before-edit profiles and the complete clean baseline are preserved; repairs will be revalidated and measured. No queue or merge action is authorized by this review. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source review at 7b7481d43225d38f12bcb02cc50fcdab3ade473e: both repair families in my previous review are resolved. The five augmentation consumers use TashkinovAugmentation.transportBeforeVertex with their actual tree, stability and finite-index witnesses. The four lexicographic consumers use the new four-number theorem while retaining the real goodS/CS construction, certificates, path bounds and minimality argument.
I independently checked the two additional findings in review2409 and agree with the owner’s current exact-head disposition. Two bounded engineering repairs remain:
-
Reuse the existing route transport theorem at all six copies.
TashkinovAugmentationSequence.transportalready accepts exactly the step callback and route supplied byExtensionBaseStepLemmas.helper_transportSeedRoute_2514,helper_transportSeedRoute2_3173,ExtensionBaseBranchPreparation.helper_transportSeedRoute_4083, and the local route proofs inExtensionBaseBranchLemmas,ExtensionBaseCaseTwoContradictionandParallelSupportClosureProperties. Their repeated head inductions can delegate directly to that theorem. Preserve the three public adapter signatures and forwarding wrappers as thin compatibility layers. Keep the actual seed orP, first/second coloring, T/Tj membership and stability witnesses, and branch-specific certificate construction; this replacement needs no new ordered-closure hypothesis. -
Separate the elementary facts from their restoration-specific interfaces.
ExtensionBaseBranchPreparation.helper_hxNe_3545,helper_hcomponentNonempty_3523,helper_hgammaFirstZero_3790and the forwardinghelper_hgammaFirstZero_6905pass large unrelated ETT/restoration/color/terminal-position bundles for small path or finite-index facts. Use a narrow graph/index fact, or a local derivation, in the three actualExtensionBaseBranchLemmasconsumers. Retain these public signatures as compatibility forwarders. The complete callers still need their real support, trace, properness, boundary, certified-tree, gamma-chain and hierarchy data for their later construction; do not delete those premises from whole callers or Conditions.
These are concrete maintenance issues in active proof paths, not a numerical-score veto or a claim that the mathematical result is false. The complete ten-file delta and all 817 published source bodies were bound to this head; the existing public contracts, retained definitions, original mathematical endpoints and acyclic import graph are preserved. The prior mathematical, provenance and source assessments retain their established exact-source scope.
Source disposition: changes requested for these two families. The owner’s published plan already retains repair custody; this review consolidates the resolved and remaining findings. I have not used private author work, compilation or timing claims as validation, and have not compiled the proposed replacements. Fresh exact-head review results and hosted checks remain independent requirements before normal protected integration.
Use general route transport at actual consumers and compatibility adapters; share first-step extraction and reuse initial-segment facts. Remove unrelated restoration/component arguments from live path and finite-index calls while preserving every existing public contract. Validation: eleven exact-source phases, kernel contracts, supplemental trust/reachability, controlled clean and focused measurements.
|
/review Review exact current head |
|
REQUEST CHANGES on exact head Independent source inspection confirms the new engineering findings. Complete types/bodies of Complete types/bodies of Configured job2411 passes faithfulness, significance and sources, discusses novelty (no duplicate found; bounded Tau Ceti comparison) and advisory quality2/5. Its full76line sanitized report has been read. The novelty limitation requires further independent evidence rather than treating previous endorsements as authority. Fresh before-edit profiles are being captured on the unchanged published source; the existing controlled clean baseline and all earlier checkpoints remain preserved. Greptile33 reports no new blocker in this six-file repair and explicitly limits whole-import approval. All ten hosted Lean shards have passed, with assembly/lint and minimal-file validation pending. These observations do not resolve the newly confirmed source findings. No queue or auto-merge action is authorized by this review. |
|
Independent source comparison addressing review2411's The pinned public text comparison now covers 27,571 retained Tau Ceti Lean files (300,126,988 bytes) at
No duplicate of either headline was identified in this expanded comparison. This is a bounded mathematical judgment over verified source and matching declarations, not a machine-proved global absence, an all-lines proof audit of either library, or a replacement for the next exact-head configured review. Review2411's recorded verdict remains |
…lification Share arbitrary-edge route containment and restriction across SE/RE branches; use general tree-position and prefix APIs at actual consumers. Remove obsolete private prefix plumbing while preserving every public contract and retained data definition. Validation: eleven exact-source phases, kernel contracts, supplemental trust/reachability, controlled clean and focused measurements.
|
/review Review exact current head |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed exact head 83ada76139a7a2825142add61618b21e196005ef, including all nine changed files and the actual structural providers and reconstruction callers. Both engineering repair families requested at 9c15253 are resolved; I found no new material source issue in this delta.
The twelve SE/RE branches now reuse TreeSequenceAdjoinEdge.initialSegment_of_route and restrict_route on the actual arbitrary edge and augmentation route. Equality transport preserves the full adjoin witness, including its final-edge data. Restricted prefixes and suffix routes retain their distinct directions, branch-kind metadata and later coloring certificates.
The affected rightOutside and hiSeed consumers now call vertex_not_mem_after and the common-prefix length_lt_of_vertex_not_mem directly. The latter correctly rules out an early position by transporting its vertex through the shared initial segment. The existing prefix theorem replaces the single-use private wrapper; its retired name has no remaining written use. Public compatibility interfaces and the reconstruction proofs’ later data remain intact.
The complete published source audit preserves the existing public written headers, definitions, Conditions, original contract statements and headline endpoints. Three general structural facts are added; no card, root index, dependency, gate or resource-limit change is bundled. The two explicit cardinality simplifications preserve their actual distinctness premises. Earlier coverage is reused through unchanged source bytes, not old-head approval alone. I have not adopted the private compiler or timing claims in the description.
The current configured review request is already posted; its exact-head result remains pending. The new head’s Lean and real exposition workflows are also pending. I independently bound their actual checkout 3f03951 to this published source plus current main 2b205bf and its own build plan. Source review is acceptable for integration once those independent requirements and the normal protected queue checks pass.
|
REQUEST CHANGES — engineering. Separate thorough review update of exact head
The current source has a controlled clean baseline and preserved focused profiles; capture missing local module baselines before this repair and measure the rebuilt result. Preserve public theorem types, assumptions, definitions, trust and default resource limits. This review update performs no queue or merge action. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source161 follow-up — engineering changes requested at 83ada76139a7a2825142add61618b21e196005ef. I independently checked the complete helper types, proofs and callers behind the new findings.
- Extract or reuse one component-swap edge-preservation lemma for an edge incident to a vertex outside the swapped component. The three
helper_incidentFixed_651/818/582proofs repeat the same component-membership and color split; their hierarchy, missing-position and prefix arguments are unnecessary for this fact. Use the same lemma for the first conjunct ofP2880_T1_ElementaryPrefixSwap, preserving its public statement and substantive missing-color second conjunct. - Remove the construction-heavy private wrappers
PositivePrefixNoRevisiting.helper_branch_3047/3057/3071: their callers need only the incompatible extension-kind equalities at the same index. Likewise, the four vertex-alternative helpers inScheideHeightFiveGammaEdgesandScheideHeightFiveOutsideLinkscan use direct disjunction elimination with the stated inequalities, without carrying graph/hierarchy construction data.
These are two concrete, bounded maintenance repairs. The two earlier job2411 repair families remain resolved, and the mathematical statement, provenance and bounded novelty assessment remain accepted. The author has already retained these new repairs in the published repair plan. Preserve public theorem types, assumptions, definitions, trust and default resource limits; review the published repair and its checks at its new exact head. Engineering acceptance remains pending that repair.
Use a general swap lemma at all three mixed change cases, elementary prefixes and enlarged strict augmentation. Remove ten obsolete construction-coupled private proof interfaces and use direct constructor contradictions and vertex-disjunction simplification at their callers. Preserve every existing public type, named argument and retained data definition. Validation: eleven exact-source phases, kernel contracts, supplemental trust/reachability, controlled clean and focused measurements.
|
/review Review exact current head |
|
REQUEST CHANGES — engineering follow-up on exact head The actual cited types, full proof bodies, general provider and live callers confirm two maintainability defects. This conclusion comes from source inspection, not earlier endorsements.
The four modules have fresh before-edit default-limit profile captures on this committed source, and the full logs and all four resource axes were inspected and preserved. Their user CPU values are respectively 13.918818, 17.593605, 8.571832 and 4.150849 seconds; the controlled complete-project baseline remains 1054.137732 wall / 1921.682816 user / 310.925982 system seconds with 2695944 KiB maximum individual-child RSS. Shared-host timing variation is retained, with no causal speedup claim. All eleven local phases and the existing source/statement/trust evidence remain preserved. All ten hosted build shards passed, while assembly/lint and remaining protected contexts are still pending. No merge readiness is claimed. I will repair these confirmed issues on the existing isolated author branch, preserve public mathematical contracts and data, rerun the required checks and measurements, and obtain fresh review of the resulting source. No queue or merge action. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source162 — engineering changes requested at cfb781341bc8b079725d2b256951adc4d7f27673. I independently verified both new job2415 maintenance findings against the complete metadata proofs/providers and the eight forwarding declarations with their live callers. I agree with the published repair plan.
Preserve two compatibility boundaries during that cleanup:
- The three metadata helpers
helper_hseriesDataAgree_772/3459/3932are public. Keep their theorem types and named-argument compatibility as shims while the live metadata proofs reuseTashkinovSeriesData.castMetadataAgreement. Narrow only the metadata dependencies: the parent PE tree-agreement construction still uses its path and certificate data. Preserve the distinct SE/PE terminal metadata. - Keep exported names and dependent contracts when routing
Preparation6directly to augmentation/replacement providers 640/742. Preserve the substantive PE/nonparallel construction, route/stability and correspondence data, MaximumProperty, SameHierarchyStages and later GoodHierarchy assembly.
Both Source161/job2414 repairs are resolved, including the shared incident-edge preservation lemma and removal of the seven logical wrappers. The elementary-prefix second conjunct and positive-prefix PE branch remain intact. The prior mathematical, provenance and bounded novelty findings remain applicable within their unchanged-source scope. Engineering acceptance awaits the author's published repair and fresh exact-head validation; no private compilation or performance claim is adopted.
Use existing structural cast agreement in terminal-series consumers and compatibility proofs. Replace nine repeated theorem interfaces with standard aliases and call primary both-outside providers directly. Preserve all 1880 public interfaces, named arguments and 711 retained data definitions. Validation: eleven exact-source phases, original kernel contracts, supplemental trust and reachability, controlled clean and focused profiles.
|
/review Review exact current head |
There was a problem hiding this comment.
Source164, revised after configured job2418: engineering changes requested at d98983e34879bd216f6903128373c491f1bcea51. Both Source162/job2415 repair families remain resolved: the metadata paths use the general cast providers, and Preparation6 reaches the substantive augmentation/replacement providers through the preserved compatibility interfaces.
I independently checked the two newly reported maintenance families against the published proofs, providers and live consumers:
- Component-edge color proofs. The three Transport helpers 4879/4960/5296, UndoStable helpers 1176/1288, Basic2TerminalPE 904, ParallelTerminalPEPreprocessing 910 and the two Scheide variants repeat the support/reachability argument. Factor a shared result for an edge in a component rooted at a vertex, using the existing
TwoColorIncidenceEdgeColorsadjacency result. The vertex-root condition matters: an arbitrary isolated edge-root need not have either color. Route the live consumers through that smaller result and retain the three exported Transport contracts as compatibility wrappers. Keep the actual colorings, roots, color pairs and larger extension/Scheide certificates intact. - Walk/region helper interfaces. The nine public helpers 4016/4031/4043/4055/4070/4119/4150/4210/4255 in
RevisitingTerminalPreparationcarry unused prefix/correspondence, defective-choice and color-equality payload into their liveTdTerminalRERebuildapplications. Extract the elementary walk/region facts with their real premises, then use those directly internally while retaining all nine exported contracts. Preserve support witnesses, minimum-index bounds, inside endpoints, bipartite adjacency, the return-index gap and cycle injectivity on(0, length]. The enclosing reconstruction still needs its induction, properness, stability, correspondence, cast and path certificates.
These are two bounded medium repairs. The current mathematical, provenance and source-informed novelty findings remain favorable within their reviewed scopes; the numeric quality grade is not the decision rule. The previously resolved job2415 work should stay resolved.
The current configured review passes its first four rubrics. Its private compilation claims are not adopted here. Hosted validation remains independent: the observed shard00 error was an Elan download HTTP504 before compilation. Preserve author branch custody, publish the repairs, and run the normal exact-head reviews and protected checks. Current Main also retains its infrastructure hold pending its own push validation.
|
Independent acquisition review of The configured review's mathematical faithfulness, novelty, significance and source assessments pass. The prior metadata/cast and theorem-forwarding repairs remain valid. These findings concern additional code:
The published checkpoint and its measured baseline are preserved. Ten additional fresh, sequential two-thread before-profiles were captured before edits, with complete logs inspected. Repairs are in the isolated author worktree; they require a complete build, warning/lint/style/quality/trust checks, original-contract replay and comparable performance measurements before publication. No merge or queue request is authorized by this review. |
Use one vertex-rooted component color theorem and general walk-region facts at the actual terminal and Scheide consumers. Reuse caller predicate decisions, retain public contracts, and remove six private duplicates and all finite-set conversion adapters. Validation: eleven exact-source phases, original kernel contracts, supplemental trust and reachability, controlled clean and fresh targeted profiles.
|
/review Review exact current head |
|
REQUEST CHANGES — consolidate the remaining finite-union and component proof families. Separate thorough acquisition review of exact head Two concrete maintenance findings remain:
The mathematical/source assessment remains independent of reported reviewer endorsements: the explicit finite loopless multigraph bound and high-index equality match the definitions and cited Chen–Jing–Zang theorem; independent edge IDs preserve parallel edges; the active-set Graph bridge does not claim equality to an unsupported native chromatic-index invariant. The pinned Apache-2.0 Tablet source, AI/Trellis provenance, October 12 day-precision completion evidence, and original eligible interval are recorded. Actual bounded Mathlib, Tau Ceti and current-main comparisons identified no duplicate of the advertised arbitrary-multigraph headlines. Prior-verdict prose was not used as mathematical authority. Observed validation: all eleven exact-source local project phases and 545 original/generalized contracts passed, including the full safe-private trust audit. Hosted CI has ten successful exact-head shards and successful assembly/lint in the latest observation; required minimal-file verification is still pending. These observations do not waive the remaining protected checks or the unresolved source findings. The configured faithfulness worker reported its own Mathlib-fetch HTTP 403, so I do not claim that worker recompiled the project. The controlled clean measured 1406.637111 s wall / 2081.777522 s user / 332.429137 s system / 2,689,688 KiB maximum child RSS, with a separate 10.886811 s public aggregate. The explicit uncommitted intermediate baseline was 1041.690629 / 1972.763439 / 320.992213 s and 2,702,216 KiB; published parent measurements and all higher/lower observations are retained in the description. All 39 final profile vectors, 30 actual before pairs, nine after-only targets, all 809 clean rows, full edited-module logs and the fixed repeat set were read. No stable CPU or whole-build speedup is claimed. Additional before-edit profiles for the newly affected modules have now been captured; the next repair must preserve theorem strength and pass a new source-bound validation and measurement cycle. This finding requests author repairs; it is not approval, queue readiness, or a merge action. The quality rubric is advisory, but these specific reusable-infrastructure repairs are actionable and will be handled on this PR. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source review 170 at 8f481868729f128cef2d2af6216536daff8b6675: two further bounded maintenance repairs requested.
Both earlier Source164R2/2418 families are resolved: the vertex-rooted component theorem replaces the original repeated arguments, and the walk/region API removes unrelated reconstruction data from the actual elementary consumers. The twelve public compatibility contracts remain intact.
I independently corroborated the two further families identified in the new acquisition review:
- Finite-union counts: sixteen sites in fifteen complete programs repeat insert induction despite already having pairwise disjointness and fiber cardinalities. The actual pinned Mathlib
Finset.card_biUnion, followed by the supplied constant-cardinality sum, gives these counts directly. Eight counting-only private wrappers each have one live use and can be removed at their four enclosing consumers. Preserve the genuine matching, oddness, eligibility, maximum-order and Scheide-witness arguments around these leaves. - Component extraction: seventeen blocks in sixteen complete declarations repeat vertex-rooted extraction. Three need only the color conclusion supplied by
TwoColorComponent.edge_colors; fourteen also need the shared consequence that an incident vertex belongs to that component. Share that consequence while retaining the vertex-root restriction: an isolated edge root does not justify the same claim. Keep the higher missing-color, properness, stability, path/degree, tree and routing certificates.
These are concrete medium reuse requests, not mathematical counterexamples or an automatic veto from an advisory grade. The bounded inspection covers all cited sites, their full containing programs and actual downstream use records; it does not claim a fresh semantic audit of every line in the import.
Written preservation checks retain all prior public headers, all nineteen existing alias commands, the 506 original and sixteen endpoint contracts, and all 712 existing nonproof value token streams. The one raw-value difference is an attached documentation comment. Other source is inherited only through identical native Git bodies. No private author build, compiled manifest, kernel-contract run or performance result is credited as this review's own validation.
Author custody remains in place. Please publish the two repairs with preserved theorem strength and normal validation; fresh exact-head configured review and all protected checks remain independent. No branch takeover, queue admission or waiver is made here.
This imports the unconditional Goldberg–Seymour edge-coloring bound for every finite loopless multigraph:
ChromaticIndex G ≤ max (MaximumDegree G + 1) (DensityCeil G).Parallel edges have independent identities. Odd-set density is the maximum of zero and
2 |E(U)| / (|U| - 1)over odd vertex sets of size at least three; the chromatic index is the least size of a proper full edge-coloring palette. The import also proves equality with the density ceiling when the chromatic index is at least the maximum degree plus two. These are existence results; the card makes no executable-algorithm or polynomial-time claim.The primary mathematical source is Chen, Jing and Zang, arXiv:1901.10316v2, Theorem 1.1 and §2.2. The public Lean source is wpegden/goldberg_seymour at 88d98c1d1a59d1f1bf7c4eb58e73f3945f6daf12. The author's Trellis page dates material completion 2026-10-12, at day precision. The snapshot's authored/committed time is 2026-10-12T19:36:46Z; that corroborates the day and is not asserted as an exact announcement timestamp. It lies inside this recovered acquisition's original interval [2026-09-05T10:45:10Z, 2026-10-29T10:45:10Z).
The upstream Apache-2.0 license expressly covers the Tablet Lean sources. The import contains Lean code; paper text and the proof-generation service are excluded from its dependency scope. Provenance is AI: Trellis operated by Wesley Pegden, with Lean Pool porting and general API work credited to Lean Pool contributors. Required headers, source pin and paper attribution are retained in the single project card and code.
The imported upstream dependency closure contains 684 source modules. The port and shared APIs have 817 source modules, 809 in the headline closure, 347,067 physical Lean lines and 3,875 direct import edges. Seven supporting modules and the generated aggregate retain useful infrastructure beyond the headline closure. The exact target is Lean 4.35.0, Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679, and ten tracked-clean dependency revisions. One YAML project card and generated public wrappers register the project;
LeanPool.leanremains fixed.Reusable infrastructure covers proper partial edge colorings, incidence-based Kempe components, critical subgraphs, Tashkinov trees, extension sequences, stable coloring transport and good hierarchies. The Mathlib
Graphbridge uses active vertex and edge subtypes, preserving isolated active vertices and distinct parallel edges, and supports finite active sets in infinite ambient types. Its bound concerns the imported invariants of the converted graph; it makes no unsupported identification with a native Mathlib chromatic-index definition.Current exact head:
8f481868729f128cef2d2af6216536daff8b6675.Component edge-color extraction now has one general vertex-rooted component theorem. It needs only component membership, without finiteness, proper coloring, distinct colors, series data or defective-choice certificates. Nine actual call sites use it; six private duplicate wrappers are removed and three public compatibility proof bodies share the provider. Requiring a vertex root is essential because an isolated edge-rooted component need not have a selected color.
The new
WalkVertexRegionmodule supplies two index sets and six facts about arbitrary walks on a sum type and an arbitrary vertex region: finding an outside position, membership before the first exit, positivity and endpoint bounds, existence of a later return, and exclusion before that return. Nine live crossing/index calls use this API or Mathlib's existing adjacency/cycle injectivity facts directly. Their mathematical inputs no longer carry Tashkinov-tree, prefix or color-agreement scaffolding. The API takes the decisions for its index predicates, so finite and classical callers reuse their own decisions directly. This removes all finite-set conversion proofs from the two consumers. The predicates add no finiteness, tree or coloring assumptions. Six complete prior canonical theorem contracts replay against the new API on arbitrary, possibly infinite, vertex and edge types. Public compatibility statements keep their original types.Twelve Lean files change, including the generated public Imports wrapper and the new module. All 1,871 ordinary public declarations and 19 existing aliases retain their complete headers/statements and user-named arguments. All 711 previous public/private nonproof definitions remain unchanged; two index definitions are new. Thirteen public proof bodies change. Earlier reports counted 1,880 interfaces as the ordinary declarations plus nine recent aliases; the ten older aliases are also retained and explicitly included here. No card, root index, dependency, toolchain, configuration or gate is changed.
All 18 original helper contracts/proofs and their 18 actual caller blocks, every changed hunk, the complete new module and the existing providers were inspected. Other coverage is inherited only from the immutable published parent through identical source bytes. An independently compiled minimal-import trial removes an unused tactic import. A second isolated trial and the six complete canonical contracts validate the decision-input API before removing conversion adapters. Initial type/decidable-instance and binder trials are excluded from successful validation; no resource limit override was introduced.
All eleven exact-source local phases pass: complete warning-free public aggregate, generated indexes/card declarations, style/static quality, Mathlib linters, compiled diagnostics, declarations, axiom/option audits and original contracts. The unchanged current-main compiler plugin freshly compiles 131 modules and preserves 686 identical complete contexts with zero diagnostics. The compiler reuse baseline is the explicitly preserved uncommitted, fully validated F snapshot; published E remains the public-contract and git-parent baseline. Reuse requires identical transitive source bytes, plugin/options/toolchain/configuration and all ten tracked-clean dependency revisions. The 506 original signatures in 17 batches, 24 inherited contracts, nine original alias contracts and six complete canonical walk contracts (545 contracts total) pass kernel replay; compiled alias universes, safety, binder kinds and user names are retained. The supplemental trust audit checks 19,547 distinct safe declarations including 15,198 private declarations. Allowed axioms remain only
Classical.choice,propext,Quot.sound; zero source-declared private proofs are unreachable and 948 generated residuals are classified.Clean command:
LEAN_NUM_THREADS=2 lake build LeanPool.GoldbergSeymour, deleting only this isolated worktree's build artifacts. The published parent has an 808-module headline closure and 816-module public aggregate. The fully validated uncommitted intermediate F baseline and current G each have an 809-module headline closure and 817-module public aggregate. The same ten pinned dependencies are warm and tracked-clean, with no owned compiler overlap. Other activity on the shared 16 CPU host is uncontrolled. RSS is the largest individual child's usage, not aggregate RAM.d98983e348798f481868729fSeparate full-aggregate wall times are 14.130418 s for published E, 8.900428 s for uncommitted F, and 10.886811 s for G; separate CPU/RSS were not measured. The original different 685-source scope measured 1240.429533 / 2019.935844 / 282.813140 s and 2,165,628 KiB and is not an equivalent-scope speedup baseline. Every intervening higher/lower clean result, control and source trial remains preserved in the historical checkpoints and the explicit F snapshot.
The final clean wall time is 35.03% higher than the validated uncommitted F intermediate; user CPU is 5.53% higher, system CPU 3.56% higher, and maximum child RSS 0.46% lower. These higher values remain in the report. No overall or causal speedup is claimed. Of 681 identical complete source/dependency contexts, 134 rounded per-file wall times fell, 62 were equal and 485 rose (median raw ratio 1.1818); this is descriptive and supplies no load normalization.
The pass has 39 fresh final profiles, 30 actual F pairs and nine after-only targets. Eight selected targets use the latest of nine F repeats captured before G edits; all 46 official F profiles and all nine repeats remain retained. All 809 clean rows, all four resources and available category/event data were read, including all eleven edited-module full logs (719 lines). No paired user-CPU increase exceeded both 15% and 0.2 seconds, and the individual logs/resources were judged independently of that screen.
A fixed seven-target repeat set followed the official pass because identical-source sampling varied. The following table retains all G observations for the three decision-API targets; these are repeated after samples, not new F baselines. Cells are wall/user/system seconds and maximum child RSS in KiB.
All seven fixed-repeat resource vectors and full logs were read and retained. The measurements do not establish a stable CPU improvement: the concrete result is a simpler shared API, removal of the conversion adapters, and retained canonical theorem contracts. The earlier 5.54-second cumulative simp category and thirteen unnamed individual events cannot be assigned to particular adapters. Categories overlap. Shared-host scheduling, CPU/cache behavior and other load are uncontrolled.
The full edited logs and current hotspots show no specific further material safe source repair supported by this comparison. Existing large hotspots were investigated in the preceding preserved passes; no resource override, weakened statement, changed gate or linter suppression was introduced. This is a bounded engineering judgment, not a claim of optimal proofs. Fresh hosted CI and independent exact-head reviews remain required.
There are 39 fresh focused profiles and no reused after samples: every edited mathematical module, current clean top20/largest20 absolute increases, four controls with unchanged source and the historical Seed lead. 8 of nine chronological latest F repeat profiles supply primary before values for selected targets; all 46 official F profiles and all nine repeats, captured before any G edit, remain retained; 30 targets have actual before pairs and 9 have no immediate F baseline profile; older historical observations are retained separately. Full clean timings cover all 809 headline modules. All four resources, leading overlapping categories, available top events, all 809 clean rows and full edited-module profile logs were inspected. The earlier F module profile reported 13 individual simp events and 5.54 s cumulative simp time; these unnamed overlapping events cannot establish ownership by the removed adapters and are not claimed as an attributable speedup. This targeted pass does not claim every changed transitive context received a separate profile.
All focused measurements
Independent novelty evidence includes actual source comparisons, subsequent actual source-delta inspection and freshly reconfirmed complete public source maps: TauCetiProject/TauCeti
7ca783d4c8d324c9c74efaacd641c8a40f69f284; leanprover-community/mathlib4ff2494ea5e438f8a8452db803068acd711fa0059. Existing incidence lower bounds, banana-graph equalities, bipartite completion/matching/flow results and conditional simple-graph bounds do not establish this arbitrary loopless multigraph sharp degree/odd-density bound. These are bounded mathematical comparisons, not a formal global absence theorem or an all-lines audit of either library. Pool history, public issues/PRs and actual current-main source deltas are assessed separately.Published parent
d98983e34879passed all eight required contexts, all ten shards and assembly/lint after one failed-job retry for an Elan HTTP 504. Its configured review passed the four mathematical/source dimensions and identified the two engineering families addressed here; Greptile reported limited coverage and no established new blocker, without whole-import approval. Those earlier results do not approve this head. Fresh exact-head configured GPT, Greptile, independent thorough review and CI remain required. Earlier main555f0468adadrecovered from a separate observed post-merge Elan installer HTTP 504 through a normal failed-job retry and all applicable individual validation workflows were subsequently observed green. Fresh green-main queue requirements still apply. Documentation preflight and minimal Lean validation remain gates; daily asynchronous publishing is separate. No queue, auto-merge, bypass or announcement is performed by publication.Latest main observation:
ebd251b92dfb1a37d13aed2b3c8ba287080daee8at 2026-11-09T08:50:58.847501+00:00. All applicable individual validation runs successful: False. Observed runs: Lean Action CI/push: in_progress/None; PR Separation Guard/merge_group: completed/success; Exposition Verify/merge_group: completed/success; Documentation/merge_group: completed/success; Python CI/merge_group: completed/success; Workflow Lint/merge_group: completed/success; Lean Action CI/merge_group: completed/success. The new ACMax source delta was independently inspected as Laplacian/spectral test-vector bounds and scalar charges, without a duplicate of this multigraph coloring theorem. This publication performs no queue or merge action; queue readiness still requires green applicable current-main validations.