[Vilin97]

This imports the exact adaptive single-copy qubit stabilizer learner from Antonio Anna Mele’s formalization. The endpoint connects actual normalized complex amplitudes, physical measurement PMFs, Clifford gate updates, a finite circuit/readout, recovery up to global phase, and explicit confidence/copy/gate upper bounds. The reusable layers include finite probability identities, geometric domination and tails, binary symplectic linear algebra, stabilizer measurement, and instruction semantics.

The source is Bittel–Eisert–Gong–Mele–Schatzki, arXiv:2610.02031, submitted 2026-10-01 16:48:31 UTC. The pinned implementation commit d8282e1d59a1a9b8d34396f06298f478c54237c6, completed 2026-10-01 22:19:37 UTC, adds the revised sample bounds and gate-doping results. Both are inside this acquisition’s eligible interval [2026-08-24 09:45:15 UTC, 2026-10-17 09:45:15 UTC). Upstream is public and MIT licensed, copyright Antonio Anna Mele; its complete MIT grant is retained in the entry module. Proof provenance is conservatively AI, based on the repository’s Codex-assisted implementation/review documentation and the paper’s AI disclosure.

Scope is the dependency closure of ExactLearningTheorem.exact_learning, including exact_learning_copy_bound_linear: 22 complete upstream modules and the three needed Hadamard coefficient declarations extracted from QubitGates, plus the entry module and generated imports (25 Lean files, 4,684 lines). Tolerant learning/testing, memory testing, low-nullity/tomography, lower bounds, qudit extensions, and unrelated vendor code are excluded. The card claims the proved conservative upper bounds, not optimal constants, classical running time, or all results of the paper. No duplicate was found in pool cards/source/history, public PRs/issues, or the pinned Mathlib/TauCeti source trees.

Ported Lean/Mathlib 4.24 to the pool’s Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. Changes adapt bilinear nondegeneracy, orthogonal dimension, finite sum/PMF and subgroup APIs; use stable two-residue proofs for ZMod 2; remove inherited linter/heartbeat options; generalize unused hypotheses; document public definitions; and use the current public-module layout. The three endpoint theorem signatures are unchanged after namespace normalization. The fixed LeanPool.lean is unchanged. No checks, workflow settings, linter settings, or waivers are changed.

Measured optimization used the same command, lake build LeanPool.SingleCopyStabilizer.Imports, after removing only this project’s build artifacts, with matching dependency oleans warm, on the same shared 16-CPU VM. GNU time results:

Measurement	Port baseline	Optimized closure
Wall time	34.65 s	27.62 s
User CPU	79.00 s	52.93 s
System CPU	15.14 s	12.34 s
Peak RSS	1,826,720 KiB	1,500,496 KiB

Wall time fell 20.3%, user CPU 33.0%, peak RSS 17.9%. Per-file build timings and a Clifford module profiler guided narrower Mathlib imports, a simpler Hadamard covariance proof, removal of the illustrative matrix-only dependency, elimination of unnecessary finiteness assumptions, and reuse of an existing physical-round equivalence proof. Shared-host load limits precision; these are one controlled clean-project run per final configuration, not a statistical benchmark.

Local validation on the final source:

• Project-clean build, warning-free.
• lake exe mk_all --module --check.
• lake exe runLinter LeanPool.SingleCopyStabilizer.Imports.
• lake exe lint-style LeanPool.SingleCopyStabilizer.Imports.
• PYTHONPATH=python python3 -m lean_pool.quality --repo . --static-only.
• The unmodified quality checker’s compiled axiom, option, and registered-declaration audits on this module: 426 public declarations, zero findings. Only Classical.choice, propext, and Quot.sound are allowed; no sorry/admit, unsafe/partial/native evaluation, added axioms, or option escape hatches remain.
• Whitespace validation and all three endpoint signature comparisons pass. A separate Lean audit constructs physical computational-basis states for every qubit count and checks zero/one-qubit and delta=1 boundary instantiations. No Python/workflow files are affected.

CI remains the final authority for full-pool and protected checks. Configured Greptile and GPT reviews and a separate thorough source review are required before any merge eligibility. This PR remains open under the infrastructure priority hold. The latest primary main validation run 39830849898 failed from runner disk exhaustion while packaging, before lint/style/quality. Current main changes only README since that Lean-input-identical revision. This is separate from asynchronous daily documentation publishing. No auto-merge or queue request is enabled. Current-head Greptile is clear; the separate thorough source review approves; remote Lean CI and the explicitly requested GPT review are pending.

[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] The proof-only repair leaves no outstanding review findings.

Summary

Imports exact adaptive single-copy stabilizer learning, connecting Born measurements, Clifford circuits, recovery up to global phase, and explicit resource bounds.

• A finite measurement record now describes recovery of a stabilizer state.
• Adaptive rounds now have a proved confidence-based stopping budget.
• Recorded Clifford gates now have proved resource costs.
• Lean Pool now lists the stabilizer learner as a verified project.

_{Reviews (2) · Last reviewed commit: "Reuse physical-round equivalence in outp..." · Reviewed by Greptile}

[Vilin97]

/review

Please review current head d145590. Local final-source build, linters, style, index, trust and semantic boundary checks pass; CI is running. The one Greptile finding was repaired. This requests review only; the infrastructure priority hold remains in effect and no merge or queue action is authorized by this comment.

[Vilin97]

{
"review_kind": "Separate thorough source review by acquisition agent; author-side audit, not an independent GitHub approval",
"reviewed_commit": "d14559001de1929b3ea16ffcc9719bb5f3782662",
"conclusion": "approve",
"merge_authorized": false,
"coverage": {
"changed_files": 26,
"lean_files": 25,
"lean_lines": 4684,
"source_modules": 23,
"full_diff_read": true,
"all_source_modules_reachable_from_endpoint": true,
"upstream_commit": "d8282e1d59a1a9b8d34396f06298f478c54237c6",
"upstream_scope": "ExactLearningTheorem dependency closure; no tolerant/testing, memory, tomography, vendor, lower-bound or runtime import."
},
"faithfulness": {
"verdict": "pass",
"bottom_line": "Both card results describe the proved physical exact learner and its resource upper bounds.",
"proves_the_claim": "proves_it",
"claim_note": "exact_learning quantifies over normalized pure qubit stabilizer states and 0<delta<=1; at T=ceil(2n+4+8sqrt((2n+4)log(1/delta))+64log(1/delta)), success is at least 1-delta, every supported output has 2T+1 copies and at most (n+1)T^2 elementary gates, and the decoder is normalized. The linear 136(n+log(1/delta)) bound explicitly requires n>=1.",
"assumed_inputs": "PureStabilizerState supplies normalized complex amplitudes and a maximal isotropic space of actual Pauli eigenlabels, which is the input promise in the card. It does not supply measurement uniformity, progress, reconstruction, or the final probability guarantee.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No existing exact single-copy stabilizer-learning endpoint was found in the searched sources.",
"already_formalized": "",
"novelty_note": "Checked pool cards/source/history and public PRs/issues, pinned full module trees and source keyword searches in Mathlib and TauCeti. TauCeti stabilizer hits concern group actions/Clifford representation theory, not quantum-state learning. Negative lexical searches remain bounded evidence rather than a proof that no differently named equivalent theorem exists.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "A completed research-level quantum learning result with reusable mathematical infrastructure.",
"fit": "good_fit",
"level": "research",
"branch": "quantum information",
"mode": "theory_building",
"significance_one_sentence": "Adaptive computational measurements exactly recover arbitrary pure qubit stabilizer states with linear-in-n logarithmic-confidence copy upper bounds, supported by symplectic and finite-probability layers.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The primary paper and pinned MIT source support the scoped exact-learning claim.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Competent layered Lean with concrete physical semantics; the duplicated round proof has been repaired and the measured dependency closure reduced.",
"code_quality": 3,
"findings": []
},
"semantic_evidence": [
{
"file": "LeanPool/SingleCopyStabilizer/StabilizerState.lean",
"line": 42,
"declaration": "PureStabilizerState",
"evidence": "amplitude : Amplitude ι; normalized : IsNormalized amplitude; labels : Submodule (ZMod 2) (Label (ZMod 2) ι); isotropic : IsIsotropic labels; maximal : Module.finrank (ZMod 2) labels = Fintype.card ι; eigenlabels : HasEigenlabels amplitude labels",
"assessment": "Input promise only. A separate compiled audit constructs basisState z for every finite register, so these hypotheses are jointly satisfiable."
},
{
"file": "LeanPool/SingleCopyStabilizer/PhysicalSampling.lean",
"line": 32,
"declaration": "outcomePMF",
"evidence": "(bornDifferencePMF S.amplitude S.normalized).bind fun u => (PMF.uniformOfFintype (ZMod 2)).map fun b => (u, b)",
"assessment": "Two independent Born samples and an independent fair correction bit; outcomePMF_eq_kernel derives the abstract kernel."
},
{
"file": "LeanPool/SingleCopyStabilizer/QuantumRound.lean",
"line": 92,
"declaration": "applyRoundAmplitude",
"evidence": "if hu : u = 0 then ψ else let i := binaryPivot u hu; correctionAmplitude i b (CNOTAction.applyCNOTs i (u - Pi.single i 1) ... ψ)",
"assessment": "Uses observed difference and correction bit, not a stabilizer membership oracle. The abstract safe update is confined to analysis and matches supported physical observations."
},
{
"file": "LeanPool/SingleCopyStabilizer/OutputCorrectness.lean",
"line": 70,
"declaration": "descriptionPMF",
"evidence": "| 0, S => (bornPMF S.amplitude S.normalized).map fun z => ([], z) | t + 1, S => (PhysicalSampling.outcomePMF S).bind fun o => (descriptionPMF t (QuantumRound.quantumRound S o)).map fun d => (o :: d.1, d.2)",
"assessment": "Returned data is a finite outcome list and basis string; unknown amplitudes are absent from the classical output. Decoding inverts the recorded circuit."
},
{
"file": "LeanPool/SingleCopyStabilizer/GeometricDomination.lean",
"line": 174,
"declaration": "failure_probability_le_product",
"evidence": "P.failureProbability t s <= productPotential p lambda (P.rank s) * (1 - lambda) ^ t [rendered ASCII for this review]",
"assessment": "Local progress implies a proved product-potential tail bound. ExactLearning discharges progress from the actual symplectic update; the headline does not assume independent waiting times or the desired tail."
}
],
"boundary_checks": "Compiled explicit basis-state family for every qubit count, zero-qubit/delta=1 endpoint instantiation, and one-qubit linear copy-bound instantiation. General proof handles arbitrarily small positive delta; the linear bound does not claim n=0.",
"source_comparison": "Primary arXiv:2610.02031v1, Theorem II.1/Algorithm 1, compared with actual code. The source chooses a first pivot; Lean uses a fixed classical choice of a nonzero coordinate. This is a valid pivot variant; no classical running-time assertion is made. Larger confidence constants are disclosed. MIT grant, author attribution and conservative AI proof provenance retained.",
"validation": {
"local": "Clean project build, Mathlib linters, style, generated indexes, repository static checks, 426-public-declaration axiom and environment-option audit, endpoint checks and boundary audit pass.",
"compile_cost": "34.65 s baseline to 27.62 s final wall; 79.00 to 52.93 s user CPU; 1,826,720 to 1,500,496 KiB peak RSS. Same clean-project command and warm pinned dependencies on a shared VM. Earlier optimized run 25.77 s illustrates timing variability.",
"remote": "As of 2026-10-24 11:10:48 UTC: Greptile passes at the reviewed head with no outstanding findings; scope workflows pass (inapplicable steps skipped). Lean Action CI is building and advisory Proof Profile is running. GPT review was requested and has not posted a result. Remote validation is not yet complete."
},
"repairs_verified": [
"Port API and option cleanup without changing any of the three headline theorem signatures modulo namespace.",
"Preserved field-general symplectic lemmas and finite-probability abstractions; removed unnecessary hypotheses.",
"Pruned illustrative matrix-only dependency while retaining physical arbitrary-register H/S/CNOT semantics.",
"Replaced repeated OutputCorrectness.roundEquiv_apply proof by QuantumRound.roundEquiv_apply_eq_applyRoundAmplitude; public API unchanged."
],
"remaining_merge_requirements": [
"Finish current-head applicable protected CI and configured GPT review.",
"Infrastructure priority hold remains: primary main Lean Action CI run 39830849898 fails with runner disk exhaustion while packaging, before lint/style/quality. Current main changes only README since that Lean-input-identical revision. This failure is distinct from background daily publishing. No merge, auto-merge, or queue action."
]
}

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 40.38 s (= 0.67 min) — user 74.23 s, sys 15.72 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: 663,442 maxHeartbeats units across 25 valid files (4,684 added LOC).

Sum of lean --profile: 59539.4 ms (= 59.54 s) across 25 valid files. Import-excluded time: 32727.4 ms (= 32.73 s).

Count-heartbeats wall-clock total: 137.35 s. Repeated import cost inside lean --profile: 26812.0 ms (= 26.81 s).

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. 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)	Commands	Errors
LeanPool/SingleCopyStabilizer/CliffordAction.lean	328	90,860	13.66	5.19	4.08	1.11	92	0
LeanPool/SingleCopyStabilizer/StabilizerState.lean	304	85,830	12.21	3.99	2.91	1.08	65	0
LeanPool/SingleCopyStabilizer/Symplectic.lean	303	73,511	8.82	3.46	2.61	0.84	85	0
LeanPool/SingleCopyStabilizer/Projection.lean	192	71,843	7.40	2.54	1.66	0.88	83	0
LeanPool/SingleCopyStabilizer/ExactLearning.lean	267	52,735	7.21	3.20	2.30	0.91	80	0
LeanPool/SingleCopyStabilizer/FiniteProbability.lean	274	45,241	9.59	3.52	2.43	1.09	43	0
LeanPool/SingleCopyStabilizer/GeometricTailBounds.lean	250	37,591	7.43	3.82	2.71	1.11	26	0
LeanPool/SingleCopyStabilizer/Measurement.lean	339	35,641	7.49	2.69	1.58	1.11	89	0
LeanPool/SingleCopyStabilizer/InstructionSemantics.lean	211	22,456	5.26	2.21	1.10	1.11	68	0
LeanPool/SingleCopyStabilizer/Circuit.lean	247	19,943	5.06	2.32	1.20	1.12	74	0
LeanPool/SingleCopyStabilizer/AdaptiveProcess.lean	237	17,783	4.90	2.14	1.48	0.66	28	0
LeanPool/SingleCopyStabilizer/SharpExactLearning.lean	162	16,726	5.54	2.33	1.23	1.10	32	0
LeanPool/SingleCopyStabilizer/QuantumRound.lean	187	16,004	4.23	2.02	0.93	1.09	35	0
LeanPool/SingleCopyStabilizer/ExactResources.lean	213	15,161	3.91	1.90	1.07	0.83	49	0
LeanPool/SingleCopyStabilizer/GeometricDomination.lean	214	14,891	3.39	1.76	1.11	0.65	27	0
LeanPool/SingleCopyStabilizer/OutputCorrectness.lean	231	13,141	3.98	2.09	0.99	1.10	53	0
LeanPool/SingleCopyStabilizer/CNOTAction.lean	98	11,894	4.11	1.79	0.67	1.12	21	0
LeanPool/SingleCopyStabilizer/Round.lean	149	8,164	3.38	1.43	0.59	0.84	36	0
LeanPool/SingleCopyStabilizer/PhysicalSampling.lean	79	5,051	3.23	1.57	0.46	1.11	21	0
LeanPool/SingleCopyStabilizer/PhysicalExactLearning.lean	87	2,688	3.00	1.48	0.37	1.11	16	0
LeanPool/SingleCopyStabilizer/Transcript.lean	108	2,613	2.88	1.49	0.37	1.12	22	0
LeanPool/SingleCopyStabilizer/ExactLearningTheorem.lean	89	2,064	3.17	1.40	0.30	1.10	17	0
LeanPool/SingleCopyStabilizer/HadamardCoefficient.lean	31	1,609	2.52	1.01	0.21	0.80	11	0
LeanPool/SingleCopyStabilizer.lean	52	0	2.31	2.91	0.18	2.73	3	0
LeanPool/SingleCopyStabilizer/Imports.lean	32	0	2.67	1.26	0.17	1.09	1	0
Total	4,684	663,442	137.35	59.54	32.73	26.81	1077	0

Aggregate phase totals

Phase	Time
import	26812.0 ms (= 26.81 s)
typeclass inference	9025.5 ms (= 9.03 s)
interpretation	8638.0 ms (= 8.64 s)
simp	3828.7 ms (= 3.83 s)
tactic execution	3064.1 ms (= 3.06 s)
type checking	1801.6 ms (= 1.80 s)
elaboration	1650.3 ms (= 1.65 s)
norm_num	862.6 ms (= 0.86 s)
initialization	685.0 ms (= 0.69 s)
tacticAnalysis	680.3 ms (= 0.68 s)
ring	460.9 ms (= 0.46 s)
linting	447.6 ms (= 0.45 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.SingleCopyStabilizer.Symplectic	6.90 s
LeanPool.SingleCopyStabilizer.CliffordAction	6.90 s
LeanPool.SingleCopyStabilizer.FiniteProbability	5.70 s
LeanPool.SingleCopyStabilizer.StabilizerState	5.70 s
LeanPool.SingleCopyStabilizer.Measurement	4.80 s
LeanPool.SingleCopyStabilizer.GeometricTailBounds	4.80 s
LeanPool.SingleCopyStabilizer.ExactLearning	3.80 s
LeanPool.SingleCopyStabilizer.Projection	3.70 s
LeanPool.SingleCopyStabilizer.AdaptiveProcess	3.60 s
LeanPool.SingleCopyStabilizer.SharpExactLearning	3.30 s
LeanPool.SingleCopyStabilizer.GeometricDomination	3.20 s
LeanPool.SingleCopyStabilizer.CNOTAction	3.20 s

Per-file `lean --profile` output

LeanPool/SingleCopyStabilizer.lean

import took 2.73s
cumulative profiling times:
	elaboration 0.217ms
	import 2.73s
	initialization 24.7ms
	interpretation 157ms
	linting 0.805ms
	module linting 0.00162ms
	overlappingInstancesLinter 0.224ms
	parsing 0.0486ms
	tacticAnalysis 1.67ms
real 3.53
user 1.06
sys 1.03

LeanPool/SingleCopyStabilizer/AdaptiveProcess.lean

import took 659ms
cumulative profiling times:
	attribute application 0.237ms
	blocked (unaccounted) 55.7ms
	compilation (IR) 0.444ms
	compilation (LCNF base) 9.41ms
	compilation (LCNF impure) 2.12ms
	compilation (LCNF mono) 4.52ms
	congr simp thm 5.32ms
	elaboration 55.3ms
	fix level params 1.54ms
	import 659ms
	initialization 32.5ms
	instantiate metavars 1.35ms
	interpretation 436ms
	let-to-have transformation 0.215ms
	linting 23.9ms
	module linting 0.00146ms
	norm_num 64.6ms
	overlappingInstancesLinter 7.89ms
	parsing 12.9ms
	process pre-definitions 12.6ms
	ring 33.5ms
	share common exprs 9.35ms
	simp 123ms
	tactic execution 154ms
	tacticAnalysis 33.4ms
	type checking 107ms
	typeclass inference 292ms
real 1.78
user 1.86
sys 0.75

LeanPool/SingleCopyStabilizer/CNOTAction.lean

import took 1.12s
cumulative profiling times:
	attribute application 0.0783ms
	compilation (IR) 0.37ms
	compilation (LCNF base) 11.6ms
	compilation (LCNF impure) 1.7ms
	compilation (LCNF mono) 6.95ms
	congr simp thm 3.3ms
	elaboration 30.8ms
	fix level params 0.441ms
	import 1.12s
	initialization 31.3ms
	instantiate metavars 0.422ms
	interpretation 209ms
	let-to-have transformation 0.125ms
	linting 8.09ms
	module linting 0.0014ms
	norm_num 0.215ms
	overlappingInstancesLinter 4.56ms
	parsing 5.15ms
	process pre-definitions 3.05ms
	ring 5.47ms
	share common exprs 1.52ms
	simp 54.3ms
	tactic execution 69.3ms
	tacticAnalysis 16ms
	type checking 30.7ms
	typeclass inference 177ms
real 2.22
user 1.59
sys 0.87

LeanPool/SingleCopyStabilizer/Circuit.lean

import took 1.12s
cumulative profiling times:
	attribute application 38.5ms
	compilation (IR) 0.199ms
	compilation (LCNF base) 2.92ms
	compilation (LCNF impure) 0.76ms
	compilation (LCNF mono) 1.8ms
	congr simp thm 11.1ms
	elaboration 196ms
	fix level params 2.08ms
	import 1.12s
	initialization 24.9ms
	instantiate metavars 1.28ms
	interpretation 298ms
	let-to-have transformation 0.568ms
	linting 24.6ms
	module linting 0.00157ms
	overlappingInstancesLinter 12.8ms
	parsing 14.3ms
	process pre-definitions 16.1ms
	share common exprs 6.01ms
	simp 123ms
	tactic execution 93.9ms
	tacticAnalysis 43ms
	type checking 69ms
	typeclass inference 216ms
real 2.25
user 2.08
sys 0.92

LeanPool/SingleCopyStabilizer/CliffordAction.lean

import took 1.11s
cumulative profiling times:
	attribute application 0.669ms
	blocked (unaccounted) 195ms
	compilation (IR) 0.475ms
	compilation (LCNF base) 9.12ms
	compilation (LCNF impure) 2.23ms
	compilation (LCNF mono) 5.2ms
	congr simp thm 16.6ms
	elaboration 117ms
	fix level params 3.21ms
	import 1.11s
	initialization 25.1ms
	instantiate metavars 4.46ms
	interpretation 954ms
	let-to-have transformation 10.2ms
	linting 36.6ms
	module linting 0.00144ms
	norm_num 172ms
	overlappingInstancesLinter 11.6ms
	parsing 16.7ms
	process pre-definitions 22.8ms
	ring 67.7ms
	share common exprs 21.1ms
	simp 363ms
	tactic execution 157ms
	tacticAnalysis 54.8ms
	type checking 114ms
	typeclass inference 1.7s
real 3.42
user 4.67
sys 0.94

LeanPool/SingleCopyStabilizer/ExactLearning.lean

import took 909ms
simp took 126ms
cumulative profiling times:
	attribute application 0.247ms
	congr simp thm 6.59ms
	dsimp 1.71ms
	elaboration 108ms
	fix level params 3.93ms
	import 909ms
	initialization 25.3ms
	instantiate metavars 3.51ms
	interpretation 364ms
	let-to-have transformation 0.63ms
	linting 23.7ms
	module linting 0.00154ms
	norm_num 20.2ms
	overlappingInstancesLinter 10.3ms
	parsing 15.6ms
	process pre-definitions 16.6ms
	ring 9.01ms
	share common exprs 14.2ms
	simp 384ms
	tactic execution 343ms
	tacticAnalysis 37.2ms
	type checking 299ms
	typeclass inference 609ms
real 2.35
user 3.03
sys 0.82

LeanPool/SingleCopyStabilizer/ExactLearningTheorem.lean

import took 1.1s
cumulative profiling times:
	attribute application 0.0338ms
	dsimp 3.13ms
	elaboration 23ms
	fix level params 0.201ms
	import 1.1s
	initialization 24.4ms
	instantiate metavars 0.0925ms
	interpretation 188ms
	let-to-have transformation 1.98ms
	linting 4.97ms
	module linting 0.00149ms
	overlappingInstancesLinter 2.31ms
	parsing 3.46ms
	process pre-definitions 1.09ms
	share common exprs 0.605ms
	tactic execution 11.1ms
	tacticAnalysis 11.1ms
	type checking 2.84ms
	typeclass inference 26ms
real 1.95
user 1.20
sys 0.85

LeanPool/SingleCopyStabilizer/ExactResources.lean

import took 831ms
cumulative profiling times:
	attribute application 1.49ms
	blocked (unaccounted) 0.856ms
	compilation (IR) 0.278ms
	compilation (LCNF base) 2.99ms
	compilation (LCNF impure) 1.4ms
	compilation (LCNF mono) 3.93ms
	congr simp thm 9.29ms
	elaboration 58.9ms
	fix level params 1.32ms
	import 831ms
	initialization 24.1ms
	instantiate metavars 1.12ms
	interpretation 368ms
	let-to-have transformation 0.48ms
	linting 16.6ms
	module linting 0.00143ms
	norm_num 6.82ms
	overlappingInstancesLinter 11.7ms
	parsing 11.5ms
	process pre-definitions 7.97ms
	ring 28.5ms
	share common exprs 5.6ms
	simp 132ms
	tactic execution 58.3ms
	tacticAnalysis 28.4ms
	type checking 60.2ms
	typeclass inference 230ms
real 1.88
user 1.72
sys 0.81

LeanPool/SingleCopyStabilizer/FiniteProbability.lean

import took 1.09s
cumulative profiling times:
	attribute application 0.21ms
	blocked (unaccounted) 0.418ms
	compilation (IR) 0.131ms
	compilation (LCNF base) 2.47ms
	compilation (LCNF impure) 0.593ms
	compilation (LCNF mono) 1.26ms
	congr simp thm 7.57ms
	elaboration 74.4ms
	fix level params 2.27ms
	import 1.09s
	initialization 28.9ms
	instantiate metavars 2.77ms
	interpretation 743ms
	let-to-have transformation 0.314ms
	linting 24.3ms
	module linting 0.00148ms
	norm_num 173ms
	overlappingInstancesLinter 9.44ms
	parsing 16.1ms
	process pre-definitions 17.3ms
	ring 56.1ms
	share common exprs 18.4ms
	simp 172ms
	tactic execution 181ms
	tacticAnalysis 38.4ms
	type checking 113ms
	typeclass inference 750ms
real 2.68
user 3.21
sys 0.94

LeanPool/SingleCopyStabilizer/GeometricDomination.lean

import took 650ms
cumulative profiling times:
	attribute application 0.379ms
	congr simp thm 2.02ms
	elaboration 47.2ms
	fix level params 1.15ms
	import 650ms
	initialization 24.7ms
	instantiate metavars 1.55ms
	interpretation 381ms
	let-to-have transformation 0.175ms
	linting 17.2ms
	module linting 0.0015ms
	norm_num 20.5ms
	overlappingInstancesLinter 4.78ms
	parsing 11.7ms
	process pre-definitions 8.81ms
	ring 40.2ms
	share common exprs 9.51ms
	simp 95.8ms
	tactic execution 91.6ms
	tacticAnalysis 32.4ms
	type checking 85.6ms
	typeclass inference 229ms
real 1.71
user 1.62
sys 0.75

LeanPool/SingleCopyStabilizer/GeometricTailBounds.lean

import took 1.11s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 104ms
cumulative profiling times:
	attribute application 0.182ms
	congr simp thm 1.68ms
	elaboration 87.4ms
	fix level params 2.69ms
	import 1.11s
	initialization 28.9ms
	instantiate metavars 4.42ms
	interpretation 976ms
	let-to-have transformation 0.367ms
	linting 46.1ms
	module linting 0.00161ms
	norm_num 264ms
	overlappingInstancesLinter 5.1ms
	parsing 17.5ms
	process pre-definitions 28.1ms
	ring 123ms
	share common exprs 35.6ms
	simp 36.8ms
	tactic execution 222ms
	tacticAnalysis 43.9ms
	type checking 159ms
	typeclass inference 625ms
real 2.58
user 3.49
sys 0.93

LeanPool/SingleCopyStabilizer/HadamardCoefficient.lean

import took 802ms
cumulative profiling times:
	attribute application 0.187ms
	congr simp thm 0.337ms
	elaboration 4ms
	fix level params 0.0587ms
	import 802ms
	initialization 25.1ms
	instantiate metavars 0.0194ms
	interpretation 139ms
	let-to-have transformation 0.0257ms
	linting 1.98ms
	module linting 0.00137ms
	norm_num 4.3ms
	overlappingInstancesLinter 0.839ms
	parsing 1.26ms
	process pre-definitions 0.713ms
	share common exprs 0.41ms
	simp 5.31ms
	tactic execution 3.45ms
	tacticAnalysis 4.94ms
	type checking 3.53ms
	typeclass inference 14.2ms
real 1.58
user 0.87
sys 0.79

LeanPool/SingleCopyStabilizer/Imports.lean

import took 1.09s
cumulative profiling times:
	elaboration 0.0884ms
	import 1.09s
	initialization 28.5ms
	interpretation 143ms
	linting 0.204ms
	module linting 0.00147ms
	overlappingInstancesLinter 0.096ms
	parsing 0.00185ms
	tacticAnalysis 0.368ms
real 1.88
user 1.05
sys 0.87

LeanPool/SingleCopyStabilizer/InstructionSemantics.lean

import took 1.11s
cumulative profiling times:
	attribute application 1.72ms
	blocked (unaccounted) 0.154ms
	compilation (IR) 0.266ms
	compilation (LCNF base) 3.01ms
	compilation (LCNF impure) 1.41ms
	compilation (LCNF mono) 4.61ms
	congr simp thm 5.52ms
	elaboration 68.4ms
	fix level params 1.9ms
	import 1.11s
	initialization 25ms
	instantiate metavars 1.74ms
	interpretation 252ms
	let-to-have transformation 0.284ms
	linting 16.8ms
	module linting 0.00149ms
	norm_num 0.236ms
	overlappingInstancesLinter 7.13ms
	parsing 10.1ms
	process pre-definitions 11.4ms
	ring 3.61ms
	share common exprs 5.26ms
	simp 168ms
	tactic execution 164ms
	tacticAnalysis 28.1ms
	type checking 50.8ms
	typeclass inference 271ms
real 2.25
user 1.99
sys 0.87

LeanPool/SingleCopyStabilizer/Measurement.lean

import took 1.11s
cumulative profiling times:
	attribute application 3.27ms
	compilation (IR) 0.366ms
	compilation (LCNF base) 8.74ms
	compilation (LCNF impure) 1.56ms
	compilation (LCNF mono) 3.96ms
	congr simp thm 4.2ms
	dsimp 6.88ms
	elaboration 99ms
	fix level params 1.41ms
	import 1.11s
	initialization 28.9ms
	instantiate metavars 1.09ms
	interpretation 366ms
	let-to-have transformation 0.39ms
	linting 33ms
	module linting 0.00151ms
	norm_num 10.3ms
	overlappingInstancesLinter 11.4ms
	parsing 18.1ms
	process pre-definitions 10.1ms
	ring 1.58ms
	share common exprs 4.69ms
	simp 104ms
	tactic execution 124ms
	tacticAnalysis 46.6ms
	type checking 56.3ms
	typeclass inference 639ms
real 2.56
user 2.41
sys 0.94

LeanPool/SingleCopyStabilizer/OutputCorrectness.lean

import took 1.1s
cumulative profiling times:
	attribute application 0.193ms
	blocked (unaccounted) 28.9ms
	compilation (IR) 0.167ms
	compilation (LCNF base) 1.33ms
	compilation (LCNF impure) 0.609ms
	compilation (LCNF mono) 0.908ms
	congr simp thm 5.13ms
	elaboration 61.8ms
	fix level params 1.46ms
	import 1.1s
	initialization 24.8ms
	instantiate metavars 1.37ms
	interpretation 283ms
	let-to-have transformation 0.266ms
	linting 18.2ms
	module linting 0.00175ms
	norm_num 0.801ms
	overlappingInstancesLinter 8.61ms
	parsing 11ms
	process pre-definitions 12.9ms
	ring 6.25ms
	share common exprs 4.18ms
	simp 77.7ms
	tactic execution 194ms
	tacticAnalysis 29.6ms
	type checking 34.7ms
	typeclass inference 178ms
real 2.12
user 1.77
sys 0.90

LeanPool/SingleCopyStabilizer/PhysicalExactLearning.lean

import took 1.11s
cumulative profiling times:
	attribute application 0.0562ms
	congr simp thm 0.808ms
	elaboration 20.9ms
	fix level params 0.401ms
	import 1.11s
	initialization 24.7ms
	instantiate metavars 0.215ms
	interpretation 199ms
	let-to-have transformation 0.0798ms
	linting 6.76ms
	module linting 0.00156ms
	overlappingInstancesLinter 3.72ms
	parsing 3.33ms
	process pre-definitions 3.77ms
	share common exprs 0.937ms
	simp 5.02ms
	tactic execution 39.5ms
	tacticAnalysis 11.8ms
	type checking 13.1ms
	typeclass inference 35.7ms
real 1.98
user 1.27
sys 0.87

LeanPool/SingleCopyStabilizer/PhysicalSampling.lean

import took 1.11s
cumulative profiling times:
	attribute application 0.0564ms
	compilation (IR) 0.057ms
	compilation (LCNF base) 1.2ms
	compilation (LCNF impure) 0.264ms
	compilation (LCNF mono) 1.28ms
	congr simp thm 2.43ms
	dsimp 1.92ms
	elaboration 23ms
	fix level params 0.643ms
	import 1.11s
	initialization 30.6ms
	instantiate metavars 0.336ms
	interpretation 204ms
	let-to-have transformation 0.0967ms
	linting 8ms
	module linting 0.00167ms
	norm_num 1.61ms
	overlappingInstancesLinter 4.08ms
	parsing 2.99ms
	process pre-definitions 3.61ms
	ring 3.68ms
	share common exprs 1.93ms
	simp 49.2ms
	tactic execution 44.8ms
	tacticAnalysis 12.3ms
	type checking 23.5ms
	typeclass inference 41.8ms
real 2.01
user 1.33
sys 0.89

LeanPool/SingleCopyStabilizer/Projection.lean

import took 880ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 231ms
cumulative profiling times:
	attribute application 1.7ms
	compilation (IR) 0.298ms
	compilation (LCNF base) 6.88ms
	compilation (LCNF impure) 1.3ms
	compilation (LCNF mono) 3.85ms
	congr simp thm 2.86ms
	elaboration 85ms
	fix level params 2.47ms
	import 880ms
	initialization 24.7ms
	instantiate metavars 1.7ms
	interpretation 198ms
	let-to-have transformation 0.419ms
	linting 16.5ms
	module linting 0.00144ms
	overlappingInstancesLinter 10.1ms
	parsing 8.57ms
	process pre-definitions 11.5ms
	share common exprs 5.01ms
	simp 89.6ms
	tactic execution 470ms
	tacticAnalysis 25.4ms
	type checking 139ms
	typeclass inference 559ms
real 2.27
user 2.36
sys 0.80

LeanPool/SingleCopyStabilizer/QuantumRound.lean

import took 1.09s
cumulative profiling times:
	attribute application 11.7ms
	congr simp thm 14.5ms
	elaboration 90.4ms
	fix level params 1.14ms
	import 1.09s
	initialization 31.3ms
	instantiate metavars 0.732ms
	interpretation 237ms
	let-to-have transformation 0.995ms
	linting 14.1ms
	module linting 0.00143ms
	overlappingInstancesLinter 6.42ms
	parsing 8.23ms
	process pre-definitions 7.06ms
	share common exprs 2.67ms
	simp 115ms
	tactic execution 54.8ms
	tacticAnalysis 24.6ms
	type checking 32.9ms
	typeclass inference 281ms
real 2.08
user 1.77
sys 0.89

LeanPool/SingleCopyStabilizer/Round.lean

import took 837ms
cumulative profiling times:
	attribute application 0.593ms
	congr simp thm 0.386ms
	elaboration 55.5ms
	fix level params 0.909ms
	import 837ms
	initialization 25.1ms
	instantiate metavars 0.594ms
	interpretation 190ms
	let-to-have transformation 0.327ms
	linting 17.2ms
	module linting 0.0014ms
	overlappingInstancesLinter 6.61ms
	parsing 6.78ms
	process pre-definitions 5.53ms
	share common exprs 2.44ms
	simp 0.626ms
	tactic execution 102ms
	tacticAnalysis 22.5ms
	type checking 50.3ms
	typeclass inference 101ms
real 1.72
user 1.25
sys 0.80

LeanPool/SingleCopyStabilizer/SharpExactLearning.lean

import took 1.1s
cumulative profiling times:
	attribute application 0.117ms
	compilation (IR) 0.221ms
	compilation (LCNF base) 5.52ms
	compilation (LCNF impure) 0.903ms
	compilation (LCNF mono) 1.58ms
	congr simp thm 2.09ms
	dsimp 1.72ms
	elaboration 45ms
	fix level params 1.14ms
	import 1.1s
	initialization 40.3ms
	instantiate metavars 1.29ms
	interpretation 514ms
	let-to-have transformation 0.23ms
	linting 17.2ms
	module linting 0.00176ms
	norm_num 120ms
	overlappingInstancesLinter 6.74ms
	parsing 8.26ms
	process pre-definitions 8.95ms
	ring 42ms
	share common exprs 11.4ms
	simp 22.1ms
	tactic execution 66ms
	tacticAnalysis 22.6ms
	type checking 63.1ms
	typeclass inference 224ms
real 2.33
user 2.02
sys 0.93

LeanPool/SingleCopyStabilizer/StabilizerState.lean

import took 1.08s
simp took 149ms
simp took 139ms
simp took 128ms
simp took 129ms
cumulative profiling times:
	attribute application 0.376ms
	blocked (unaccounted) 14.9ms
	congr simp thm 11.6ms
	elaboration 114ms
	fix level params 1.96ms
	import 1.08s
	initialization 24.5ms
	instantiate metavars 1.77ms
	interpretation 341ms
	let-to-have transformation 0.487ms
	linting 27.4ms
	module linting 0.0014ms
	norm_num 2.66ms
	overlappingInstancesLinter 6.96ms
	parsing 14.9ms
	process pre-definitions 7.89ms
	ring 4.35ms
	share common exprs 6.61ms
	simp 760ms
	tactic execution 207ms
	tacticAnalysis 42.1ms
	type checking 150ms
	typeclass inference 1.17s
real 3.19
user 3.71
sys 0.91

LeanPool/SingleCopyStabilizer/Symplectic.lean

import took 844ms
simp took 111ms
simp took 116ms
simp took 104ms
cumulative profiling times:
	attribute application 1.73ms
	blocked (unaccounted) 0.309ms
	compilation (IR) 0.701ms
	compilation (LCNF base) 14.8ms
	compilation (LCNF impure) 3.41ms
	compilation (LCNF mono) 15.1ms
	congr simp thm 8.51ms
	dsimp 0.718ms
	elaboration 156ms
	fix level params 3.99ms
	import 844ms
	initialization 24.7ms
	instantiate metavars 2.45ms
	interpretation 294ms
	let-to-have transformation 0.576ms
	linting 35.5ms
	module linting 0.00158ms
	norm_num 1.31ms
	overlappingInstancesLinter 23ms
	parsing 18.9ms
	process pre-definitions 15.8ms
	ring 35.9ms
	share common exprs 9.36ms
	simp 940ms
	tactic execution 189ms
	tacticAnalysis 54.3ms
	type checking 139ms
	typeclass inference 622ms
real 2.91
user 3.30
sys 0.80

LeanPool/SingleCopyStabilizer/Transcript.lean

import took 1.12s
cumulative profiling times:
	attribute application 0.104ms
	congr simp thm 1.29ms
	elaboration 29ms
	fix level params 0.388ms
	import 1.12s
	initialization 32ms
	instantiate metavars 0.443ms
	interpretation 204ms
	let-to-have transformation 0.095ms
	linting 7.92ms
	module linting 0.00134ms
	overlappingInstancesLinter 3.92ms
	parsing 4.97ms
	process pre-definitions 1.72ms
	share common exprs 0.94ms
	simp 8.2ms
	tactic execution 24.3ms
	tacticAnalysis 14.8ms
	type checking 5.01ms
	typeclass inference 34.8ms
real 1.98
user 1.24
sys 0.90

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