WIP: Import Brill–Noether theory and gonality of finite graphs

[Vilin97]

Imports npflueger/brill-noether-graphs at ce62dd82fd499fcec9b5a4110a5312befd6e96e2 into LeanPool.BrillNoetherGraphs.

Formalizes Brill–Noether existence through genus five, chains of marked banana graphs and loops, the treewidth lower bound for gonality, and a tricycle example whose gonality drops under regular subdivision. Includes divisor and transmission infrastructure and the Demazure-product support used by vertex gluing.

The census retains all 527 production and required upstream modules, with dependency and layout modules giving 564 destination Lean files. Four new receipt modules hold the unchanged sparse Farkas data for rows 03, 04, 06, and 14; the original fixed-cover modules publicly re-export the same declaration names. Original attribution and license notices are preserved. The upstream duplicate open challenge and standalone execution harnesses remain outside the production scope.

The port remains in progress. Please leave this PR unmerged. No checks, settings, waivers, or resource budgets were weakened.

Validation at bdfad79f1:

• The unchanged scoped header, forbidden-construct, file-size, and proof-size checks report zero findings across all 564 files. Both module indexes include the four receipt modules.
• All 2,339 entries in the original missing-documentation inventory have been documented. Large proofs were separated into helper lemmas with their public mathematical statements preserved.
• The latest completed CI run reached four receipt modules with layout parser errors. Their replacement layout preserves every non-whitespace character and every sparse receipt value, keeping each inner record intact; kernel validation is pending. Two nested certificate types use the clearer CertificateData name, with all project references updated and the field contracts retained.
• The 496 reported goal-changing show tactics and 45 deprecated lambdas have been updated. Further structural and simplifier warning cleanup, a fresh full kernel build, and the scoped declaration-linter audit remain.
• Current main and the maintainer's whitespace and citation corrections were preserved by ordinary merges. Local compilation uses the shared resource lock and bounded compiler process tree.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Changes requested by automated review

Reviewed exact head d505061ed575f91bdd45ea52e858298a8645b6ac. The exact-head protected run fails lake exe mk_all --check: LeanPool.lean is out of date. Regenerate and commit the repository index from this branch, then rerun the complete required checks. Do not weaken the gate.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds mathematical proofs in a proof assistant library.

The PR should remain unmerged while its verified catalog status and public API boundary remain unresolved.

Findings

1.  Premature verified status ▶
2.  Duplicate public graph API ▶

Summary

This PR imports the Brill–Noether graphs formalization, its supporting modules, and a project catalog entry. No Brill–Noether files changed since the previous review. The import remains marked as work in progress, and the prior verified-status and duplicate-public-API findings remain outstanding.

_{Reviews (29) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[greptile-apps]

Premature verified status

This entry marks the project as verified, and the generated project card repeats that status, while the PR description says the Lean 4.34 build, lint cleanup, completeness reconciliation, and verification are still unfinished. The repository requires pooled projects to be finished and pass these checks before acceptance. Publishing this status now exposes unfinished work as a completed, verified catalog entry; keep it outside the verified catalog until that work is complete.

File Used: CONTRIBUTING.md (source)

Knowledge Base Used:

• Lean formalization library
• Formalization project catalog

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[greptile-apps]

Duplicate public graph API

This file defines a second public graph, divisor, rank, gonality, subdivision, and tree-decomposition API for all three registered headline theorems. However, the conversions and compatibility results for the implementation API are private at lines 614–675 and 1138–1204. Users with the project’s actual _root_.CFGraph or Utilities objects therefore cannot apply these headline results without recreating the conversions and proof obligations, while maintainers must keep both public models aligned. Register the implementation-level declarations instead, or expose a supported public equivalence layer.

Knowledge Base Used:

• Lean formalization library
• Formalization project catalog

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: 18a4a87001b10658d4764ef6b1b7c89f1f82d3a5

Verdict: 🛑 request_changes — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All three registered headlines match the Lean statements, with no undisclosed theorem assumptions.
Novelty	✅ pass	Direct searches of pinned Mathlib and the existing pool found no duplicate of the Brill–Noether, marked-chain, treewidth–gonality, or subdivision-counterexample headlines.
Significance	✅ pass	The project merits pooling as a substantial, coherent development of graph divisor theory with several named research-level results.
Sources	🛑 block	The ABKS citation presents an orientability-existence result as the stronger canonical-representative theorem and needs relabelling.
Code quality (advisory)	🤔 discuss	The libraries are generally competently organized, but duplicated foundational APIs and symmetry proofs create maintenance debt worth resolving before merging.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Connectedness, the genus bound, and the Brill–Noether inequality are explicit hypotheses; the treewidth headline uses an equivalent rank-one divisor witness formulation. The auxiliary geometric obligations are discharged within the PR.
Matches cited source	🛑 mismatch
Fit	✅ good_fit
Level	research
Branch	graph theory and tropical geometry
Mode	theory_building
Code quality	3 / 5

Statement check: For connected finite loopless multigraphs, the PR proves Brill–Noether existence when ρ ≥ 0 through genus five, the treewidth lower bound for divisorial gonality, and a tricycle whose gonality falls from six to five under twofold regular subdivision.

It proves Brill–Noether existence through genus five, the treewidth lower bound for gonality, and the tricycle subdivision counterexample, supported by extensive chip-firing and transmission theory.

Sources findings (1)

• unlabelled-variant — LeanPool/BrillNoetherGraphs/Utilities/Foundations/Orientability.lean:972
  ABKS Theorem 1.2 fixes a point q and asserts existence and uniqueness of a q-orientable representative; this declaration asserts ordinary orientation existence up to linear equivalence. Labelling it Theorem 1.2 overstates which cited result is formalized. Cite Theorem 4.10 of ABKS v2, which states this finite-graph existence result, or explicitly label the weakening. Reconcile the related references at lines 14 and 151 and in Utilities/Foundations/OrientationReversal.lean:1511.
  Evidence: The diff labels the declaration /**-style Lean docstring as **ABKS Theorem 1.2.** and states: theorem orientable_of_deg_eq (h_conn : graph_connected G) (D : CFDiv G) (hDeg : deg D = genus G - 1) : Orientable G D. Its predicate is def Orientable (G : CFGraph) (D : CFDiv G) : Prop := ∃ O : CFOrientation G, linear_equiv G D (ordiv G O), with no q-orientability or uniqueness conclusion.

Code quality findings (2)

• duplicate-proof — LeanPool/BrillNoetherGraphs/Utilities/Subdivision/ClosedRowProof/ClosedAuto.lean:243
  The development from adjacency transport through classEquiv, isForest_iff, isLoopy_iff, and bnExists_iff duplicates ClosedCoreSymmetry.lean almost verbatim. LowGenus/GenusFiveClosedOrbit.lean repeats it using zeroSlots/faceSpec. These copies have separate production consumers, so changes to contraction transport require maintaining three implementations. Consolidate the common transport in ClosedCoreSymmetry and retain thin adapters for the other interfaces; importing that shared module introduces no dependency cycle.
  Evidence: ClosedAuto.lean:243 and ClosedCoreSymmetry.lean:112 both contain exactly:
  theorem rep_eq_iff (u v : Fin n) :
  compFold core (zeroSet (targetLength symmetry length)) (symmetry.vertexPerm u) =
  compFold core (zeroSet (targetLength symmetry length)) (symmetry.vertexPerm v) ↔
  compFold core (zeroSet length) u = compFold core (zeroSet length) v := by
  rw [compFold_iff, compFold_iff, reach_map_iff symmetry length]

GenusFiveClosedOrbit.lean:144 repeats this declaration and proof with zeroSlots replacing zeroSet.

• duplicate-definition — LeanPool/BrillNoetherGraphs/Highlights.lean:42
  Highlights introduces another graph type and independently copies the divisor, subdivision, and tree-decomposition vocabulary. The canonical graph already exists in ChipFiringWithLean/Basic.lean:40, and TwiceMarkedBananas.lean:81 adds TMB.CFGraph. Maintaining these representations requires extensive conversion proofs. Highlights additionally keeps its conversions and compatibility lemmas private, leaving downstream users to recreate bridges when combining headline results with implementation objects. Use canonical definitions for the public interface, or expose supported conversions and equivalences, as TMB already does with toLib/ofLib.
  Evidence: Highlights.lean:42:
  structure CFGraph where
  V : Type u
  [instDecidableEq : DecidableEq V]
  [instFintype : Fintype V]
  [instNonempty : Nonempty V]
  edges : Multiset (V × V)
  loopless : ∀ v, (v, v) ∉ edges

Highlights.lean:614:
private def libraryGraph (G : CFGraph) : root.CFGraph :=
{ V := G.V
instDecidableEq := G.instDecidableEq
instFintype := G.instFintype
instNonempty := G.instNonempty
edges := G.edges
loopless := G.loopless }

Highlights.lean:1148:
private theorem gonality_leq_library_iff (G : CFGraph) (k : ℤ) :
gonality_leq G k ↔ root.gonality_leq (libraryGraph G) k := by

---

Tokens: 5,093,637 in / 37,275 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $104.6684 (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.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 53bf84d925a59792e9b64e86182ee819cf57fffb. The protected run still fails lake exe mk_all --check because LeanPool.lean is out of date. Regenerate the index and rerun the complete required checks; the ABKS source/card wording must also match the cited orientability result.

[Vilin97]

Changes requested by automated review

Reviewed head 186d852f8582e144342676fa72ef5635bc6b3863. Genus-at-most-five Brill–Noether is partial toward the general theorem but independently significant alongside treewidth/gonality and subdivision results.

1. Complete the pinned-toolchain integration. The previous source-identical build failed at 305ddde0127cf6dab8ac0ee9be05ae2ee0fe4b02. The same source-level blocker is present at this reviewed head; its error includes:

   error: LeanPool.lean:1:0: cannot import non-`module` LeanPool.BrillNoetherGraphs from `module`
   

   The file/dependency audit finds 558 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

2. Resolve the substantive source/interface defect. The ABKS Theorem 1.2 citation concerns a unique q-orientable representative, whereas the cited Lean orientation endpoint only supplies the ordinary orientation existence statement. Correct the theorem reference/source mapping or supply the claimed stronger conclusion. Preserve the explicit genus ≤ 5 scope; do not describe this as the unrestricted Brill–Noether theorem.

Review coverage: complete changed-file inventory and full diff retained; 558 changed project files, 198,049 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Graph divisors and orientation methods; supporting overlap with #474. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

Exact-head reconciliation: the automatic main merge left all project Lean source and the pinned toolchain unchanged. This run restored the original parsed project card after the rebase parser dropped the title-first entry; parsed-card equality and the generated module-index check pass. The restoration is a narrowly scoped fast-forward commit from an isolated worktree. It does not repair the substantive blockers above; new CI is not assumed green.

[Vilin97]

Reviewed the port changes through ae8d7b2, carrying forward the earlier ABKS/genus scope review.

The declaration audit and manual review of the changed mathematical contracts found no weakened endpoint or added mathematical assumption. This includes the Demazure helper renames and choice witnesses, graph equivalences and rank constructions, the Utilities helpers, and the low-genus atlas data. The three extracted certificate trees expand to the same ordered trees with 134, 140, and 144 leaves. The 130 declarations moved into the two TwiceMarkedBananas vocabulary modules retain their names, types, and namespace/variable contexts, and remain available through the public import chain.

The subsequent formatting updates preserve executable tokens. I preserved those changes and the incoming parser repair, and fixed two trailing spaces and one extra EOF blank line. The pinned index check and diff whitespace check pass; the unchanged header, forbidden-source, file-size, and proof-size checks report no findings across all 560 project Lean files, including a recheck of the latest 26 reformatted files. The project card is unchanged.

This is a source-contract review, not a claim that every changed proof body has been kernel-checked. Full project compilation, Lean linters, and environment/axiom checks are still required at the current head. Leave this port unmerged until those checks pass.

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head 366d8cbef55076d381dfade73e655c3668693cc5. Genus-at-most-five Brill–Noether existence is independently significant beside treewidth/gonality and subdivision results; it is not unrestricted Brill–Noether existence. The ABKS source map distinguishes orientation existence from unique q-orientability, and the recovered module/certificate consolidation is retained. The complete source/dependency review and recovered repairs were reconciled through the lossless main integration; fresh protected CI remains the integration authority.

Build project: pending/not yet reported, Content / non-content separation: SUCCESS, Documentation preflight: SUCCESS. These are observed check states, not an assertion that unfinished checks passed.

The remaining authority boundary is operational: this repository has allow_auto_merge=false, and GitHub rejected enablePullRequestAutoMerge with “Auto merge is not allowed for this repository.” The maintainer must make protected queuing available through an authorized repository-setting decision, or remove this label and perform a normal squash merge after the required checks and current-base integration pass. This cycle does not change repository settings or bypass protection. No unresolved substantive author-actionable finding justifies another change request or closure; the label is not for draft status, missing profiling, or an old advisory score.

[Vilin97]

{
"reviewed_commit": "366d8cbef55076d381dfade73e655c3668693cc5",
"conclusion": "Source acceptance carries forward from review5324441246; merge remains conditional on all mandatory exact-head checks.",
"scope": "Complete131-file incoming project/umbrella delta since ae8d7b2, reconciled against the previous full source review.",
"findings": [],
"source_evidence": [
"All35 moved Farkas receipt definitions and concatenations retain their original namespaces and exact ordered data in four separate modules. Their public imports resolve without cycles.",
"The two Certificate→CertificateData type/namespace renames preserve record fields, validity predicates, Boolean checkers and soundness proofs. These are intentional public API renames; literal old-name compatibility is not claimed.",
"The remaining executable changes are496 unchanged-goal show→change replacements,47 current proof bullets,45 λ→fun replacements, and one equivalent receiver-method call. Complete whole-file reconciliation found no additional mathematical contract/data change. Full let-bearing types, equation-defined data proof fields and the leaf_sound receiver/argument context were inspected.",
"The card is byte-identical and retains the genus≤5 Brill–Noether scope. Root index adds exactly the four receipt modules. The prior faithfulness, novelty, significance and source judgments carry forward."
],
"independent_peer": "The two complete certificate/checker/soundness modules were independently reread by a second reviewer and matched modulo the disclosed rename.",
"validation": "Read-only source and import/index inventory audit; no new local compilation or pinned-generator execution. Full project compilation, Lean linters, compiled trust checks and required CI remain mandatory at this head. This review does not assert merge readiness."
}

[Vilin97]

{
"reviewed_head": "fcbcd743297b846eb32435e01fec9830672f8a28",
"verdict": "request_changes",
"scope": "Focused cross-project integration review of the public graph-divisor degree. This supplements the existing source review; it is not a new full five-axis assessment.",
"source_evidence": [
"At this head, LeanPool/BrillNoetherGraphs/ChipFiringWithLean/Basic.lean:472 publicly defines root deg : CFDiv G →+ ℤ, with value ∑ v, D v. LeanPool/BrauerGroupNew/SplittingOfCSA.lean:207 already publicly defines root deg for A : CSA k with result ℕ, using dim_is_sq.choose. These are different constants with incompatible types and meanings.",
"The merge from 366d8cb to the reviewed head leaves the complete BrillNoetherGraphs source tree, its entry module/card, SplittingOfCSA.lean, toolchain, Lake configuration and dependency manifest byte-identical. The namespace collision therefore remains present in the current source.",
"A source census finds the token deg on 1,296 non-comment lines across 164 project files. This is a lexical scope estimate, not a list of 164 files to replace mechanically: it includes the separate Highlights.deg and TMB.deg definitions and local numeric binders. Highlights also has explicit root.deg implementation bridges."
],
"validation": {
"observed_failure": "Build pool at exact prior head 366d8cb failed at LeanPool.lean:1:0 importing ChipFiringWithLean.Basic: the environment already contains deg._proof_1 from BrauerGroupNew.SplittingOfCSA. This is an actual combined-import compiler failure, not only a canceled or aggregate check.",
"failed_job": "https://github.com/Vilin97/lean-pool/actions/runs/36223244196/job/108352844071",
"current_ci": "At publication, Build pool for fcbcd74 is still in progress; no current-run failure or success is claimed.",
"current_job": "https://github.com/Vilin97/lean-pool/actions/runs/36226533988/job/108361657820",
"local": "Source and exact Git-object identity checks only; no new local compiler run."
},
"findings": [
{
"severity": "blocking",
"location": "LeanPool/BrillNoetherGraphs/ChipFiringWithLean/Basic.lean:472",
"problem": "The new public root deg conflicts with the established central-simple-algebra degree. Renaming or hiding only the generated deg._proof_1 does not resolve the incompatible root definitions.",
"requested_change": "Move the graph-divisor degree into a project-scoped public name and migrate its actual implementation consumers. Classify references semantically: redirect graph-degree calls and implementation-side bridges; preserve the independent Highlights.deg and TMB.deg statement APIs and unrelated numeric deg binders. Preserve the existing BrauerGroupNew API. Do not use a blanket token replacement across the lexical census.",
"validation_expectation": "First compile a small mixed-import regression importing both ChipFiringWithLean.Basic and BrauerGroupNew.SplittingOfCSA, checking the graph degree's finite-sum formula and the unchanged CSA degree-square theorem. Then validate migrated clients in bounded dependency batches with current-source/artifact guards, retaining headline theorem contracts and the Highlights/TMB bridges. Require fresh full integration CI before merge."
}
],
"limits": "This finding concerns namespace integration and build compatibility. It does not reverse the prior mathematical faithfulness assessment or claim a new complete quality audit. No source, gate, waiver, branch, or CI-queue change was made for this review."
}

[Vilin97]

Changes requested by automated review

Reviewed exact head d7f8f64c0a9ec3152544df9ea20a322597480b0c. The previous comprehensive source/declaration review was reconciled against this head; valid prior repairs and accurately scoped endpoints are preserved.

The genus-at-most-five Brill–Noether result is independently significant and the corrected ABKS attribution carries forward. Current whole-pool integration fails: importing BrillNoetherGraphs.ChipFiringWithLean.Basic collides with BrauerGroupNew.SplittingOfCSA at the declaration deg._proof_1 (LeanPool.lean:1). An isolated project build cannot establish coexistence.

Acceptance condition: Place the conflicting graph-divisor implementation in an appropriate project namespace and update its dependency closure, then pass the whole-pool import/build. This PR is not accepted as unrestricted Brill–Noether existence.

Protected-check snapshot: Build project: FAILURE; Content / non-content separation: SUCCESS; Documentation preflight: SUCCESS. Current CI logs and automated findings were assessed independently. This remains an author-actionable request for changes.