Examples: 11 declarations
On this page · Permalink · Source line 716
L030 andOracle_restores
On this page · Permalink · Source line 718
Source. CircuitObstructions/Examples.lean:27
Block. 01 Axioms. Quot.sound
CircuitObstructions.Examples.andOracle_restores :
CircuitObstructions.Restores CircuitObstructions.Examples.andBoundary CircuitObstructions.Examples.andOracle fun x =>
x.fst && x.sndL031 andOracle_toffoli_count
On this page · Permalink · Source line 729
Source. CircuitObstructions/Examples.lean:33
Block. 01 Axioms. propext
CircuitObstructions.Examples.andOracle_toffoli_count :
CircuitObstructions.toffoliCount CircuitObstructions.Examples.andOracle = 2L032 and_scratch_can_be_dirty
On this page · Permalink · Source line 739
Source. CircuitObstructions/Examples.lean:36
Block. 01 Axioms. none
CircuitObstructions.Examples.and_scratch_can_be_dirty :
CircuitObstructions.run CircuitObstructions.Examples.andCompute
(CircuitObstructions.Examples.andBoundary.encode (true, true) false)
CircuitObstructions.Examples.WorkWire.scratch =
trueL033 andOracle_every_cut
On this page · Permalink · Source line 752
Source. CircuitObstructions/Examples.lean:40
Block. 01 Axioms. propext, Classical.choice, Quot.sound
CircuitObstructions.Examples.andOracle_every_cut (k : Nat) (x : Bool × Bool) :
(x.fst && x.snd) = true ↔
∃ i,
CircuitObstructions.packet CircuitObstructions.Examples.andBoundary
(List.take k CircuitObstructions.Examples.andOracle) (List.drop k CircuitObstructions.Examples.andOracle) x
i =
trueL034 outputActiveOracle_restores
On this page · Permalink · Source line 767
Source. CircuitObstructions/Examples.lean:66
Block. 01 Axioms. Quot.sound
CircuitObstructions.Examples.outputActiveOracle_restores :
CircuitObstructions.Restores CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.outputActiveOracle
fun x => trueL035 outputActiveOracle_length
On this page · Permalink · Source line 778
Source. CircuitObstructions/Examples.lean:71
Block. 01 Axioms. none
CircuitObstructions.Examples.outputActiveOracle_length : List.length CircuitObstructions.Examples.outputActiveOracle = 7L036 outputActiveOracle_toffoli_count
On this page · Permalink · Source line 787
Source. CircuitObstructions/Examples.lean:73
Block. 01 Axioms. propext
CircuitObstructions.Examples.outputActiveOracle_toffoli_count :
CircuitObstructions.toffoliCount CircuitObstructions.Examples.outputActiveOracle = 0L037 moved_discrepancy_data
On this page · Permalink · Source line 797
Source. CircuitObstructions/Examples.lean:76
Block. 01 Axioms. none
CircuitObstructions.Examples.moved_discrepancy_data (x : Bool) :
CircuitObstructions.packet CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.swapCircuit
CircuitObstructions.Examples.swapSuffix x CircuitObstructions.Examples.SwapWire.data =
trueL038 moved_discrepancy_target
On this page · Permalink · Source line 809
Source. CircuitObstructions/Examples.lean:80
Block. 01 Axioms. none
CircuitObstructions.Examples.moved_discrepancy_target (x : Bool) :
CircuitObstructions.packet CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.swapCircuit
CircuitObstructions.Examples.swapSuffix x CircuitObstructions.Examples.SwapWire.target =
falseL039 target_only_reconstruction_is_false
On this page · Permalink · Source line 821
Source. CircuitObstructions/Examples.lean:85
Block. 01 Axioms. none
CircuitObstructions.Examples.target_only_reconstruction_is_false :
¬∀ (x : Bool),
CircuitObstructions.packet CircuitObstructions.Examples.swapBoundary CircuitObstructions.Examples.swapCircuit
CircuitObstructions.Examples.swapSuffix x CircuitObstructions.Examples.SwapWire.target =
trueL040 degenerate_encoding_control
On this page · Permalink · Source line 834
Source. CircuitObstructions/Examples.lean:93
Block. 01 Axioms. none
CircuitObstructions.Examples.degenerate_encoding_control :
have bad := fun x x_1 => false;
(∀ (y : Bool), CircuitObstructions.run [] (bad y) = bad (y ^^ true)) ∧
∀ (i : CircuitObstructions.Examples.SwapWire), (bad false i ^^ bad false i) = false