Quantum and Circuits: DegreeChecks: 8 declarations

Verification statements describe the retained edition and its recorded evidence. This HTML presentation adds no Lean execution or proof review.

DegreeChecks: 8 declarations

On this page · Permalink · Source line 1561

L108 squareParity_add

On this page · Permalink · Source line 1563

Source. CircuitObstructions/DegreeChecks.lean:17
Block. 02 Axioms. propext

Permalink · Source line 1564

CircuitObstructions.squareParity_add (f g : CircuitObstructions.BFun 2) :
  (CircuitObstructions.squareParity fun x => f x ^^ g x) =
    (CircuitObstructions.squareParity f ^^ CircuitObstructions.squareParity g)

Permalink · Source line 1566

L109 affine_squareParity_zero

On this page · Permalink · Source line 1574

Source. CircuitObstructions/DegreeChecks.lean:22
Block. 02 Axioms. propext, Quot.sound

Permalink · Source line 1575

CircuitObstructions.affine_squareParity_zero (f : CircuitObstructions.BFun 2) (h : CircuitObstructions.DegreeLE 1 f) :
  CircuitObstructions.squareParity f = false

Permalink · Source line 1577

L110 andTwo_degree_two

On this page · Permalink · Source line 1584

Source. CircuitObstructions/DegreeChecks.lean:39
Block. 02 Axioms. propext, Quot.sound

Permalink · Source line 1585

CircuitObstructions.andTwo_degree_two : CircuitObstructions.DegreeLE 2 CircuitObstructions.andTwo

Permalink · Source line 1587

L111 andTwo_not_affine

On this page · Permalink · Source line 1593

Source. CircuitObstructions/DegreeChecks.lean:43
Block. 02 Axioms. propext, Quot.sound

Permalink · Source line 1594

CircuitObstructions.andTwo_not_affine : ¬CircuitObstructions.DegreeLE 1 CircuitObstructions.andTwo

Permalink · Source line 1596

L112 andTwo_no_degree_one_safe_cover

On this page · Permalink · Source line 1602

Source. CircuitObstructions/DegreeChecks.lean:49
Block. 02 Axioms. propext, Quot.sound

Permalink · Source line 1603

CircuitObstructions.andTwo_no_degree_one_safe_cover :
  ¬CircuitObstructions.CompleteSafeDegreeLE CircuitObstructions.andTwo 1

Permalink · Source line 1605

L113 beta_andTwo

On this page · Permalink · Source line 1612

Source. CircuitObstructions/DegreeChecks.lean:64
Block. 02 Axioms. propext, Classical.choice, Quot.sound

Permalink · Source line 1613

CircuitObstructions.beta_andTwo : CircuitObstructions.beta CircuitObstructions.andTwo = 2

Permalink · Source line 1615

L114 betaStar_andTwo

On this page · Permalink · Source line 1621

Source. CircuitObstructions/DegreeChecks.lean:72
Block. 02 Axioms. propext, Classical.choice, Quot.sound

Permalink · Source line 1622

CircuitObstructions.betaStar_andTwo : CircuitObstructions.betaStar CircuitObstructions.andTwo = 2

Permalink · Source line 1624

L115 restored_andTwo_needs_toffoli

On this page · Permalink · Source line 1630

Source. CircuitObstructions/DegreeChecks.lean:78
Block. 02 Axioms. propext, Classical.choice, Quot.sound

Permalink · Source line 1631

CircuitObstructions.restored_andTwo_needs_toffoli (a : Nat)
  (c : CircuitObstructions.Circuit (CircuitObstructions.CanonicalWire 2 a))
  (hR : CircuitObstructions.Restores (CircuitObstructions.canonicalBoundary 2 a) c CircuitObstructions.andTwo) :
  1 ≤ CircuitObstructions.toffoliCount c

Permalink · Source line 1633

Source and conversion record

Source SHA-256: 36eb83548efd74b42264ab400e359c2de20c701b436b132b8b2859312d2dcdba

Unsupported prose commands stop the build. The mathematical expression sequence is checked against the source, with manuscript macros expanded for display.

Conversion records

Read and explore

Proofs and implementation

About this work

Other resources