Skip to content

Import quantum parallel repetition proof - #395

Open
Vilin97 wants to merge 4 commits into
mainfrom
codex/import-openai-quantum-parallel-repetition-2026-09-04
Open

Import quantum parallel repetition proof#395
Vilin97 wants to merge 4 commits into
mainfrom
codex/import-openai-quantum-parallel-repetition-2026-09-04

Conversation

@Vilin97

@Vilin97 Vilin97 commented Sep 4, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

What this imports

This imports the complete formal proof of quantum parallel repetition from OpenAI's ten-proofs, preserving the exact public contracts of:

  • QuantumParallelRepetition.distributionUniformExponential
  • QuantumParallelRepetition.standardQuantumParallelRepetition

Canonical source: openai/ten-proofs@94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6 (Apache-2.0).

The proof also retains genuine proof-engineering improvements from Dean Cureton's Apache-2.0 comparison branch at deancureton/ten-proofs@30c21d72a2ee3308d66c945387729d736e0cb305, hence the mix provenance and joint attribution.

Optimization and cleanup

  • Split the 70,980-line monolith into 12 dependency-ordered implementation modules; every file is below 10,000 non-comment lines and every proof is at most 200 lines.
  • Replaced the broad Mathlib import with 13 exact leaf imports plus the narrow module chain. The focused build closure falls from 8,707 canonical jobs to 3,147 (63.9%). The final review pass alone removed six unrelated Part01 import carriers and cut the reviewed-head closure from 3,578 to 3,147 jobs (-431, -12.0%); compiling Part01 directly without those carriers succeeded with empty diagnostics in 7.93s / 3,735,952 KiB peak RSS, so no replacement imports were needed.
  • Removed all 419 inherited set_option commands and every diagnostic/waiver mechanism.
  • Removed or weakened redundant typeclass requirements: 154 fewer explicit Fintype binders and 64 fewer DecidableEq binders, with 12 genuinely needed assumptions weakened to Finite.
  • Marked 321 endpoint-internal, same-module-only implementation definitions private after compiled dependency, source-command, and downstream-token analysis. Seven apparent candidates were restored because downstream elaboration still uses them.
  • Consolidated the duplicate rectangular-matrix norm proof and duplicate conjugate-swap pipeline onto the existing canonical lemmas, and removed 11 unused internal helper arguments and their call obligations.
  • A refreshed compiled-kernel plus source-command DCE pass removed 18 declarations/commands from the reviewed head, including nine obsolete split-era norm instances. At the fixed point, all 2,651 exposed declarations and all 2,644 declaration commands are reachable from the two exact endpoints; zero dead commands remain. The visible kernel closure also fell from 3,123 to 3,120 declarations.
  • LOC (physical / non-comment code): canonical source 70,980 / 66,674; Dean-optimized source 71,128 / 66,822; final split plus root 71,999 / 66,590. The review cleanup removed 202 physical and 174 code lines from the submitted split; the final code is 84 lines below the canonical source and 232 below the optimized comparison despite the option-removal repairs and module boundaries.

Clean-build comparison on the same machine/toolchain, measured before the final deletion-only review pass:

version result wall peak RSS
canonical monolith reached one current-Mathlib signature incompatibility after full elaboration 5:44.73 15,346,484 KiB
split import baseline success 3:43.10 10,027,180 KiB

That baseline is 35.3% less wall time and 34.7% less peak RSS than the canonical monolith. The later deletion pass reduced both code and import closure further; its changed Parts 04--12 rebuild completed warning-free in 3:20.55 / 9,624,200 KiB. Parts 10--12, which contain the formerly memory-heavy tail, compile independently.

I also checked LeanPool.LeanQuantumAlg for reuse. Its pure-qubit/state-vector interface is not definitionally compatible with this development's arbitrary finite-dimensional density-matrix/POVM/game API; forcing adapters would enlarge the trusted surface and compile closure, so no reuse was accepted.

Contract and trust audits

Both endpoint source signatures remain byte-identical in the canonical source, Dean's optimized source, and this import:

  • distributionUniformExponential: SHA-256 65c987a3b4589f4b2ebf5d0e1ad3c794d57d944e15dce9f1bb46a4ffc3b894be
  • standardQuantumParallelRepetition: SHA-256 dc54fba91820ffe2239b0c59714c79cde1c6d814680875076c945f91f3c3dac9

An independent compiled type check accepts both original contracts. Each endpoint, and all 2,203 surviving public textual declarations, uses only propext, Classical.choice, and Quot.sound. The compiled option/backdoor audit is clean.

Validation

  • lake build LeanPool.QuantumParallelRepetition (warning-free; 3,147-job closure)
  • lake exe runLinter LeanPool.QuantumParallelRepetition and aggregate runLinter --no-build LeanPool (all 14 linters)
  • lake exe lint-style LeanPool
  • lake exe mk_all --check
  • repository static quality checker (9:59.91 / 4,166,364 KiB peak RSS)
  • focused headers, forbidden-text, file-size, proof-size, project-card, source-signature, all-public-declaration axiom, and compiled backdoor audits
  • aggregate LeanPool.lean collision build against current main: empty diagnostics, 45.58s wall / 7,486,932 KiB peak RSS, with no borrowed top-level LeanPool.olean

@greptile-apps

greptile-apps Bot commented Sep 4, 2026 •
edited
Loading

Copy link
Copy Markdown

Greptile Summary

The PR imports a quantum parallel repetition formalization as twelve dependency-ordered modules and registers its two headline results.

  • Adds finite-game, entangled-strategy, analytic, and parallel-repetition proof infrastructure.
  • Exposes distributionUniformExponential and standardQuantumParallelRepetition through the project entry module.
  • Registers the project in LeanPool/projects.yml and the aggregate LeanPool.lean import surface.

Important Files Changed
Filename Overview
LeanPool/QuantumParallelRepetition.lean Adds the documented project entry module, which transitively exports the complete implementation through Part12.
LeanPool/QuantumParallelRepetition/Part01.lean Introduces the foundational finite-game, strategy, probability, matrix, and analytic definitions used by later modules.
LeanPool/QuantumParallelRepetition/Part12.lean Completes the dependency chain and defines both registered headline theorems with types matching their catalog claims.
LeanPool/projects.yml Registers the project, provenance, measured characteristics, and faithful descriptions of both headline results.
LeanPool.lean Adds the project entry and implementation modules to the aggregate library import surface.

Reviews (4): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile

@github-actions

github-actions Bot commented Sep 4, 2026

Copy link
Copy Markdown
Contributor

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 427.26 s (= 7.12 min) — user 841.56 s, sys 23.16 s.

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: 13,664 maxHeartbeats units across 13 files (72,201 added LOC).

Sum of lean --profile: 706537.8 ms (= 706.54 s). Import-excluded time: 681507.8 ms (= 681.51 s).

Count-heartbeats wall-clock total: 632.97 s. Repeated import cost inside lean --profile: 25030.0 ms (= 25.03 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File LOC Heartbeats (maxHB) Count wall (s) lean --profile (s) Without import (s) Import (s) Decls Errors
LeanPool/QuantumParallelRepetition/Part12.lean 1,295 2,450 151.33 158.67 156.78 1.89 57 0
LeanPool/QuantumParallelRepetition/Part04.lean 7,535 2,106 45.00 57.28 55.30 1.98 364 0
LeanPool/QuantumParallelRepetition/Part01.lean 7,177 1,957 52.20 60.82 58.97 1.85 343 0
LeanPool/QuantumParallelRepetition/Part05.lean 7,487 1,261 39.01 43.46 41.54 1.92 278 0
LeanPool/QuantumParallelRepetition/Part06.lean 7,157 1,241 36.32 39.43 37.42 2.01 208 0
LeanPool/QuantumParallelRepetition/Part08.lean 7,011 1,072 52.19 61.77 59.82 1.95 162 0
LeanPool/QuantumParallelRepetition/Part07.lean 7,481 886 38.19 42.19 40.30 1.89 207 0
LeanPool/QuantumParallelRepetition/Part03.lean 7,426 852 43.64 49.68 47.72 1.96 311 0
LeanPool/QuantumParallelRepetition/Part02.lean 7,260 762 49.58 58.02 56.13 1.89 296 0
LeanPool/QuantumParallelRepetition/Part09.lean 7,164 720 68.23 72.45 70.51 1.94 243 0
LeanPool/QuantumParallelRepetition/Part10.lean 3,848 307 37.14 51.57 49.65 1.92 116 0
LeanPool/QuantumParallelRepetition/Part11.lean 1,342 50 16.79 9.06 7.12 1.94 25 0
LeanPool/QuantumParallelRepetition.lean 18 0 3.35 2.14 0.25 1.89 0 0
Total 72,201 13,664 632.97 706.54 681.51 25.03 2610 0

Aggregate phase totals

Phase Time
type checking 167550.0 ms (= 167.55 s)
tactic execution 131877.0 ms (= 131.88 s)
typeclass inference 127440.0 ms (= 127.44 s)
simp 84318.2 ms (= 84.32 s)
interpretation 75652.0 ms (= 75.65 s)
elaboration 30916.1 ms (= 30.92 s)
import 25030.0 ms (= 25.03 s)
blocked (unaccounted) 12684.9 ms (= 12.68 s)
tacticAnalysis 10018.2 ms (= 10.02 s)
norm_num 7524.7 ms (= 7.52 s)
linting 7045.9 ms (= 7.05 s)
let-to-have transformation 4791.1 ms (= 4.79 s)

Slowest changed modules (from lake build)

Changed module Lake time
LeanPool.QuantumParallelRepetition.Part12 166.00 s
LeanPool.QuantumParallelRepetition.Part09 43.00 s
LeanPool.QuantumParallelRepetition.Part01 32.00 s
LeanPool.QuantumParallelRepetition.Part10 24.00 s
LeanPool.QuantumParallelRepetition.Part04 22.00 s
LeanPool.QuantumParallelRepetition.Part08 22.00 s
LeanPool.QuantumParallelRepetition.Part02 21.00 s
LeanPool.QuantumParallelRepetition.Part03 18.00 s
LeanPool.QuantumParallelRepetition.Part05 17.00 s
LeanPool.QuantumParallelRepetition.Part07 17.00 s
LeanPool.QuantumParallelRepetition.Part06 16.00 s
LeanPool.QuantumParallelRepetition.Part11 10.00 s
Per-file `lean --profile` output

LeanPool/QuantumParallelRepetition.lean

import took 1.89s
cumulative profiling times:
	elaboration 0.147ms
	import 1.89s
	initialization 31.1ms
	interpretation 215ms
	linting 0.328ms
	module linting 0.00119ms
	overlappingInstancesLinter 0.281ms
	parsing 0.0268ms
	tacticAnalysis 2.16ms
real 2.85
user 1.60
sys 1.25

LeanPool/QuantumParallelRepetition/Part01.lean

import took 1.85s
typeclass inference of Nonempty took 112ms
simp took 134ms
simp took 124ms
simp took 221ms
simp took 116ms
simp took 191ms
simp took 187ms
typeclass inference of CompleteSpace took 154ms
typeclass inference of StarHomClass took 192ms
typeclass inference of StarHomClass took 189ms
simp took 139ms
simp took 117ms
simp took 133ms
simp took 397ms
typeclass inference of StarHomClass took 177ms
typeclass inference of CompleteSpace took 151ms
typeclass inference of CompleteSpace took 145ms
tactic execution of Lean.Parser.Tactic.congr took 260ms
simp took 300ms
typeclass inference of CompleteSpace took 145ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 192ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 214ms
simp took 117ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 105ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 196ms
typeclass inference of Monoid took 792ms
typeclass inference of StarHomClass took 367ms
simp took 232ms
tactic execution of Lean.Parser.Tactic.congr took 675ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 119ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 158ms
simp took 129ms
cumulative profiling times:
	attribute application 19ms
	blocked (unaccounted) 1.7s
	compilation (IR) 4.68ms
	compilation (LCNF base) 52.4ms
	compilation (LCNF impure) 23.2ms
	compilation (LCNF mono) 52.4ms
	congr simp thm 178ms
	dsimp 62.8ms
	elaboration 3.02s
	fix level params 73.2ms
	import 1.85s
	initialization 29.4ms
	instantiate metavars 62ms
	interpretation 7.2s
	let-to-have transformation 77ms
	linting 643ms
	module linting 0.00179ms
	norm_num 93.9ms
	overlappingInstancesLinter 145ms
	parsing 473ms
	process pre-definitions 436ms
	ring 264ms
	share common exprs 277ms
	simp 8.03s
	tactic execution 9.68s
	tacticAnalysis 1.12s
	type checking 3.85s
	typeclass inference 21.4s
real 19.77
user 58.36
sys 1.72

LeanPool/QuantumParallelRepetition/Part02.lean

import took 1.89s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 231ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 227ms
simp took 402ms
simp took 4.37s
simp took 823ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 382ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 611ms
simp took 106ms
simp took 203ms
simp took 104ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 280ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 110ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 104ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 169ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 101ms
typeclass inference of Nonempty took 152ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 440ms
simp took 106ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 396ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 148ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 710ms
typeclass inference of AddMonoidHomClass took 121ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 164ms
tactic execution of Lean.Parser.Tactic.congr took 227ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 140ms
simp took 381ms
cumulative profiling times:
	attribute application 8.67ms
	blocked (unaccounted) 111ms
	compilation (IR) 2.76ms
	compilation (LCNF base) 31.4ms
	compilation (LCNF impure) 12.8ms
	compilation (LCNF mono) 24.7ms
	congr simp thm 122ms
	dsimp 127ms
	elaboration 2.57s
	fix level params 50.7ms
	import 1.89s
	initialization 29.7ms
	instantiate metavars 76.6ms
	interpretation 9.68s
	let-to-have transformation 51.5ms
	linting 636ms
	module linting 0.00146ms
	norm_num 471ms
	overlappingInstancesLinter 116ms
	parsing 450ms
	process pre-definitions 437ms
	ring 745ms
	share common exprs 351ms
	simp 10.5s
	tactic execution 9.76s
	tacticAnalysis 960ms
	type checking 3.21s
	typeclass inference 15.6s
real 18.71
user 57.19
sys 1.71

LeanPool/QuantumParallelRepetition/Part03.lean

import took 1.96s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 179ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 137ms
tactic execution of Lean.Parser.Tactic.change took 103ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 331ms
simp took 131ms
simp took 221ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 244ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 536ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 333ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 161ms
simp took 114ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 155ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 199ms
tactic execution of Mathlib.Tactic.nlinarith took 150ms
tactic execution of Lean.Parser.Tactic.congr took 1.06s
simp took 142ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 673ms
typeclass inference of AddMonoidHomClass took 122ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 175ms
cumulative profiling times:
	attribute application 8.92ms
	blocked (unaccounted) 5.24s
	compilation (IR) 2.75ms
	compilation (LCNF base) 28.7ms
	compilation (LCNF impure) 14.1ms
	compilation (LCNF mono) 31.1ms
	congr simp thm 118ms
	dsimp 68.1ms
	elaboration 2.51s
	fix level params 46.1ms
	import 1.96s
	initialization 37.5ms
	instantiate metavars 61ms
	interpretation 8.01s
	let-to-have transformation 10.6ms
	linting 649ms
	module linting 0.00147ms
	norm_num 554ms
	overlappingInstancesLinter 109ms
	parsing 439ms
	process pre-definitions 374ms
	ring 545ms
	share common exprs 281ms
	simp 4.13s
	tactic execution 8.31s
	tacticAnalysis 1.02s
	type checking 2.62s
	typeclass inference 12.5s
real 14.97
user 43.73
sys 1.69

LeanPool/QuantumParallelRepetition/Part04.lean

import took 1.98s
simp took 168ms
elaboration took 102ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 176ms
simp took 1.41s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.13s
simp took 181ms
simp took 176ms
simp took 169ms
simp took 173ms
simp took 170ms
simp took 172ms
simp took 180ms
simp took 180ms
simp took 170ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 142ms
elaboration took 349ms
simp took 129ms
simp took 110ms
simp took 106ms
simp took 143ms
simp took 108ms
simp took 149ms
simp took 477ms
simp took 881ms
simp took 894ms
simp took 896ms
simp took 992ms
simp took 2.33s
simp took 300ms
simp took 491ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 111ms
simp took 203ms
simp took 199ms
simp took 196ms
simp took 205ms
tactic execution of Mathlib.Tactic.nlinarith took 106ms
cumulative profiling times:
	aesop 194ms
	attribute application 13.7ms
	blocked (unaccounted) 2.35s
	compilation (IR) 2.76ms
	compilation (LCNF base) 28.3ms
	compilation (LCNF impure) 15.1ms
	compilation (LCNF mono) 29.8ms
	congr simp thm 132ms
	elaboration 4.05s
	fix level params 73.1ms
	import 1.98s
	initialization 30.4ms
	instantiate metavars 68.3ms
	interpretation 6.85s
	let-to-have transformation 11.5ms
	linting 705ms
	module linting 0.00203ms
	norm_num 160ms
	overlappingInstancesLinter 161ms
	parsing 455ms
	process pre-definitions 405ms
	ring 325ms
	share common exprs 282ms
	simp 16s
	tactic execution 5.3s
	tacticAnalysis 1.14s
	type checking 2.52s
	typeclass inference 14s
real 18.46
user 54.41
sys 1.75

LeanPool/QuantumParallelRepetition/Part05.lean

import took 1.92s
typeclass inference of Nonempty took 161ms
typeclass inference of Nonempty took 139ms
typeclass inference of Nonempty took 155ms
typeclass inference of Nonempty took 139ms
type checking took 113ms
tactic execution of Lean.Parser.Tactic.change took 103ms
typeclass inference of AddMonoidHomClass took 125ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 917ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 328ms
tactic execution of Lean.Parser.Tactic.exact took 112ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 327ms
tactic execution of Lean.Parser.Tactic.exact took 112ms
tactic execution of Lean.Parser.Tactic.congr took 343ms
tactic execution of Lean.Parser.Tactic.congr took 182ms
simp took 101ms
tactic execution of Lean.Parser.Tactic.exact took 238ms
tactic execution of Lean.Parser.Tactic.exact took 224ms
simp took 406ms
simp took 111ms
simp took 101ms
tactic execution of Lean.Parser.Tactic.change took 122ms
typeclass inference of AddMonoidHomClass took 115ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 837ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 400ms
tactic execution of Lean.Parser.Tactic.change took 253ms
tactic execution of Mathlib.Tactic.FieldSimp.fieldSimp took 104ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 428ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 374ms
tactic execution of Lean.Parser.Tactic.change took 256ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 450ms
type checking took 100ms
cumulative profiling times:
	attribute application 19.7ms
	blocked (unaccounted) 1.35s
	compilation (IR) 2.28ms
	compilation (LCNF base) 19.1ms
	compilation (LCNF impure) 11ms
	compilation (LCNF mono) 21ms
	congr simp thm 119ms
	dsimp 10.9ms
	elaboration 2.73s
	fix level params 86.5ms
	import 1.92s
	initialization 28.9ms
	instantiate metavars 67.1ms
	interpretation 5.03s
	let-to-have transformation 45.8ms
	linting 589ms
	module linting 0.00147ms
	norm_num 74ms
	overlappingInstancesLinter 142ms
	parsing 391ms
	process pre-definitions 459ms
	ring 172ms
	share common exprs 264ms
	simp 4.44s
	tactic execution 12.2s
	tacticAnalysis 969ms
	type checking 2.56s
	typeclass inference 9.74s
real 14.35
user 41.51
sys 1.64

LeanPool/QuantumParallelRepetition/Part06.lean

import took 2.01s
linting took 102ms
tactic execution of Lean.Parser.Tactic.exact took 238ms
tactic execution of Lean.Parser.Tactic.exact took 235ms
tactic execution of Lean.Parser.Tactic.exact took 233ms
tactic execution of Lean.Parser.Tactic.exact took 227ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 128ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 147ms
simp took 130ms
simp took 107ms
simp took 168ms
simp took 175ms
simp took 102ms
tactic execution of Lean.Parser.Tactic.refine took 130ms
simp took 153ms
tactic execution of Lean.Parser.Tactic.change took 889ms
simp took 219ms
simp took 240ms
simp took 359ms
simp took 240ms
simp took 116ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 476ms
cumulative profiling times:
	attribute application 4.77ms
	blocked (unaccounted) 2.55ms
	compilation (IR) 1.13ms
	compilation (LCNF base) 22ms
	compilation (LCNF impure) 6.59ms
	compilation (LCNF mono) 14.3ms
	congr simp thm 90.2ms
	dsimp 156ms
	elaboration 2.5s
	fix level params 73.7ms
	import 2.01s
	initialization 34.5ms
	instantiate metavars 69.7ms
	interpretation 5.65s
	let-to-have transformation 79.4ms
	linting 716ms
	module linting 0.00129ms
	norm_num 173ms
	overlappingInstancesLinter 97.4ms
	parsing 371ms
	process pre-definitions 321ms
	ring 251ms
	share common exprs 256ms
	simp 5.92s
	tactic execution 8.57s
	tacticAnalysis 1.02s
	type checking 2.3s
	typeclass inference 8.72s
real 13.35
user 38.36
sys 1.81

LeanPool/QuantumParallelRepetition/Part07.lean

import took 1.89s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 596ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 114ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 156ms
typeclass inference of Nonempty took 115ms
simp took 179ms
tactic execution of Lean.Parser.Tactic.exact took 768ms
tactic execution of Lean.Parser.Tactic.exact took 240ms
tactic execution of Lean.Parser.Tactic.change took 133ms
tactic execution of Lean.Parser.Tactic.exact took 757ms
tactic execution of Lean.Parser.Tactic.exact took 207ms
tactic execution of Lean.Parser.Tactic.change took 131ms
tactic execution of Lean.Parser.Tactic.refine took 104ms
tactic execution of Lean.Parser.Tactic.exact took 146ms
simp took 318ms
tactic execution of Lean.Parser.Tactic.refine took 1.02s
tactic execution of Lean.Parser.Tactic.exact took 593ms
linting took 367ms
tactic execution of Lean.Parser.Tactic.refine took 106ms
tactic execution of Lean.Parser.Tactic.exact took 146ms
tactic execution of Lean.Parser.Tactic.refine took 929ms
tactic execution of Lean.Parser.Tactic.exact took 669ms
simp took 321ms
linting took 350ms
tactic execution of Lean.Parser.Tactic.congr took 150ms
cumulative profiling times:
	attribute application 4.28ms
	blocked (unaccounted) 1.38ms
	compilation (IR) 0.273ms
	compilation (LCNF base) 2.7ms
	compilation (LCNF impure) 1.38ms
	compilation (LCNF mono) 1.94ms
	congr simp thm 84.6ms
	dsimp 63.2ms
	elaboration 2.21s
	fix level params 48.5ms
	import 1.89s
	initialization 37.7ms
	instantiate metavars 69.9ms
	interpretation 6.68s
	let-to-have transformation 12.6ms
	linting 1.39s
	module linting 0.00136ms
	norm_num 1.8s
	overlappingInstancesLinter 99.8ms
	parsing 403ms
	process pre-definitions 289ms
	ring 635ms
	share common exprs 270ms
	simp 3.06s
	tactic execution 12.8s
	tacticAnalysis 1.03s
	type checking 1.67s
	typeclass inference 7.63s
real 13.42
user 41.17
sys 1.65

LeanPool/QuantumParallelRepetition/Part08.lean

import took 1.95s
simp took 112ms
typeclass inference of ZeroHomClass took 129ms
type checking took 144ms
tactic execution of Lean.Parser.Tactic.congr took 128ms
typeclass inference of Nonempty took 120ms
typeclass inference of Nonempty took 171ms
typeclass inference of Nonempty took 163ms
interpretation of Mathlib.Meta.Positivity.evalMul._lam_3._boxed took 206ms
simp took 109ms
simp took 164ms
simp took 231ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 189ms
simp took 154ms
interpretation of Mathlib.Meta.Positivity.evalMul._lam_3._boxed took 249ms
tactic execution of Lean.Parser.Tactic.congr took 864ms
tactic execution of Lean.Parser.Tactic.congr took 155ms
tactic execution of Lean.Parser.Tactic.congr took 854ms
tactic execution of Lean.Parser.Tactic.congr took 154ms
tactic execution of Lean.Parser.Tactic.change took 2.48s
simp took 366ms
tactic execution of Lean.Parser.Tactic.exact took 220ms
simp took 380ms
simp took 370ms
tactic execution of Lean.Parser.Tactic.exact took 786ms
tactic execution of Lean.Parser.Tactic.exact took 455ms
tactic execution of Lean.Parser.Tactic.exact took 1.47s
tactic execution of Lean.Parser.Tactic.eqRefl took 147ms
tactic execution of Lean.Parser.Tactic.exact took 495ms
tactic execution of Lean.Parser.Tactic.change took 915ms
tactic execution of Lean.Parser.Tactic.congr took 556ms
tactic execution of Lean.Parser.Tactic.congr took 164ms
tactic execution of Lean.Parser.Tactic.exact took 390ms
tactic execution of Lean.Parser.Tactic.eqRefl took 237ms
tactic execution of Lean.Parser.Tactic.congr took 190ms
tactic execution of Lean.Parser.Tactic.exact took 480ms
tactic execution of Lean.Parser.Tactic.congr took 3.32s
tactic execution of Lean.Parser.Tactic.change took 2.41s
simp took 363ms
tactic execution of Lean.Parser.Tactic.exact took 245ms
simp took 391ms
simp took 377ms
tactic execution of Lean.Parser.Tactic.exact took 820ms
tactic execution of Lean.Parser.Tactic.exact took 396ms
tactic execution of Lean.Parser.Tactic.exact took 1.35s
tactic execution of Lean.Parser.Tactic.eqRefl took 148ms
tactic execution of Lean.Parser.Tactic.exact took 502ms
tactic execution of Lean.Parser.Tactic.change took 954ms
tactic execution of Lean.Parser.Tactic.congr took 572ms
tactic execution of Lean.Parser.Tactic.congr took 147ms
tactic execution of Lean.Parser.Tactic.exact took 346ms
tactic execution of Lean.Parser.Tactic.change took 518ms
tactic execution of Lean.Parser.Tactic.refine took 509ms
tactic execution of Lean.Parser.Tactic.exact took 547ms
cumulative profiling times:
	attribute application 24.4ms
	blocked (unaccounted) 1.05s
	compilation (IR) 1.68ms
	compilation (LCNF base) 19.1ms
	compilation (LCNF impure) 8.55ms
	compilation (LCNF mono) 15.9ms
	congr simp thm 134ms
	dsimp 21.2ms
	elaboration 2.89s
	fix level params 65ms
	import 1.95s
	initialization 32.8ms
	instantiate metavars 65.7ms
	interpretation 4.59s
	let-to-have transformation 67.5ms
	linting 539ms
	module linting 0.00145ms
	norm_num 64.5ms
	overlappingInstancesLinter 112ms
	parsing 363ms
	process pre-definitions 338ms
	ring 105ms
	share common exprs 249ms
	simp 5.76s
	tactic execution 29s
	tacticAnalysis 945ms
	type checking 2.46s
	typeclass inference 10.9s
real 19.05
user 59.98
sys 1.90

LeanPool/QuantumParallelRepetition/Part09.lean

import took 1.94s
simp took 112ms
simp took 153ms
simp took 155ms
type checking took 137ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 144ms
simp took 201ms
simp took 123ms
simp took 118ms
simp took 118ms
simp took 112ms
simp took 119ms
simp took 119ms
simp took 119ms
simp took 119ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 285ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 236ms
type checking took 113ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 135ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 164ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 100ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 336ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 271ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 124ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 374ms
simp took 142ms
simp took 1.28s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 102ms
type checking took 146ms
tactic execution of Lean.Parser.Tactic.change took 119ms
simp took 113ms
tactic execution of Lean.Parser.Tactic.change took 385ms
simp took 162ms
simp took 333ms
simp took 1.06s
simp took 576ms
simp took 1.88s
simp took 2.6s
simp took 4.9s
tactic execution of Lean.Parser.Tactic.change took 120ms
simp took 379ms
simp took 305ms
simp took 302ms
simp took 293ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 372ms
type checking took 149ms
simp took 260ms
let-to-have transformation took 3.72s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 324ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 519ms
simp took 1.33s
tactic execution of Lean.Parser.Tactic.refine took 139ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 153ms
tactic execution of Lean.Parser.Tactic.exact took 248ms
simp took 283ms
tactic execution of Lean.Parser.Tactic.congr took 1.12s
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 113ms
type checking took 975ms
simp took 433ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 352ms
type checking took 179ms
tactic execution of Lean.Parser.Tactic.refine took 120ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 188ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 113ms
tactic execution of Lean.Parser.Tactic.change took 229ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 539ms
type checking took 198ms
cumulative profiling times:
	attribute application 15.2ms
	compilation (IR) 4.63ms
	compilation (LCNF base) 63.9ms
	compilation (LCNF impure) 22.2ms
	compilation (LCNF mono) 43.3ms
	congr simp thm 163ms
	dsimp 54.4ms
	elaboration 4.23s
	fix level params 61ms
	import 1.94s
	initialization 29.4ms
	instantiate metavars 104ms
	interpretation 6.91s
	let-to-have transformation 3.85s
	linting 595ms
	module linting 0.00152ms
	norm_num 393ms
	overlappingInstancesLinter 116ms
	parsing 409ms
	process pre-definitions 545ms
	ring 394ms
	share common exprs 426ms
	simp 21s
	tactic execution 12.1s
	tacticAnalysis 975ms
	type checking 5.71s
	typeclass inference 12.3s
real 24.46
user 72.06
sys 1.74

LeanPool/QuantumParallelRepetition/Part10.lean

import took 1.92s
typeclass inference of Nonempty took 105ms
simp took 661ms
typeclass inference of Nonempty took 159ms
typeclass inference of Nonempty took 114ms
simp took 601ms
typeclass inference of Nonempty took 155ms
typeclass inference of Nonempty took 113ms
simp took 651ms
simp took 594ms
tactic execution of Lean.Parser.Tactic.change took 129ms
elaboration took 131ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 107ms
simp took 324ms
simp took 189ms
simp took 461ms
type checking took 896ms
type checking took 128ms
tactic execution of Lean.Parser.Tactic.change took 130ms
type checking took 160ms
tactic execution of Lean.Parser.Tactic.exact took 458ms
tactic execution of Lean.Parser.Tactic.exact took 2.42s
type checking took 112ms
tactic execution of Lean.Parser.Tactic.exact took 122ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 471ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 115ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 6.26s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 106ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 107ms
interpretation of Mathlib.Meta.Positivity.evalDiv._lam_0._boxed took 107ms
elaboration took 113ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 369ms
tactic execution of Lean.Parser.Tactic.obtain took 390ms
tactic execution of Lean.Parser.Tactic.simpa took 112ms
tactic execution of Lean.Parser.Tactic.obtain took 356ms
type checking took 110ms
cumulative profiling times:
	attribute application 2.84ms
	compilation (IR) 0.408ms
	compilation (LCNF base) 5.26ms
	compilation (LCNF impure) 2.08ms
	compilation (LCNF mono) 3.84ms
	congr simp thm 73.3ms
	dsimp 37.8ms
	elaboration 2.21s
	fix level params 39ms
	import 1.92s
	initialization 37.8ms
	instantiate metavars 62ms
	interpretation 13.4s
	let-to-have transformation 144ms
	linting 412ms
	module linting 0.00164ms
	norm_num 3.74s
	overlappingInstancesLinter 57.6ms
	parsing 215ms
	process pre-definitions 270ms
	ring 732ms
	share common exprs 345ms
	simp 5.28s
	tactic execution 7.54s
	tacticAnalysis 543ms
	type checking 3.3s
	typeclass inference 11.2s
real 16.72
user 50.89
sys 1.43

LeanPool/QuantumParallelRepetition/Part11.lean

import took 1.94s
type checking took 102ms
type checking took 235ms
dsimp took 277ms
type checking took 100ms
tactic execution of Lean.Parser.Tactic.simpa took 214ms
type checking took 156ms
cumulative profiling times:
	attribute application 0.556ms
	congr simp thm 99.6ms
	dsimp 302ms
	elaboration 846ms
	fix level params 9.47ms
	import 1.94s
	initialization 32.2ms
	instantiate metavars 10.1ms
	interpretation 718ms
	let-to-have transformation 439ms
	linting 94.2ms
	module linting 0.00117ms
	overlappingInstancesLinter 21.2ms
	parsing 47.1ms
	process pre-definitions 84.4ms
	share common exprs 68.5ms
	simp 68.2ms
	tactic execution 917ms
	tacticAnalysis 130ms
	type checking 1.35s
	typeclass inference 1.88s
real 6.61
user 8.79
sys 1.33

LeanPool/QuantumParallelRepetition/Part12.lean

import took 1.89s
congr simp thm took 113ms
elaboration took 185ms
tactic execution of Lean.Parser.Tactic.obtain took 756ms
tactic execution of Lean.Parser.Tactic.exact took 475ms
tactic execution of Lean.Parser.Tactic.exact took 432ms
tactic execution of Lean.Parser.Tactic.exact took 887ms
tactic execution of Lean.Parser.Tactic.congr took 8.58s
tactic execution of Lean.Parser.Tactic.change took 1.27s
type checking took 129ms
tactic execution of Lean.Parser.Tactic.exact took 121ms
tactic execution of Lean.Parser.Tactic.change took 939ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 367ms
tactic execution of Lean.Parser.Tactic.exact took 469ms
type checking took 106ms
tactic execution of Lean.Parser.Tactic.change took 394ms
type checking took 85.9s
tactic execution of Lean.Parser.Tactic.change took 268ms
type checking took 49.2s
cumulative profiling times:
	attribute application 1.45ms
	blocked (unaccounted) 880ms
	compilation (IR) 0.082ms
	compilation (LCNF base) 0.924ms
	compilation (LCNF impure) 0.432ms
	compilation (LCNF mono) 2.76ms
	congr simp thm 144ms
	elaboration 1.15s
	fix level params 5.7ms
	import 1.89s
	initialization 29ms
	instantiate metavars 10.8ms
	interpretation 719ms
	let-to-have transformation 2.21ms
	linting 77.4ms
	module linting 0.00135ms
	norm_num 1.32ms
	overlappingInstancesLinter 27ms
	parsing 57.8ms
	process pre-definitions 58.4ms
	ring 3.23ms
	share common exprs 40ms
	simp 130ms
	tactic execution 15.7s
	tacticAnalysis 164ms
	type checking 136s
	typeclass inference 1.57s
real 153.04
user 156.73
sys 2.15

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

@github-actions

github-actions Bot commented Sep 4, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

Reviewed head: da4ddbe1af656b540f35e3a92d4642d278410121

⚠️ Partial review — diff exceeded the size budget. The bodies of the 5 largest of 15 file patches were elided before review; an elided review cannot approve.

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

Rubric Verdict Bottom line
Faithfulness 🤔 discuss Based on the partial diff, the visible endpoint statements match the card, but the elided Parts 03, 05, 06, 07, and 09 prevent a complete audit for postulated or vacuous intermediate content.
Novelty ✅ pass Based on the partial diff and supplied prior-art search, neither headline is already formalized in Mathlib or the pool.
Significance ✅ pass Based on the partial diff, this is a research-level formalization of a named quantum-information theorem with a substantial supporting development.
Sources ✅ pass Based on the partial diff, the canonical repository and commit are identified consistently and Dean Cureton's prior branch is credited, but the source contents are not independently verifiable from the diff.
Code quality (advisory) 🤔 discuss Based on the partial diff, the code is competent but the pervasive public/private boundary leaks and duplicate abstractions require maintainer review.
Aspect Value
Proves the claim ➖ unverifiable
Assumed, not proved The quantitative endpoint assumes Nonempty A, Nonempty B, 0 < 1 - entangledValue G, and 0 < n; the qualitative endpoint assumes entangledValue G < 1; these conditions are disclosed in the card, and neither endpoint retains a proof-result hypothesis.
Matches cited source 🟡 unverifiable
Fit ✅ good_fit
Level research
Branch quantum information theory
Mode theory_building
Code quality 3 / 5

Statement check: distributionUniformExponential gives a game-independent 0 < c and, for nonempty answer types, positive gap, and 0 < n, the displayed gap/alphabet bound on the finite-dimensional entangled value of G.repeat n; standardQuantumParallelRepetition gives the qualitative ∃ c, C > 0, ∀ n form.

The development culminates in distributionUniformExponential, an explicit universal exponential upper bound for repeated entangled values, and standardQuantumParallelRepetition, the standard parallel-repetition theorem for finite nonlocal games.

Faithfulness findings (1)

  • partial-diff — PR-wide
    The endpoint contracts are visible and faithful, but their proof chain traverses five elided implementation modules; those modules must be inspected for bundled hypotheses or structure-field postulates before the faithfulness audit is complete.
    Evidence: The visible qualitative contract is def StandardQuantumParallelRepetition (G : Game X Y A B) : Prop := entangledValue G < 1 → HasExponentialBound (repeatedEntangledValue G), where def HasExponentialBound (v : ℕ → ℝ) : Prop := ∃ c : ℝ, 0 < c ∧ ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, v n ≤ C * Real.exp (-c * (n : ℝ)); however, for example, the Part03 patch contains [elided by lean-pool llm-review: 7,388 of 7,428 patch lines omitted — diff exceeded the review size budget], with corresponding elisions in Parts 05, 06, 07, and 09.

Code quality findings (2)

  • api-visibility — PR-wide
    Implementation visibility is inconsistent across the PR: public theorems expose private constants in their types. Part01 does this for the mixture, spectral-purification, spectral-support, and purification-range families; Part12 publicly returns and consumes private sampler, stopping, and ledger structures. These declarations are difficult to use from another module and make private refactors part of the compiled interface. Mark each associated theorem private with its implementation, or make the underlying abstraction intentionally public.
    Evidence: Part01 declares private def mixtureEmbedding (S : J → Strategy G) : but then exposes theorem mixtureEmbedding_isometry (S : J → Strategy G) : (mixtureEmbedding S)ᴴ * mixtureEmbedding S = 1 := by. Part12 similarly declares private structure UnconditionalActualFairSourceSamplerData and then exposes a theorem with result Nonempty (UnconditionalActualFairSourceSamplerData G n S D gamma) := by.
  • duplicate-definition — PR-wide
    The visible modules contain exact duplicate public abstractions and a repeated norm proof. Keep one canonical Schmidt-coefficient definition, consolidate the two remaining-coordinate cardinality lemmas, and prove the matrix-purification norm result by rewriting matrixVectorization_norm_sq rather than duplicating its calculation.
    Evidence: Part02 defines both def dSVUniformLeftDensitySchmidtCoefficient {d : ℕ} (ξ : BipartiteUnitVector d) (i : Fin d) : ℝ := Real.sqrt ((dSVSoftBobLeftReducedDensity_posSemidef ξ).isHermitian.eigenvalues i) and def dSVUniformDensityPolarLeftSchmidtCoefficient {d : ℕ} (ξ : BipartiteUnitVector d) (i : Fin d) : ℝ := Real.sqrt ((dSVSoftBobLeftReducedDensity_posSemidef ξ).isHermitian.eigenvalues i). Part04 separately proves remainingCoordinate_card_pos and exactRemainingCoordinate_card_pos with the same conclusion and the same simpa only [Fintype.card_coe, card_pos] proof. Part01 defines private def matrixPurificationVector {d : Type*} (K : Matrix d d ℂ) : EuclideanSpace ℂ (d × d) := toLp 2 (Matrix.vec K) and then reproves matrixPurificationVector_norm_sq despite the earlier matrixVectorization_norm_sq.

Tokens: 2,293,564 in / 19,779 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $11.9128
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.

@Vilin97

Vilin97 commented Sep 4, 2026

Copy link
Copy Markdown
Owner Author

Addressed the fresh code-quality findings in da4ddbe1 with endpoint contracts held immutable.

  1. Part01 import residue: all six flagged high-level carriers were removed, with no replacement imports. A direct compile of an exact Part01 copy without them completed with empty diagnostics in 7.93s / 3,735,952 KiB peak RSS. The project now has 13 exact Mathlib leaves (down from 19), and its build graph is 3,147 jobs, down from 3,578 at the reviewed head (-431 / -12.0%) and 8,707 for the canonical monolith (-5,560 / -63.9%).
  2. Duplicated proof pipelines: removed the duplicate rectangular-matrix norm theorem and routed all consumers through rectangularMatrix_norm_sq; removed the five-declaration duplicate polar conjugate-swap pipeline and reused dSVUniformLeftDensityConjugateSwap plus its existing density theorem. The visible endpoint kernel closure fell from 3,123 to 3,120 declarations.
  3. Unused hypotheses: cascade-removed 11 internal helper binders and every associated call obligation: six positivity arguments in the greedy-stopping chain, four equal-card/normalization arguments in the permutation chain, and one positivity argument in the conditioning wrapper. The full 14-linter pass now reports no unusedArguments finding.

I then repeated compiled-kernel plus source-command DCE rather than stopping at the reported sites. Net result: 18 declarations/commands removed from the reviewed head (including nine obsolete split-era norm instances), 202 physical / 174 non-comment code lines removed, and a fixed point of 2,651/2,651 endpoint-live exposed declarations plus 2,644/2,644 endpoint-live declaration commands, with zero dead commands. All 2,203 public textual declarations pass the axiom audit.

Contract verification after the final rebuild:

  • distributionUniformExponential source hash remains 65c987a3b4589f4b2ebf5d0e1ad3c794d57d944e15dce9f1bb46a4ffc3b894be and depends only on [propext, Classical.choice, Quot.sound].
  • standardQuantumParallelRepetition source hash remains dc54fba91820ffe2239b0c59714c79cde1c6d814680875076c945f91f3c3dac9 and depends only on [propext, Classical.choice, Quot.sound].

Final verification is green: warning-free focused rebuild; all 14 project and aggregate linters; full-tree style; mk_all --check; repository static quality; source-signature, public-axiom, option/backdoor, file/proof-size scans; and a direct aggregate LeanPool.lean collision compile against current main (45.58s / 7,486,932 KiB peak RSS, empty diagnostics).

@github-actions
Merge remote-tracking branch 'origin/main' into pr-395
7fa69c8 
# Conflicts:
#	LeanPool/projects.yml
@Vilin97

Vilin97 commented Sep 5, 2026

Copy link
Copy Markdown
Owner Author

Automation disposition: needs-maintainer

Reviewed exact head 7fa69c87dc89867c9c52d4e16b1833b58f4476b2. The endpoint contracts, source/provenance, and current CI are green, and the author addressed the previously identified import/duplication/dead-declaration findings. A fresh complete exact-head LLM review is not available for this 72,054-line, 427.26 s development (the prior review was elided and scored code quality 3/5); the remaining public/private API and generated-scale maintenance trade-off requires a maintainer decision before merge.

@Vilin97 Vilin97 added the needs-maintainer Requires a maintainer decision; automation must not merge label Sep 5, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

needs-maintainer Requires a maintainer decision; automation must not merge

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Vilin97