Quantum and Circuits · Lean sources

Quantum and Circuits

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Source files 29

Source locations and editions

Files are shown relative to verification/.

Historical editions keep their original paths. Package caches and build files are omitted.

29 files

Audit.leancircuits_fresh_20261026/fresh_source/
248 lines · 0 declaration locations
CircuitObstructions.leancircuits_fresh_20261026/fresh_source/
8 lines · 0 declaration locations
AffineOutput.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
148 lines · 17 declaration locations
CutComparison.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
149 lines · 19 declaration locations
Degree.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
150 lines · 23 declaration locations
DegreeChecks.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
85 lines · 11 declaration locations
Examples.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
99 lines · 21 declaration locations
Gates.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
122 lines · 24 declaration locations
MultiplicativeDegree.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
171 lines · 15 declaration locations
SafeDegree.leancircuits_fresh_20261026/fresh_source/CircuitObstructions/
193 lines · 25 declaration locations
false_affine_and.leancircuits_fresh_20261026/fresh_source/negative/
3 lines · 0 declaration locations
false_betaStar_bound.leancircuits_fresh_20261026/fresh_source/negative/
3 lines · 0 declaration locations
false_beta_bound.leancircuits_fresh_20261026/fresh_source/negative/
3 lines · 0 declaration locations
false_monomial_degree.leancircuits_fresh_20261026/fresh_source/negative/
3 lines · 0 declaration locations
false_statement.leancircuits_fresh_20261026/fresh_source/negative/
2 lines · 0 declaration locations
illegal_repeated_wire.leancircuits_fresh_20261026/fresh_source/negative/
3 lines · 1 declaration location
placeholder_guard.leancircuits_fresh_20261026/fresh_source/negative/
2 lines · 0 declaration locations
target_only_claim.leancircuits_fresh_20261026/fresh_source/negative/
3 lines · 0 declaration locations
AxiomAudit.leanquantum_fresh_20261026/fresh/
193 lines · 0 declaration locations
Conventions.leanquantum_fresh_20261026/fresh/
120 lines · 17 declaration locations
FiniteFourier.leanquantum_fresh_20261026/fresh/
128 lines · 38 declaration locations
Publication.leanquantum_fresh_20261026/fresh/
82 lines · 10 declaration locations
QuantumArithmeticBridge.leanquantum_fresh_20261026/fresh/
268 lines · 55 declaration locations
QuantumFourierRefutation.leanquantum_fresh_20261026/fresh/
18 lines · 2 declaration locations
SemanticBridge.leanquantum_fresh_20261026/fresh/
191 lines · 41 declaration locations
AdmittedProof.leanquantum_fresh_20261026/fresh/negative_controls/
3 lines · 0 declaration locations
FalseFourierMode.leanquantum_fresh_20261026/fresh/negative_controls/
4 lines · 0 declaration locations
FalseFourierModeExplicit.leanquantum_fresh_20261026/fresh/negative_controls/
5 lines · 0 declaration locations
FalseSignalSign.leanquantum_fresh_20261026/fresh/negative_controls/
4 lines · 0 declaration locations