### Abstract

Linear algebraic techniques are powerful, yet often underrated tools in combinatorial proofs. This formalisation provides a library including matrix representations of incidence set systems, general formal proof techniques for the rank argument and linear bound argument, and finally a formalisation of a number of variations of the well-known Fisher's inequality. We build on our prior work formalising combinatorial design theory using a locale-centric approach, including extensions such as constant intersect designs and dual incidence systems. In addition to Fisher's inequality, we also formalise proofs on other incidence system properties using the incidence matrix representation, such as design existence, dual system relationships and incidence system isomorphisms. This formalisation is presented in the paper "Formalising Fisher's Inequality: Formal Linear Algebraic Techniques in Combinatorics", accepted to ITP 2022.

### License

BSD License

### Topics

- Mathematics/Combinatorics
- Mathematics/Algebra

### Session Fishers_Inequality

- Set_Multiset_Extras
- Matrix_Vector_Extras
- Design_Extras
- Incidence_Matrices
- Dual_Systems
- Rank_Argument_General
- Linear_Bound_Argument
- Fishers_Inequality
- Vector_Matrix_Mod
- Fishers_Inequality_Variations
- Fishers_Inequality_Root

### Depends on

- The BKR Decision Procedure for Univariate Real Arithmetic
- The Factorization Algorithm of Berlekamp and Zassenhaus
- Combinatorial Design Theory
- Gröbner Bases Theory
- List Index
- Polynomial Factorization

### Used by

- Hypergraphs

## Cite

×

Fishers_Inequality-AFP

    @article{Fishers_Inequality-AFP,
      author  = {Chelsea Edmonds and Lawrence C. Paulson},
      title   = {Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Fishers_Inequality.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jun 19, 2022 : Isabelle2021-1
- Apr 29, 2022 : Isabelle2021-1