Add the Shearer–Kleitman conjecture on orthogonal symmetric chain decompositions

### What is the conjecture

The n-cube is the poset of all subsets of `{1, …, n}` ordered by inclusion. It can be partitioned into `binom(n, ⌊n/2⌋)` chains, which is the minimum possible number (the width of the poset, by Sperner's theorem). A partition into that many *symmetric* chains (each chain spanning levels symmetric about the middle) is a symmetric chain decomposition (SCD). Two SCDs are called orthogonal if any chain of the one and any chain of the other share at most a single element.

The Shearer–Kleitman conjecture (1979) states that the n-cube has `⌊n/2⌋ + 1` pairwise orthogonal symmetric chain decompositions. Shearer and Kleitman constructed two of them. The best known bounds are four pairwise orthogonal SCDs for `n ≥ 60` and five pairwise edge-disjoint ones for `n ≥ 90`, due to Däubel, Jäger, Mütze and Scheucher. The conjecture is still open.

References:
- J. B. Shearer and D. J. Kleitman, *Probabilities of independent choices being ordered*, Studies in Applied Mathematics 60 (1979), 271–276.
- R. Däubel, S. Jäger, T. Mütze and M. Scheucher, [*On orthogonal symmetric chain decompositions*](https://doi.org/10.37236/8531), Electronic Journal of Combinatorics 26(3) (2019), no. P3.64.
- [Symmetric chain decomposition (Wikipedia)](https://en.wikipedia.org/wiki/Symmetric_chain_decomposition)

### Prerequisites needed

None beyond the statement itself. The formalization is purely combinatorial (subsets of `Fin n` as `Finset`, chains, and decompositions), so no addition to `FormalConjecturesForMathlib` and no open Mathlib dependency are needed.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05 Combinatorics
* ams-06 Order, lattices, ordered algebraic structures

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Use the conjecture statement and listed references as the specification; the payload names no repository files, tests, or entry points. Done means adding the Shearer–Kleitman conjecture as a Lean formal statement, including the definitions needed for subsets, chains, symmetric chain decompositions, and orthogonality.

Written by the indexing model from the issue text.