Quantum and Circuits · Lean source

CircuitObstructions.lean

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.

circuits_fresh_20261026/fresh_source/CircuitObstructions.lean8 lines

Original source path

verification/circuits_fresh_20261026/fresh_source/CircuitObstructions.lean

1 import CircuitObstructions.Gates
2 import CircuitObstructions.CutComparison
3 import CircuitObstructions.Examples
4 import CircuitObstructions.Degree
5 import CircuitObstructions.MultiplicativeDegree
6 import CircuitObstructions.SafeDegree
7 import CircuitObstructions.AffineOutput
8 import CircuitObstructions.DegreeChecks

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: db92393f60a80af88c5cc7b4df2a2297630f295d760d86603e3a4ee74db2ccd5

Original source on GitHub

Back to Quantum and Circuits