WIP: import Markoff mod p

[Vilin97]

Imports the complete Yuma Mizuno Markoff-mod-p development, including explicit strong approximation, orbit theory, curve point counts, and the supporting function-field and Riemann–Roch proofs. All 609 production source modules are retained, with the pool entry module making 610 files. Source attribution includes Yuma Mizuno and Guanghao Li.

The Lean/Mathlib 4.34.0 port preserves the main statements, exposes the data and helper interfaces required by Lean's module system, generalizes unused enumeration assumptions to finiteness, and factors the normal-closure Hasse–Weil argument through a compatible abstract Galois tower. It also corrects the local-monogenicity source citation and labels the formalized generalization.

At current head 3dac82b815734a04dc47075602a3a92c1649749a, all 610 files pass static header, forbidden-text, file-size and proof-size checks. The bounded target157 run compiled cage-axis equivalence and the concrete Hasse–Weil theorem, then finished with exactly two failing modules: cage connectivity and descended irreducibility. Their private proof/type aliases are now replaced by an existing public proof and the same underlying field terms. The assembly reuses that proof as well, and 38 further compiler-recommended section-variable omissions are applied. A bounded full-project build162 is queued at this head.

This is still an incomplete port: the full project build, zero-warning requirement, scoped declaration linters, compiled axiom/environment audit, and refreshed independent review remain outstanding. The latest hosted CI failures are recorded; none is treated as a pass. The independent review's older source-citation finding has been addressed, while its advisory duplication findings still need assessment.

Main was integrated by an ordinary merge; the owned project sources, entry module, registry card, and toolchain pins were preserved.

Part of the requested 42-project import batch. Do not merge.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Changes requested by automated review

Reviewed exact head 35ab82180c9cd886a2b09ed568feb9f2806d9eb7. The exact-head MarkoffModP build fails in ExactConstantExtensionNormalClosureTower.lean with stuck typeclass synthesis, deterministic heartbeat timeouts, and resulting unsolved goals. Repair the failing closure and obtain warning-free full CI at the new head.

[Vilin97]

/review

[Vilin97]

{
"reviewed_head": "e3a9026cb9b3ebad3e0f94befdac60bcba8f25a3",
"review_scope": "Local-monogenicity source documentation and supporting authorship only.",
"source_assessment": "The paper is Balçık, Chan, Liu and Viray, Number fields generated by points in linear systems on curves. Lemma 3.1 in https://arxiv.org/html/2503.07846v2 assumes both rings regular local. The Lean theorem uses integrally closed local R and local UFD S, together with its finite faithful extension and etale height-one quotient assumptions. The overview, result list and theorem docstring now explicitly label that independently proved broader statement a generalization. No theorem type or proof was changed.",
"authorship": "Added Guanghao Li to the registry and generated card, matching the imported RiemannRoch/Basic and RiemannRoch/RRspace/Basic authorship headers.",
"validation": "Confirmed the repair changes no executable Lean text; scoped registry/card checks passed. Lossless main integration preserves all 218 cards from 99afd29 and adds only this project. The old normal-closure elaboration failure has been repaired in the importer, with a successful targeted build; that result had warnings and is not current-head full certification.",
"remaining_work": "The importer has a newer unpublished module-system checkpoint and active compiler-frontier repairs. Full current-head build, warning-free linters, quality/axiom/environment audits and final integration review remain pending. Its dirty worktree was not modified by this patch.",
"merge_approval": false,
"disposition": "The specific citation/generalization and supporting-credit findings are repaired. This scope-limited source review is not approval to merge the unfinished port."
}

[Vilin97]

Reviewed the 80-file incoming delta 3640b4b31b70c9ff67eeb1f792336dc957a8dfc9 → eff45ff7477b05fb37f5b109baa1a76cb5ee69bb. The refactoring preserves the mathematical results; full port validation is still required before merge.

The Hasse–Weil argument now separates a generic exact-constant Galois-tower estimate from the normal-closure construction. Two reviewers checked the construction adapters and count-transport identities: the field/algebra maps, genus/degree constants, extension exponent and public error-bound statement are retained. The other changes remove unused hypotheses, generalize enumeration assumptions from Fintype to Finite, and repair proof/style elaboration. The quotient-fiber counting results retain their stabilizer-surjectivity hypothesis; no conclusion is weakened. Two overlong Wronskian helper names are normalized with no old-name references left in the project.

All 80 changed files were covered by the source review. At this exact head, the unchanged header, forbidden-text, file-size and proof-size checks pass across all 610 project files; the pinned generated-index and delta whitespace checks also pass. No fresh full-project compilation, lint or environment-audit pass is claimed. Keep the PR unmerged until the remaining compiler work and complete validation finish.

[Vilin97]

Source-review carry-forward on 3dac82b815734a04dc47075602a3a92c1649749a, comparing the 54 incoming project files with previously reviewed eff45ff7477b05fb37f5b109baa1a76cb5ee69bb (previous review). The complete incoming source comparison is acceptable; the independent review covered the 18 constant-extension/normal-closure files alongside the other 36 files.

• Omitted section assumptions preserve the existing conclusions. The two restored IsDomain A premises are already implied by the statements' explicit IsDedekindDomain A assumption. Full affected types, including type-level algebra/instance choices, were inspected.
• The Stepanov and finite-place Fintype → Finite changes select enumerations locally with Fintype.ofFinite; the linear-independence, residue-field and maximality statements retain their substantive hypotheses and conclusions.
• The exported canonical-different alias and coordinate equivalences retain their defining values and all match branches. The reconstruction/integrality helpers retain their proofs. Local field notation denotes the same field constructors.
• The shared nonzero-three helper has exactly the same statement and proof as all four previous copies. Its use inside letI inverse instances preserves the mathematical contracts. All other incoming executable changes were accounted for by these reviewed transformations.

The 610-file project inventory and exact project-card bytes are preserved. This carries forward source acceptance only: fresh full compilation, linters, compiled axiom/trust checks and required CI remain necessary, including confirmation of the inferred declaration interfaces after the module port. It does not establish merge readiness. No new local build was launched for this review.

[Vilin97]

Changes requested by automated review

Reviewed 3dac82b815734a04dc47075602a3a92c1649749a. The sufficiently-large-prime Markoff transitivity result is a substantial completed target, with integer lifting separate from the modular orbit statement.

Blocking finding: NonparabolicComplementFrontier.lean:194 cannot resolve normalizedPuncturedPointNonparabolicComplement; ExplicitPuncturedTransitivity.lean:71 cannot resolve normalizedPuncturedPoint. CoarseSupportTail.lean:42,57 also exceeds the recursion limit. Restore the correct namespace/import dependencies and restructure the failing elaboration without a limit override, then rebuild all endpoint dependencies.

Evidence: exact-head build log. Acceptance condition: the complete project, repository quality/axiom gates and required protected checks pass on the repaired head, and the remaining substantive/maintainability findings are resolved. The prior bot verdict does not override these reproduced source/build failures.

[Vilin97]

Changes requested by automated review

Reconciled to exact current head 7e79885976638469ca8f9094defd27ba17a284f6. The main-branch integration leaves this project’s Lean sources byte-identical to the reviewed source; the existing substantive findings and acceptance conditions remain unresolved. The missing normalized punctured-point definitions and CoarseSupportTail elaboration failures still prevent the Markoff theorem closure from compiling.

Preserve the valid completed repairs. Merge requires the cited author-actionable defects to be resolved and all protected checks to pass at the resulting head; this is not a needs-maintainer handoff.

[Vilin97]

{
"reviewed_commit": "88235424dacace8f91484c3bf1cff5d5d1138124",
"base_commit": "5ebcced2e4ee3d5b112ce7e88f0509ab045ad85d",
"scope": "Focused repair of the four compiler errors in CoarseSupportTail, ExplicitPuncturedTransitivity and NonparabolicComplementFrontier. Existing project assessments and Do not merge hold remain.",
"conclusion": "The two support-margin proofs now elaborate their intermediate inequalities separately. The two public frontier hypotheses use the exact public normalization composition underlying their private aliases.",
"problem": {
"job": "https://github.com/Vilin97/lean-pool/actions/runs/36226854948/job/108362840209",
"errors": "Two calc proofs exceed recursion depth; two public hlarge types refer to private normalization helpers."
},
"changes": [
"The support margins keep exactly 68^15 * 2^1374 < 2^1512 and 100522^10 * 2^916 < 2^2268. Named product inequalities, exponent identities and strict power monotonicity compose the same bounds without the failing calc block.",
"Each affected hlarge argument expands its existing private helper to normalizedSurfaceOfPunctured (puncturedNormalizationEquiv (ZMod p) c). All hypotheses, thresholds and conclusions are preserved up to this definitional expansion; helper declarations and both theorem proof bodies are unchanged."
],
"validation": [
"Independent source reviews checked both complete numerical statements/proofs and both public hypothesis expansions.",
"Exact final extracts of both numerical proofs compile warning-free at the pinned Lean/Mathlib versions with unchanged project options, two Lean threads and an 8 GiB limit. Their two exact axiom reports contain only Classical.choice, Quot.sound and propext.",
"The four unchanged scoped source-quality checks and git diff --check pass. Only these three files changed; all other tracked files, cards, indexes and configuration are retained."
],
"limitations": "The numerical test imports Mathlib and does not compile the full project modules or the two visibility repairs. Fresh exact-head required CI, full warning cleanup and the outstanding project audits remain necessary; the preceding build reported 515 project warning headers. The author\u2019s Do not merge instruction is preserved."
}

[Vilin97]

{
"reviewed_commit": "51fb19ac0f57847d6ae960d16934f681018e8e5d",
"conclusion": "The bounded public-type visibility repair passes source review and scoped static checks. Full acceptance remains pending: clean up the remaining warnings and run fresh exact-head CI. Keep the existing Do not merge hold.",
"scope": {
"baseline": "88235424dacace8f91484c3bf1cff5d5d1138124",
"files": [
"LeanPool/MarkoffModP/BGS/Markoff/Assembly/EulerSevenNonparabolicComplementFrontier.lean",
"LeanPool/MarkoffModP/BGS/Markoff/Assembly/ExactOrderComplementObstruction.lean",
"LeanPool/MarkoffModP/BGS/Markoff/Assembly/ExactOrderEulerSevenComplementObstruction.lean",
"LeanPool/MarkoffModP/BGS/Markoff/Assembly/MaximalDivisorPuncturedTransitivity.lean"
],
"change": "Six public hlarge hypothesis occurrences expand their existing private normalized-point alias at ZMod p. This covers four actual diagnostics in three modules and two identical public-header cases found in downstream ExactOrderEulerSevenComplementObstruction."
},
"source_review": {
"preserved": "Each replacement is exactly normalizedSurfaceOfPunctured (puncturedNormalizationEquiv (ZMod p) c), the existing private alias body. All field/Invertible hypotheses, threshold p^(5/6), arithmetic bounds, sign/divisibility assumptions, same-component predicates and conclusions remain unchanged. The exact-order/Euler-seven theorem still produces one common d for both bounds.",
"implementation": "All private aliases and proof bodies are unchanged. No public helper was added and no assumption was weakened. Parent independent review covered the full six-site diff and complete affected types.",
"census": "All 610 project files were scanned. After the patch, zero normalizedPuncturedPoint-prefixed references remain in public declaration headers; all 154 other tokens (11 declaration names, 10 private-header references, 133 proof/definition-body references) are unchanged."
},
"validation": {
"static": "The existing scoped header, forbidden-text, file-size and proof-size gates pass on all four changed modules; git diff --check passes. The other 606 project files, complete inventory, registry/card, root index/umbrella, imports, configurations and gates remain byte-identical. Own generated card matches registry.",
"prior_ci": "The exact baseline CI compiled the prior CoarseSupportTail, ExplicitPuncturedTransitivity and NonparabolicComplementFrontier repairs before reaching these new visibility failures. Existing warnings remain in the first two modules.",
"prior_ci_url": "https://github.com/Vilin97/lean-pool/actions/runs/36232080939/job/108377029385",
"limits": "No local compilation, native generator/style/linter or compiled-trust check was run for this new patch. This is a source/static-only follow-up, not full project approval."
},
"remaining_requested_changes": [
"Resolve the baseline run\u2019s 512 warning headers across 126 modules using code fixes; preserve existing gates and proof budgets. This broader warning cleanup is not claimed fixed by the six header expansions.",
"Run fresh exact-head compilation, declaration/style checks, compiled trust audits and required CI; confirm the four reported failures and the two downstream cases are resolved."
],
"lifecycle": "PR body/draft/provenance and Do not merge hold preserved. Normal guarded source push and this focused COMMENT only; no main refresh, merge, manifest or CI queue action."
}

[Vilin97]

{
"reviewed_commit": "ca3684d188b232efcea5434d8d7d554f626270db",
"conclusion": "Focused source/static repair accepted; full compilation and acceptance remain pending. Preserve the existing Do not merge hold.",
"scope": {
"baseline": "51fb19ac0f57847d6ae960d16934f681018e8e5d",
"file": "LeanPool/MarkoffModP/BGS/Markoff/Assembly/JointMaximalDivisorFrontier.lean",
"change": "Expand the exact private jointNormalizedPuncturedPoint alias at the two public hlarge occurrences, retaining the private definition and all proof bodies. No new five-rubric or full-project approval is claimed."
},
"source_evidence": {
"declarations": [
"puncturedMarkoffTransitiveAt_of_jointSquareEnvelope_frontier",
"puncturedMarkoffTransitiveAt_of_jointMaximalDivisorBounds"
],
"same_point": "jointNormalizedPuncturedPoint c unfolds exactly to normalizedSurfaceOfPunctured (puncturedNormalizationEquiv (ZMod p) c). Prime-field and Invertible 3 hypotheses, the distinguished point, square-envelope/central/product bounds, safe coefficients, exponents and PuncturedMarkoffTransitiveAt conclusions are unchanged.",
"coverage": "The widened census scanned all 610 project files, including case-insensitive and prefixed alias names. A semantic definition-body search across the 15 files mentioning normalizedSurfaceOfPunctured found seven private point aliases and no differently named additional alias of this form. These were the only two remaining public-header uses in that narrow family. This is not a general visibility audit.",
"review": "Complete 154-line module, exact alias body, both full statements and proofs source-reviewed; inverse replacement reconstructs the entire baseline file."
},
"validation": {
"earlier_six_header_repairs": "At baseline 51fb19a, all four previously repaired modules compiled: ExactOrderComplementObstruction, EulerSevenNonparabolicComplementFrontier and ExactOrderEulerSevenComplementObstruction reported clean Built entries; MaximalDivisorPuncturedTransitivity built with an existing Try-this warning.",
"new_failure": "That same run emitted two real compiler errors at JointMaximalDivisorFrontier.lean:100 and 140, both rejecting the private point alias in a public header. The runner later received a shutdown signal and exited 143. The run therefore does not establish a completed full build or a complete remaining-error frontier.",
"ci_evidence": "https://github.com/Vilin97/lean-pool/actions/runs/36234185221/job/108382889168",
"static": "The existing header, forbidden-text, file-size and proof-size checks pass on the complete changed module; all lines satisfy the 100-character bound and git diff --check passes. The other 609 project files, all proof bodies, registry/card, root index/umbrella, imports and configurations are byte-identical. The own generated card matches the registry.",
"census_after": "The two independently classified public-header tokens are removed; all other census bytes are unchanged, leaving zero public-header uses in this alias family.",
"compiled": "No local compiler, native style/linter, generator or compiled-trust run was performed for this new two-line repair. Fresh exact-head CI must confirm it.",
"existing_warning_request": "The warning-cleanup request in review 5325532476 remains in force; this follow-up does not repeat it as a new finding. The observed log has 515 warning headers (413 distinct location/message tuples across 128 modules). Full warning-free compilation, lint and compiled-trust checks remain pending.",
"prior_review": "#502 (review)"
},
"lifecycle": "The body still says Do not merge. No main refresh, merge, compiler/cache expansion, CI retry/cancellation, label, manifest or gate change was performed."
}