[Vilin97]

QuantumQuery's roughly 24,000 lines contain expensive finite-sum proofs and scalar endgames inside large quantum-algorithm contexts. This changes 19 existing proof bodies across four modules and reduces the measured project-clean build median from 73.430 s to 65.057 s (11.40%) on the Azure VM.

The changes use Matrix.single_mulVec instead of re-expanding matrix sums, explicit simplification for block-diagonal embeddings and finite cardinalities, Bool.eq_not_of_ne instead of Boolean case searches, positive-factor cancellation for spectral lower bounds, and the existing orNDelta_sq identity instead of unfolding nested square roots. The square-root cross-term and algorithm-extraction arguments retain their mathematical steps while restricting arithmetic to the facts needed at each step. Matrix-product reassociation uses explicit associativity.

The measured base is 66f6943c594e459c4d2bd2901d66f6f6ab677f8b; the head is fdf917b00b203544eb08848167bf1f0164e9f884. Lean/Mathlib remain at the base's pinned v4.35.0-rc3 (Mathlib c55e6e786f49471c72fbddbec5415808896aec1e); every dependency checkout was checked against the manifest. Before commit, current main was fetched at df9538f1976de4ab3b22dcaf457f30b28191a7d5: the selected project, its card, dependency pins and applicable contribution/review rules were identical to the measured base. The validated branch was retained.

All 2,430 pre-existing declarations match the Lean environment manifest exactly after erasing kernel-irrelevant expression metadata containing source positions. The audit loads private module data with environment extensions disabled, records full kernel expression types, universe parameters, declaration kinds and safety, and compares non-theorem values, reducibility hints, inductive/constructor metadata and recursor rules. No original declaration changed or disappeared. The only additions are two generated internal simplifier helpers. A raw pre-edit manifest is also retained. Definitions, instances, notation, statement syntax, public imports and generated indexes are unchanged. A complete traversal from all 2,432 resulting declarations reaches 43,560 constants and only Classical.choice, propext and Quot.sound.

The final measurement batch alternated base/head builds in two isolated worktrees, deleting only QuantumQuery's module artifacts before every run. External dependencies and filesystem caches were warm, default Lake/Lean parallelism was retained, and no other profiling or validation was run by this task during the batch. Wall seconds are monotonic elapsed time around /usr/bin/time -v lake build LeanPool.QuantumQuery.Imports; GNU time supplies peak RSS. Every run compiled the entire project and finished warning-free.

Revision	Run 1 (s)	Run 2 (s)	Run 3 (s)	Median (s)	Median peak RSS (KiB)
Base	74.441	72.170	73.430	73.430	2,112,396
Head	67.947	63.369	65.057	65.057	2,099,524

Separate synchronous command profiles identify where work was removed. These are allocation-counter reductions, not wall-time or RAM percentages:

Proof	Allocation reduction
single_one_mulVec	97.50%
blockDiagonal_mulVec_embed	91.52%
sqrt_cross_sum_le	81.05%
exists_algorithm_of_dualPairOn	78.91%
sqrt_starWeight_le_norm_wStarMatrix	77.30%
orNDual_isCostLe	71.66%
qNormSq_uniformConvError_le_sixteenth	68.10%

Validation passed:

• lake build LeanPool.QuantumQuery.Imports, including six final project-clean builds and warning scans.
• lake env lean --run scripts/ci/lint-project.lean with all seven project modules: 2,432 declarations passed the current CI linter.
• lake exe runLinter --no-build LeanPool.QuantumQuery.Imports.
• lake exe lint-style LeanPool.QuantumQuery.Imports.
• The unchanged python -m lean_pool.quality --repo <project-view>, including axiom and option-backdoor audits. The view contains byte-identical project sources, its existing YAML card, the unchanged discovery root/configuration and the real compiled artifacts.
• lake exe mk_all --module --check --repo <project-view>.
• lake shake --force --keep-public --explain LeanPool.QuantumQuery.Imports: all public imports retained.
• Environment manifest comparison after the final clean build; complete type/value dependency trust audit; git diff --check.

Timing varies on the shared VM; the 11.40% figure describes this three-pair experiment. No material RAM reduction is claimed. Local validation covers this project; whole-pool and other applicable protected CI checks and independent review remain required. CI, lint configuration, metadata, and waivers are untouched. The PR is left open without auto-merge.

Declaration-manifest reproduction script

Save the following outside the repository. After building the project at each revision, run lake env lean --run Manifest.lean manifest.jsonl. Compare the JSON objects indexed by name: every base record must exist unchanged at head. Theorem proof values are intentionally omitted; other values are included.

import Lean

open Lean

deriving instance Repr for ReducibilityHints

def text (s : String) : Json := toJson s

def names (ns : List Name) : Json := toJson (ns.map reprStr)

def eraseSourceMetadata : Expr → Expr
  | .app f a => .app (eraseSourceMetadata f) (eraseSourceMetadata a)
  | .lam n t b i => .lam n (eraseSourceMetadata t) (eraseSourceMetadata b) i
  | .forallE n t b i => .forallE n (eraseSourceMetadata t) (eraseSourceMetadata b) i
  | .letE n t v b d => .letE n (eraseSourceMetadata t) (eraseSourceMetadata v)
      (eraseSourceMetadata b) d
  | .mdata _ b => eraseSourceMetadata b
  | .proj n i b => .proj n i (eraseSourceMetadata b)
  | e => e

def expression (e : Expr) : Json := text (reprStr (eraseSourceMetadata e))

def details (info : ConstantInfo) : List (String × Json) :=
  match info with
  | .thmInfo v => [("kind", text "theorem"), ("mutual", names v.all)]
  | .defnInfo v => [("kind", text "definition"), ("value", expression v.value),
      ("hints", text (reprStr v.hints)), ("mutual", names v.all)]
  | .opaqueInfo v => [("kind", text "opaque"), ("value", expression v.value),
      ("mutual", names v.all)]
  | .axiomInfo _ => [("kind", text "axiom")]
  | .inductInfo v => [("kind", text "inductive"), ("mutual", names v.all),
      ("constructors", names v.ctors), ("parameters", toJson v.numParams),
      ("indices", toJson v.numIndices), ("nested", toJson v.numNested),
      ("recursive", toJson v.isRec), ("reflexive", toJson v.isReflexive)]
  | .ctorInfo v => [("kind", text "constructor"), ("inductive", text (reprStr v.induct)),
      ("index", toJson v.cidx), ("parameters", toJson v.numParams),
      ("fields", toJson v.numFields)]
  | .recInfo v => [("kind", text "recursor"), ("mutual", names v.all),
      ("parameters", toJson v.numParams), ("indices", toJson v.numIndices),
      ("motives", toJson v.numMotives), ("minors", toJson v.numMinors),
      ("k", toJson v.k), ("rules", toJson (v.rules.map fun r =>
        Json.mkObj [("constructor", text (reprStr r.ctor)),
          ("fields", toJson r.nfields), ("rhs", expression r.rhs)]))]
  | .quotInfo _ => [("kind", text "quotient")]

def main (args : List String) : IO Unit := do
  initSearchPath (← findSysroot)
  let env ← importModules #[{ module := `LeanPool.QuantumQuery.Imports }] {}
    (trustLevel := 0) (loadExts := false) (level := .private)
  let out ← IO.FS.Handle.mk (args.head!) .write
  let mut count := 0
  for (moduleName, data) in env.header.moduleNames.zip env.header.moduleData do
    unless moduleName == `LeanPool.QuantumQuery ||
        (`LeanPool.QuantumQuery).isPrefixOf moduleName do continue
    for name in data.constNames do
      let some info := env.find? name | throw (IO.userError s!"missing {name}")
      let fields := [("module", text moduleName.toString), ("name", text (reprStr name)),
        ("levels", names info.levelParams), ("type", expression info.type),
        ("unsafe", toJson info.isUnsafe), ("partial", toJson info.isPartial)]
      out.putStrLn (Json.mkObj (fields ++ details info)).compress
      count := count + 1
  IO.println s!"Manifest: {count} declarations (private data, full types and non-theorem values)."

[greptile-apps]

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 issue was found in this proof-only refactor.

Summary

Changes 19 existing proof bodies across four QuantumQuery modules to reduce elaboration work.

• Adversary matrix proofs use direct facts instead of broad simplification.
• Adversary certificate proofs use only the bounds each step needs.
• Spectral and OR-N bounds use direct cancellation and square identities.
• Quantum algorithm proofs use smaller, more direct algebra steps.
• The square-root cross-term proof follows direct bounds from its inputs.
• State-conversion proofs connect their error bounds with direct inequalities.
• Algorithm extraction proves its query bound with narrower arithmetic steps.

No actionable issues found. The reported 11.40% build-time reduction was not independently measured. Upstream source and license claims were not independently rechecked; this proof-only change leaves those claims and attribution untouched.

_{Reviews (1) · Last reviewed commit: "Reduce QuantumQuery proof elaboration co..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 1,658 tracked declarations across 4 modified files kept their type; only proofs / definition bodies changed.

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Compile cost of modified files — base → head

Heartbeats: 4,053,092 → 3,513,234 (-539,858, -13.3%). Commands: 7,471 → 7,471.

Per-file wall sum: 441.8 s → 283.3 s (-35.9%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal.

Files: 4 compared — 4 cheaper, 0 costlier, 0 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%).

Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted to maxHeartbeats units. Failed measurements are not classified as cheaper or costlier. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/QuantumQuery/StateConversion.lean	+34/-29	1,206,753	1,012,791	-193,962	-16.1%	119.53	82.21
LeanPool/QuantumQuery/Adversary.lean	+25/-31	1,749,252	1,573,868	-175,384	-10.0%	158.67	110.63
LeanPool/QuantumQuery/QueryBounds.lean	+9/-7	433,710	340,179	-93,531	-21.6%	76.12	34.02
LeanPool/QuantumQuery/Algorithms.lean	+7/-7	663,378	586,397	-76,981	-11.6%	87.50	56.45
Total	+75/-74	4,053,092	3,513,234	-539,858	-13.3%	441.8	283.3

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[Vilin97]

Source review at fdf917b00b203544eb08848167bf1f0164e9f884: favorable. I reviewed all 33 diff hunks and the 19 affected proofs across the four QuantumQuery files. Their written statements and assumptions are unchanged; complete base/head reconstruction also preserves every byte outside those existing proof values, including definitions, instances, imports, options and headers.

The direct matrix/Boolean lemmas and smaller simplification sets improve maintainability. The norm bounds retain their zero/positive cases; square-root cross-term and algorithm-extraction arguments retain the positivity conditions, witnesses and error budgets. I found no statement weakening, proof gap or new waiver in these edits.

The 11.40% timing result and compiled declaration-manifest audit remain the author's reported local experiments; I have not reproduced them. This source review does not replace current-head Lean build/lint/style/quality, other applicable protected checks, configured independent review or native integration. Those checks are still pending, and the current-main validation hold remains in force. No queue admission or auto-merge is requested by this review.

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: fdf917b00b203544eb08848167bf1f0164e9f884

Verdict: ✅ approve

The 19 proof rewrites replace sum expansion, Boolean case searches and broad arithmetic with existing lemmas, explicit cancellation and restricted tactic inputs. The larger arguments retain their intermediate bounds and mathematical structure, and reusable helpers remain intact. The stored /profile report records 13.3% fewer heartbeats across the four files. Local compilation was blocked by missing Mathlib dependencies; I did not reproduce the timing measurements.

Aspect	Value
Scope	targeted proof elaboration optimization
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The refactor makes proof dependencies more explicit and reduces automation without sacrificing structure or reusability.

---

Tokens: 646,423 in / 4,535 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.6537 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.