CubicSupport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The common-support step of the cubic classification in §3.

These lemmas concern two three-element supports avoiding coordinate zero. The last theorem states that a quotient having the cubed-value pattern proved for Hadamard row ratios forces the supports to coincide.

def OAI.MUB6.TwoValuePattern line 21
theorem OAI.MUB6.value_pair_exhausts line 27
theorem OAI.MUB6.three_supports_have_witnesses line 41
theorem OAI.MUB6.same_membership_card_ne_three line 74
Source documentation
For two subsets of size three in a six-element set, the number of coordinates on which membership agrees is even, hence cannot be three.
```
theorem same_membership_card_ne_three (S U : Finset (Fin 6))
    (hS : S.card = 3) (hU : U.card = 3) :
    (Finset.univ.filter (fun i => (i ∈ S ↔ i ∈ U))).card ≠ 3 := by
…
```
def OAI.MUB6.supportedValue line 93
def OAI.MUB6.supportedRatio line 96

theorem OAI.MUB6.common_support_of_twoValuePattern line 101

Source documentation

The exact common-support claim: a ratio of two nonconstant cubed rows cannot have the necessary three-and-three multiplicities on distinct supports.

theorem common_support_of_twoValuePattern (S U : Finset (Fin 6))
    (hS : S.card = 3) (hU : U.card = 3)
    (hS0 : (0 : (Fin 6)) ∉ S) (hU0 : (0 : (Fin 6)) ∉ U)
    (x y : ℂ) (hx0 : x ≠ 0)
    (hx1 : x ≠ 1) (hy1 : y ≠ 1)
    (hp : TwoValuePattern (supportedRatio S U x y)) : S = U := by
…

Mentions: OAI.MUB6.TwoValuePattern, OAI.MUB6.supportedRatio