Import Newman normalizer bounds for congruence subgroups

[Vilin97]

This adds the real normalizer characterization of Γ₀(N) at every positive level and the generalized necessary Newman bound for ΓΔ(N). The development supplies reusable integer matrix conjugation, Atkin–Lehner elements, rational and primitive representatives, integral matrix lattices, prime valuations, and a generic normalizer argument. It complements Mathlib's congruence-subgroup definitions and Tau Ceti's modular-form infrastructure; the main results were not found in either pinned dependency or the pool.

Source and eligibility:

• Upstream: https://github.com/F-Najman/normalizer-lean/tree/ea4445c0d991a65d54fc77af0af559f2322e8660. The exact snapshot has a verified Apache-2.0 license. Filip Najman's copyright and attribution are retained. Upstream's palomar/part1/formalization.yaml explicitly credits Claude Code / Claude Opus 5.5 with the Lean proofs, following the author's mathematical blueprints; provenance is AI.
• The acquisition window is [2026-10-11T09:15:10Z, 2026-10-18T09:15:10Z). GitHub's public event records the repository becoming public on October 12 at 12:06:44 UTC; the public completed-proof snapshot is 99e6fc82ca7a364776179d7c5452cf18593acf6f, dated October 14 at 06:37:19 UTC. Eligibility rests on public release of the formalization during this window, rather than a metadata refresh or its October 18 toolchain update.
• The classical matrix description was checked against Akbaş–Singerman, Glasgow Math. J. 32 (1990), p. 317, equation (3): https://doi.org/10.1017/S001708950000940X. The source card uses this reference because the upstream's Newman 1972 citation discusses a restricted coprime-to-6 case. In the formal statement, the positive divisor and determinant equation imply the paper's exact-divisor condition. The sign accounts for lifting PSL₂ to SL₂. The ΓΔ result is explicitly a necessary bound, with no converse claimed.

Scope and port:

• The coherent production dependency closure of newman' and newman_delta': 13 source modules, a top-level entry, and the generated public Imports.lean aggregate; 15 Lean files / 2,550 lines, plus one project YAML card. The unrelated finite presentations, group orders, automorphism classifications, certificates, and comparator packaging are outside the import's claims.
• Exact pool Lean v4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e, already used by this upstream snapshot. LeanPool.lean is unchanged. The branch is based on main 929e41d.
• Added the repository headers and public namespace, reduced broad imports and unused definition dependencies, repaired documentation placement, canonical Unicode and style, replaced flexible simplification with explicit lemmas, removed dead tactic branches, and strengthened helper lemmas by removing unnecessary positivity assumptions. No endpoint was weakened and no waiver or gate was added.
• Factored the duplicated integral-entry and primitive-representative proofs into integral_products_of_normalizer and primitive_form_of_normalizer. Both the specialized and generalized results now use these reusable lemmas; the first factoring removed 185 duplicated proof lines. The Greptile follow-up factors the remaining specialized integer, local-valuation and final Newman proofs through a constructive newmanData_gamma0 package, removing a further 336 lines. The specialized theorem interfaces remain available, including the helpers without a nonzero-level assumption. Following GPT review, the local matrix lemma now takes only its six necessary valuation bounds; the caller stops deriving the unused bounds and no longer carries an inverse-matrix representative. The local conclusion is strengthened by dropping that unused hypothesis; an unused prime hypothesis in the valuation API is removed too. Nine Lean-checked counterexamples show each remaining assumption of the local matrix lemma is necessary. The generic lattice and Newman-form predicates are defined once, with specialized wrappers. Unused free-group/presentation and superseded local-lemma modules were removed from the imported closure, while the main statements and useful normalizer infrastructure are retained.

Measured compile optimization:

Measurement	Mechanical-port baseline	Final optimized import
Clean project build, wall clock	126.15 s	39.49 s
User CPU time	105.38 s	39.99 s
Lake dependency jobs	8,974	2,249

Both measurements use lake build LeanPool.CongruenceNormalizers from a fresh project .lake/build, with warm pinned Mathlib artifacts, on the same 16-vCPU Azure EPYC VM. The VM is shared, so wall-clock comparisons include scheduling noise. The final clean build is about 69% faster; the dependency reduction and CPU measurements support a real improvement. An intermediate import/simplifier cleanup measured 53.33 s before the shared-proof factoring. The final NewmanGen profile (lean --profile -DElab.async=false) measures 8.53 s wall versus 36.26 s at baseline, with typeclass inference 1.05 s versus 5.15 s. Per-file logs and raw receipts are retained in the acquisition scratch report. Earlier optimized checkpoints measured 45.88 s / 52.87 s CPU and 46.33 s / 47.76 s CPU. The final review cleanup measures 39.49 s / 39.99 s CPU. The baseline includes the upstream dependency branches removed by this optimization; both commands build the same headline results. No heartbeat or recursion override is needed.

Local validation:

• Generated public aggregate and lake exe mk_all --module --check.
• Imported-project/public-wrapper build, with no warnings.
• Mathlib/Batteries declaration linters, including slow checks; text style; repository static quality checks.
• Quality checker's permitted-axiom audit over all 181 parsed public declarations, and compiled-environment backdoor audit over all 15 owned modules, including generated declarations. Entry declarations and card synchronization checked. Only propext, Classical.choice and Quot.sound are permitted.
• Content-only diff and git diff --check; no Python code is changed.

CI remains the final authority. Greptile, the configured GPT rubric reviews, and a separate thorough source/import review must finish before protected queue admission. PR610, PR611 and PR659 are merged; applicable main Lean validation was independently observed green at ffcc8f1, whose only difference from the base is generated README statistics. Background daily documentation is not used as a merge gate. No unrelated author branch was updated and no competing PR was merged or enabled for auto-merge by this acquisition.

[Vilin97]

Thorough acquisition review for 0236932.

Conclusion: approve. This is a separate source/import review by the acquisition agent. The configured GPT rubric reviews and protected CI remain independent prerequisites for queue admission.

I reviewed the pinned upstream snapshot ea4445c0d991a65d54fc77af0af559f2322e8660, the selected module dependency closure, declaration inventories and bounded implementation slices covering every imported source, the final port/refactoring diff, the endpoint definitions/proofs, and the build/profile and trust evidence. The 15-source closure, entry point, public aggregate and YAML card are coherent. No unresolved mathematical, source, licensing, attribution, trust or maintainability finding remains.

• Faithfulness. Gamma0R is the real image of Mathlib's CongruenceSubgroup.Gamma0; Norm0 is its actual subgroup normalizer. newman_iff proves both directions for every nonzero natural level. IsNewmanForm spells out the four integer entries, positive divisor, determinant equation and sign. For n=e*m, that equation gives a*d*e - b*c*m = 1, hence gcd(e,m)=1: the paper's exact-divisor condition is present mathematically. Γ₀ contains −I, so the two SL₂ lifts agree with the source's PSL₂ formulation. newman_delta states only necessity, as the source advertises; it does not assert the generally false converse.
• Nonvacuity and abstraction. ΓΔ is defined by ordinary congruence-subgroup membership and the lower-right unit in Δ. newmanData_delta proves each generic hypothesis, including the needed unipotents, lattice divisibilities and prime-valuation witness; it does not assume the normalizer conclusion. The rationality/primitive-representative helpers now apply to arbitrary subgroups of Γ₀ containing the two specified unipotents, and the specialized/generalized public interfaces retain their original strength. The main results have no hidden postulated hard step.
• Novelty and significance. Searches of the pool registry/history/PRs and the pinned Mathlib/Tau Ceti sources found no duplicate of these endpoint results. Tau Ceti's congruence-subgroup and Atkin–Lehner scalar infrastructure is related but does not provide this normalizer classification. The result is substantive arithmetic-group mathematics with useful matrix, representative, lattice and valuation infrastructure; it fits the pool's project scope.
• Sources and provenance. Apache-2.0 is present at the pinned source; Filip Najman's attribution is retained and upstream explicitly records Claude Code / Claude Opus 5.5 proof authorship. The public-release event and completed snapshot are inside the acquisition window. The source audit corrected the card's reference to Akbaş–Singerman (1990), p. 317, equation (3), where the full matrix description can be read directly. No claim of importing all 136 upstream headline results is made.
• Engineering and cost. Every changed file was covered; no source was omitted from the review on volume grounds. The namespace is isolated, the public wrapper covers all owned files, and the change is content-only with LeanPool.lean fixed. There are no option overrides or suppressions. Broad Mathlib imports, unused definition dependencies and duplicated proof elaboration were removed. The generic proof module loses 185 duplicated lines while preserving the original special/general statements. Clean project wall time fell from 126.15 s to 45.88 s on the same shared VM, with user CPU time 105.38 s → 52.87 s; the shared scheduling limitation is disclosed.
• Local verification. Warning-free project/public-wrapper build; generated-index check; all 15 declaration linters including slow checks; text style; repository static quality; card and endpoint resolution; permitted-axiom audit of 200 parsed public declarations; and compiled-environment audit of all 17 owned modules including generated declarations all passed. No sorry, extra axiom, unsafe/partial/native-decide mechanism or option backdoor is admitted. No Python source changed.

CI and automated review status will be checked on this exact head before any protected queue action. This comment does not substitute for those checks or GitHub's normal protections.

[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 impact] No blocking code issue was found; external source and dependency prior-art checks remain unverified.

Summary

Adds the real normalizer characterization for Γ₀(N) and a necessary Newman bound for Γ_Δ(N).

• Every Γ₀(N) normalizer has exactly a Newman matrix form.
• Every Γ_Δ(N) normalizer must fit a Newman matrix bound.

_{Reviews (4) · Last reviewed commit: "Eliminate the redundant inverse valuatio..." · Reviewed by Greptile}

[Vilin97]

Thorough acquisition review update for 4a18a28.

Conclusion: approve. The full source/import findings in the initial review still apply. I inspected the complete three-file follow-up diff and the resulting dependency graph and theorem interfaces. The generic module now depends on valuation infrastructure rather than the specialized result, and newmanData_gamma0 constructively discharges every hypothesis for Γ₀(N). The N=0 case is covered for the helper interfaces that never required nonzero level. The specialized divisibility, local-valuation and final normalizer proofs are direct instances of the generic argument; endpoint statements and generality are unchanged. This resolves Greptile's duplicated-long-proof finding without suppressions or weakened assumptions.

Validation on this exact source: warning-free project/public-wrapper build; generated-index check; all declaration linters including slow checks; text style; full repository static quality; permitted-axiom audit of 201 public declarations; compiled-environment audit of 17 modules including generated declarations; entry/card checks; and whitespace/content-only checks all pass. The final import has 17 Lean files / 2,862 lines plus its YAML card. No unrelated source or infrastructure changed.

The post-review clean project build measured 46.33 s wall / 47.76 s user CPU, against 126.15 s / 105.38 s for the mechanical-port baseline, with warm pinned dependencies on the same shared VM. The generic module's controlled profile measured 12.46 s wall, down from 36.26 s; typeclass inference fell from 5.15 s to 1.25 s. The remaining arithmetic and matrix proof cost has no identified material safe cleanup after these passes.

The old head and its receipts are preserved. Protected CI, the refreshed Greptile review and configured GPT rubrics must still complete on the current head before any queue action. Auto-merge remains off.

[Vilin97]

{
"review_kind": "independent_source_review",
"head_sha": "4a18a2843fe7d3c012961acdab6a0545e9fee88b",
"verdict": "approve",
"fit": "good_fit",
"level": "research",
"branch": "modular forms and arithmetic groups",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 4,
"summary": "The complete 18-path import provides a substantive normalizer classification and a separately labelled necessary bound for congruence subgroups. I read all 17 Lean files and the card, traced the actual subgroup definitions and both endpoint proofs, and independently checked the cited matrix formulation. The constructive NewmanData instances feed a shared rationality, lattice and valuation argument; the specialized wrappers retain their original generality. No correction is needed in the reviewed source.",
"faithfulness": "Gamma0R is the image of Mathlib's Gamma0 and Norm0 is its actual normalizer. The iff includes conjugation sufficiency as well as necessity. Positive e, e|n and the determinant equation imply the paper's exact-divisor condition; the sign gives both SL2 lifts. GammaDelta's bound asserts no converse, and all generic hypotheses are proved for the concrete groups.",
"sources": "The matrix formulation matches Akbas–Singerman (1990), p.317, equation(3). The Delta result is explicitly a generalization with only necessity claimed. The pinned Apache-2.0 upstream, author attribution and AI proof provenance are preserved.",
"source_reference": "https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B41A708751217817383FEB6D25D6FC4F/S001708950000940Xa.pdf/the-normalizer-of-g0n-in-psl2.pdf",
"novelty_note": "The inspected pinned Mathlib and Tau Ceti congruence/Atkin–Lehner APIs provide supporting definitions and special matrix results, rather than these arbitrary-real-normalizer endpoints. No duplicate headline was identified in that comparison or the pool.",
"significance": "The all-positive-level Gamma0 characterization and arbitrary-Delta necessary bound form a coherent research-level arithmetic-group development with reusable matrix, primitive-representative and valuation infrastructure.",
"findings": [],
"validation_scope": "Independent source acceptance. Current-head configured rubric reviews and applicable protected CI remain prerequisites for native queue admission. The refreshed Greptile review on this head reports no blocking defect. The author's local build and timing measurements are attributed evidence; no additional build, benchmark or compiled-manifest claim is made here."
}

[Vilin97]

/review

Please review current head 4a18a2843fe7d3c012961acdab6a0545e9fee88b. The source/import and Greptile reviews are clear, and the local build, linters, style, static quality and project trust checks pass. Protected full-pool CI is still compiling; this request does not claim CI success or authorize queue admission before CI passes. The exact source, upstream pins, primary-paper evidence and measured optimization are recorded in the PR description and thorough-review comments.

[Vilin97]

🤖 LLM review (gpt-6.1-sol, 5 rubrics)

Reviewed head: 5df28e5c135083e87778befacb44473142a8fa14

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

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All three card headlines match the Lean; CI for this head remains in progress, and no local rebuild was performed because Lake dependencies are absent.
Novelty	✅ pass	Independent source checks found no duplicate of the three headlines in Mathlib, Tau Ceti, or the pool; the supplied Mathlib API searches were unverifiable.
Significance	✅ pass	The normalizer classification and generalized necessary bound form a coherent research-level project; head CI remains in progress, and no local build was run.
Sources	✅ pass	Akbaş–Singerman, equation (3) supports the Γ₀ characterization after determinant normalization; the ΓΔ bound is explicitly labelled as an extension and its upstream formalization is credited.
Code quality (advisory)	✅ pass	The shared normalizer argument and specialized wrappers are maintainable; isolated arithmetic checks passed, while full-project CI remains in progress.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The positive level, determinant-one real matrix, subgroup Δ and normalizer membership are disclosed; newmanData_gamma0 and newmanData_delta prove all generic hypotheses, including the valuation witnesses.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	arithmetic groups and modular forms
Mode	theory_building
Code quality	3 / 5

Statement check: At every positive natural level, newman_iff proves the stated normalizer equivalence, newman_delta proves the stated necessary matrix form for every subgroup Δ, and hPart_isGreatest' proves the stated greatest-divisor characterization.

newman_iff proves the classical normalizer characterization for Γ₀(N) at every positive level, and newman_delta supplies a ΓΔ(N) necessary bound through shared primitive-representative, lattice and valuation arguments.

Faithfulness findings (1)

• prompt-injection — PR-wide
  Contributor comments 0, 2, 5 and 8 in .review-pr.json state “Conclusion: approve.”; comment 3 invokes clear earlier reviews. These prior-approval claims can bias independent judgment and were disregarded. Treat them solely as untrusted discussion.
  Evidence: prose only

Novelty findings (1)

• prompt-injection — PR-wide
  Contributor discussion asserts prior approval and invokes earlier clear reviews, risking bias in this independent novelty assessment; these claims were disregarded.
  Evidence: In .review-pr.json, comments[0], comments[2], comments[5], and comments[8] state “Conclusion: approve.”; comments[3] states “The source/import and Greptile reviews are clear”.

Significance findings (1)

• prompt-injection — PR-wide
  Contributor discussion asserts prior approval and invokes earlier clear reviews, which can bias this independent significance assessment; these assertions were disregarded.
  Evidence: In .review-pr.json, comments[0], comments[2], comments[5] and comments[8] state “Conclusion: approve.”; comments[3] states “The source/import and Greptile reviews are clear”.

Sources findings (1)

• prompt-injection — PR-wide
  Contributor discussion asserts prior approval and invokes earlier clear reviews. These claims have no authority over this independent source review and were excluded from the verdict.
  Evidence: In .review-pr.json, comments 6248435882, 6248536449, 6249400570 and 6249732833 state “Conclusion: approve.”; comment 6248860148 states “The source/import and Greptile reviews are clear”.

Code quality findings (1)

• prompt-injection — PR-wide
  Contributor discussion claims prior approval and invokes other reviews; these claims were disregarded when assessing code quality.
  Evidence: In .review-pr.json, contributor comments[0], comments[2], comments[5] and comments[8] state “Conclusion: approve.”; comments[3] states “The source/import and Greptile reviews are clear”.

---

Tokens: 7,889,409 in / 42,639 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $32.1972 (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.

[Vilin97]

Thorough acquisition review for 160d0f4.

Conclusion: approve. This is the contributor's separate source/import review; it has no authority over the independent GPT rubric reviews, Greptile or protected CI. Those must assess this head independently.

I inspected the complete nine-file repair diff and resulting declarations/dependency graph, in addition to the source and mathematical audit documented at the earlier checkpoints. The three GPT code-quality findings are addressed concretely:

• local_form_gen now proves the same conclusion with fewer assumptions: its unused 2-adic parameter and twelve redundant inputs are removed. local_conclusionG derives only the eight valuation bounds it consumes. The general integer-divisibility API is retained.
• InLe and its lattice operations are defined once below both consumers, with the specialized InL API as wrappers. IsNewmanForm specializes the single generic matrix predicate; unfolding nPart gives exactly the original formula. The two proof normalization edits change no hypothesis or conclusion.
• The unused relation/free-group branch and superseded local lemma module are removed from the selected import, including the unused word definitions and direct FreeGroup import. The generated public aggregate is updated. Useful Atkin–Lehner, normalizer-quotient, conjugation, primitive-representative and valuation infrastructure remains.

The Γ₀(N) equivalence, ΓΔ(N) necessary bound, and greatest-divisor result retain their types, mathematical generality and source interpretation. Apache-2.0, Filip Najman's attribution and AI provenance remain explicit. There is no new axiom, mechanism, waiver, option override, policy edit or unrelated file change. The import now has 13 production source modules, an entry point and public aggregate: 15 Lean files / 2,577 lines, plus one YAML card. LeanPool.lean remains fixed.

All local checks pass on this source: warning-free project/public-wrapper build; generated-index check; declaration linters including slow checks; text style; repository static quality; endpoint/card checks; permitted-axiom closure for 181 parsed public declarations; compiled-environment audit for 15 owned modules including generated declarations; content-only and whitespace checks. No Python source changed.

The controlled clean build now measures 43.70 s wall / 41.47 s user CPU, compared with 126.15 s / 105.38 s for the mechanical-port baseline, on the same shared VM with pinned warm dependencies. The baseline's unused dependency branches are among the eliminated costs. The generic module's profile is 10.33 s wall, typechecking 1.03 s, typeclass inference 1.15 s, compared with 36.26 s / 3.48 s / 5.15 s at baseline. The shared-VM scheduling limitation remains disclosed. No further material safe optimization is identified after the import, shared-proof and review-driven passes.

No mathematical, source, trust, attribution or maintainability issue remains in this review. Fresh protected CI, Greptile and GPT results on this head remain mandatory before queue admission; earlier head results do not substitute for them.

[Vilin97]

/review

[Vilin97]

{
"review_kind": "independent_source_review",
"head_sha": "160d0f465057e7805b2c47314206affc110fd7c2",
"verdict": "approve",
"fit": "good_fit",
"level": "research",
"branch": "arithmetic groups and modular forms",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 4,
"summary": "Renewed source acceptance at this exact head after the complete seven-modification/two-deletion delta review. All 16 current paths and both deleted source bodies were authenticated against accepted 4a18a28. The three historical maintenance findings are addressed in actual code: the valuation interface is smaller, the lattice and Newman-form APIs share their implementations, and an unconsumed auxiliary branch is removed.",
"faithfulness": "The positive-level real normalizer equivalence for Gamma0(N), the necessary generalized GammaDelta(N) matrix form and the characterization of h(N) as the greatest divisor of 24 whose square divides N are preserved. The generic NewmanData structure and its actual Gamma0/GammaDelta constructors remain intact; the required matrix, primitivity, divisibility and valuation facts are derived rather than postulated as the desired conclusion. No GammaDelta converse is claimed.",
"valuation_producer": "local_form_gen has the same two-branch conclusion with twelve unnecessary premises and the e2 parameter removed. Its remaining eight valuation bounds are supplied by local_conclusionG through the actual matrix/inverse/gamma witnesses and ultrametric facts. The generic final theorem and specialized main mathematical tail are unchanged.",
"predicate_and_API_review": "InLe is defined once below both consumers, with the specialized InL operation contracts retained as direct wrappers. IsNewmanForm transparently specializes the unchanged IsNewmanFormH formula at hPart; unfolding nPart gives the original signed square-root-scaled integral matrix equation. The explicit normalizations in T1General change no mathematical premise. The deleted NewmanLocal and RelBasic modules contain auxiliary public declarations that have no retained production consumers; this is an intentional auxiliary API reduction, and a blanket preservation of every public name is not claimed.",
"sources": "The unchanged card accurately credits F-Najman/normalizer-lean at ea4445c0d991a65d54fc77af0af559f2322e8660, Apache-2.0 attribution and explicit AI provenance. The Gamma0 description remains aligned with Akbas-Singerman, Glasgow Mathematical Journal 32 (1990), page 317, equation (3): the determinant equation together with e dividing n implies exact divisibility, and the sign accounts for the SL2 lift.",
"source_reference": "https://doi.org/10.1017/S001708950000940X",
"novelty_and_significance": "The unchanged headlines retain the prior primary-source and bounded pinned Mathlib/Tau Ceti/pool assessment. A complete normalizer classification and its constructive generalized necessary bound are a substantive research-level contribution, supported by reusable matrix, lattice and prime-valuation arguments.",
"engineering": "The 15-module internal import graph resolves without cycles, the entry and card are unchanged, and the specialized useful interfaces remain public. Protected configuration and shared roots are untouched. Historical quality-DISCUSS findings were evaluated against the current source; the older configured verdict is not represented as current approval.",
"prior_complete_source_review": "#676 (review)",
"findings": [],
"validation_scope": "Independent source acceptance at 160d0f4 only. Current own CI, refreshed Greptile assessment, current configured rubric result and protected integration remain prerequisites. The existing current /review request6249400721 is preserved. Contributor approval, local build, trust-audit and timing statements remain attributed evidence; I started no additional compiler or benchmark and transferred no old-head CI result."
}

[Vilin97]

/review

[Vilin97]

Thorough acquisition review update for 5df28e5.

Conclusion: approve. This is the contributor's source/import review, not authority for the independent GPT review or protected CI.

I inspected the complete three-file follow-up diff. The second GPT quality review's remaining code finding is addressed: local_form_gen drops u2, C17 and C18; local_conclusionG and its specialized wrapper require no inverse representative; the unused inverse-derived integer facts/valuations and the inverse-matrix proof in newmanG are removed. The valuation API also drops its unused prime hypothesis. These helpers have fewer assumptions; the three advertised endpoint statements and their generality are unchanged.

To check the reduced local lemma thoroughly, I constructed and Lean-checked nine independent counterexamples. Each tuple below satisfies every remaining input except the named one, and falsifies the unchanged conclusion. Thus no remaining input can simply be deleted, singly or as part of a larger deletion. The tuple order is (ν, j, k, δ₀, a, b, c, d); natural subtraction has Lean's ordinary truncated meaning.

Omitted input	Counterexample tuple
hk	(10, 0, 20, 6, 3, 30, 0, 3)
prim	(10, 0, 0, 4, 2, 10, 12, 2)
u1	(10, 0, 0, 6, 6, 0, 13, 3)
C2	(10, 0, 0, 20, 0, 20, 20, 20)
C3	(10, 0, 0, 20, 20, 20, 0, 30)
C6	(10, 0, 0, 20, 20, 0, 20, 20)
C7	(10, 0, 0, 20, 20, 20, 40, 0)
C10	(10, 0, 0, 6, 3, 0, 13, 3)
C11	(10, 0, 0, 10, 10, 0, 10, 5)

All local validation passes on this source: warning-free project/public-wrapper build; generated-index check; declaration linters including slow checks; text style; full repository static quality; permitted-axiom audit of 181 parsed public declarations; compiled-environment audit of 15 owned modules including generated declarations; endpoint/card checks; content-only and whitespace checks. The import contains 15 Lean files / 2,550 lines plus its single YAML card. No gate, option or waiver changed.

The controlled clean build measures 39.49 s wall / 39.99 s user CPU, against 126.15 s / 105.38 s baseline with the same pinned warm dependencies on the shared VM. The generic module's controlled profile is 8.53 s wall / 7.06 s user CPU, typechecking 0.696 s and typeclass inference 1.05 s, versus baseline 36.26 s / 15.94 s, 3.48 s and 5.15 s. The baseline's unused dependencies and duplicated proof work are among the eliminated costs. Shared scheduling noise remains disclosed.

The earlier full-pool green CI checkpoint is preserved. Fresh CI, Greptile and all GPT rubric results are still required on this exact head before any normal queue entry. No current-head CI or automated approval is inferred from the earlier checkpoint.

[Vilin97]

{
"review_kind": "independent_source_review",
"head_sha": "5df28e5c135083e87778befacb44473142a8fa14",
"verdict": "approve",
"fit": "good_fit",
"level": "research",
"branch": "arithmetic groups and modular forms",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 4,
"summary": "Renewed source acceptance of the exact published three-file repair. All 16 current paths are authenticated; thirteen bodies are literally unchanged from accepted 160d. The current code resolves the additional finite maintenance finding in configured review 2189 without changing any of the three headline contracts.",
"faithfulness": "The positive-level real normalizer equivalence for Gamma0(N), the necessary generalized GammaDelta(N) matrix form and the greatest divisor of 24 whose square divides N retain their statements and generality. NewmanData and its constructive Gamma0/GammaDelta providers are unchanged; no GammaDelta converse or new conclusion-shaped assumption is introduced.",
"maintenance_and_API": "local_form_gen retains its two-branch conclusion with u2,C17,C18 removed. local_conclusionG uses the actual forward matrix/gamma valuation suppliers and no inverse representative; the unused inverse integer-fact, valuation and newmanG representative calculations are gone. The specialized local wrapper is strengthened consistently, and the unused prime premise is removed from vz_eq_zero_of_not_dvd. Four auxiliary public Types intentionally have fewer explicit premises; all current callers are updated. This is not a claim that every former helper application is literally unchanged.",
"independent_math_check": "I independently examined the arithmetic reduction and kernel-checked the exact current local_form_gen command at Lean 4.35.0-rc3 in isolation. Its only axioms are propext, Classical.choice, Quot.sound. This validates that strengthened lemma; it is not a full-project or hosted-CI certificate.",
"source_and_scope": "The card, entry, aggregate imports, licensing, attribution and explicit AI provenance are unchanged. The retained primary-source assessment of F-Najman/normalizer-lean at ea4445c0d991a65d54fc77af0af559f2322e8660 and Akbas-Singerman (1990), p. 317, equation (3) applies to the unchanged headline contracts. The determinant/exact-divisor argument and real SL2 sign interpretation remain intact.",
"source_reference": "https://doi.org/10.1017/S001708950000940X",
"novelty_and_significance": "The complete normalizer classification and constructive generalized necessary bound retain the prior independent pinned Mathlib/Tau Ceti/pool comparison and research-level significance. No mathematical scope was dropped by this cleanup.",
"engineering": "The actual first-projection use of ultra_vv supplies the same retained lower bound, and the module prose correctly describes the strengthened wrappers. No import, option, quality gate or protected configuration changed. The current 15-module source graph and its entry/card remain coherent.",
"prior_complete_source_review": "#676 (review)",
"findings": [],
"validation_scope": "Source approval only at 5df28e5. Current hosted CI, current configured rubrics and normal protected integration remain independent requirements. Current Greptile is nonblocking but did not independently verify external prior art; that assessment is covered separately by the retained primary Source work. Existing request 6249724769 is preserved; the old 2189 result is historical after the head change. Contributor timing, full-build and nine-counterexample claims remain attributed; I did not replay the owner's build or benchmark. A concurrent-author guard stopped my private repair preparation before any Git object, branch or public mutation, preserving the author's actual repair."
}