Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Reduced circuits are rigid

Lax461425.ReducedRigid · concepts/Lax461425/ReducedRigid.lean · lax-461425

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Every reduced matrix-symmetric circuit is rigid.

    Two circuit automorphisms extending the same element of Γn\Gamma_n differ by a circuit automorphism ρ\rho that fixes all input gates, since input labels are distinct. By induction on the height, ρ\rho fixes every gate gg: the gate ρ(g)\rho(g) has the same label and the same multiset of children as gg, so ρ(g)=g\rho(g) = g as CC is reduced.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax461425.MatrixSymmetry
    2
    3/-!
    4---
    5title: Reduced circuits are rigid
    6type: lemma
    7---
    8Every reduced matrix-symmetric circuit is rigid.
    9
    10Two circuit automorphisms extending the same element of Γn\Gamma_n differ by a circuit
    11automorphism ρ\rho that fixes all input gates, since input labels are distinct. By induction
    12on the height, ρ\rho fixes every gate gg: the gate ρ(g)\rho(g) has the same label and the same
    13multiset of children as gg, so ρ(g)=g\rho(g) = g as CC is reduced.
    14-/
    15
    16namespace Lax461425.ReducedRigid
    17
    18open Circuits MatrixSymmetry
    19
    20/-- Every reduced matrix-symmetric circuit is rigid. -/
    21axiom isRigid {K : Type*} {n : ℕ} (C : Circuit (Fin n × Fin n) K)
    22 (hsym : IsMatrixSymmetric C) (hred : C.IsReduced) : IsRigid C
    23
    24end Lax461425.ReducedRigid
    25
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…