FactorialLift.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

A finite factorial-lift counterexample

The ten labels are the first cell's rows 0, 1, 2 and columns 3, 4, 5, and the second cell's rows 6, 7 and columns 8, 9. Conditioning on the first three rows gives a symmetric addition matrix with two distinct positive eigenvalues. This finite counterexample does not formalize a randomized approximation algorithm for contingency tables.

abbrev OAI.DistinctLifts.Label line 25
abbrev OAI.DistinctLifts.Remaining line 26
def OAI.DistinctLifts.count line 28
def OAI.DistinctLifts.factorialLift line 32
Source documentation
The factorial lift for capacities 3 and 2, with constant weight one. It is defined on all sets here and subsequently restricted to 5-subsets.
```
def factorialLift (S : Finset Label) : ℝ :=
…
```
Mentions: OAI.DistinctLifts.Label
def OAI.DistinctLifts.fixed line 36
def OAI.DistinctLifts.remaining line 37
def OAI.DistinctLifts.conditioned line 38
theorem OAI.DistinctLifts.conditioned_card line 40
def OAI.DistinctLifts.additionMatrix line 45
Source documentation
Actual row-conditioned addition matrix, with the required zero diagonal.
```
def additionMatrix : Matrix Remaining Remaining ℝ :=
…
```
Mentions: OAI.DistinctLifts.Remaining
def OAI.DistinctLifts.explicitMatrix line 49
Source documentation
First block: three first-cell columns. Second block: two rows and two columns of the second cell; same-kind and mixed-kind entries differ.
```
def explicitMatrix : Matrix Remaining Remaining ℝ := fun i j =>
…
```
Mentions: OAI.DistinctLifts.Remaining
theorem OAI.DistinctLifts.additionMatrix_eq line 55
theorem OAI.DistinctLifts.additionMatrix_symmetric line 63
def OAI.DistinctLifts.eigenvector line 69
Source documentation
Both signs use the same three nonzero first coordinates.
```
def eigenvector (s : ℝ) : Remaining → ℝ := fun i => if i.val < 3 then 2 else s
```
Mentions: OAI.DistinctLifts.Remaining
theorem OAI.DistinctLifts.eigenvector_nonzero line 71
theorem OAI.DistinctLifts.eigenvector_equation line 77
Source documentation
The calculation retains all four second-block entries separately.
```
theorem eigenvector_equation (s : ℝ) (hs : s ^ 2 = 3) :
    additionMatrix.mulVecLin (eigenvector s) = (2 + s) • eigenvector s := by
…
```
Mentions: OAI.DistinctLifts.eigenvector
theorem OAI.DistinctLifts.eigenvalue_of_square line 85
def OAI.DistinctLifts.PositiveEigenvaluesUnique line 93
Source documentation
A necessary condition for having at most one positive eigenvalue, even when multiplicities are counted. Two distinct positive native eigenvalues already contradict this condition, so no inertia convention is required.
```
def PositiveEigenvaluesUnique (A : Matrix Remaining Remaining ℝ) : Prop :=
…
```
Mentions: OAI.DistinctLifts.Remaining
theorem OAI.DistinctLifts.two_distinct_positive_eigenvalues line 97
theorem OAI.DistinctLifts.factorial_lift_fails_addition_signature line 110
Source documentation
The actual conditioned factorial lift fails the necessary spectral condition in the addition property. No claim about the other lift is made.
```
theorem factorial_lift_fails_addition_signature :
    ¬ PositiveEigenvaluesUnique additionMatrix := by
…
```
Mentions: OAI.DistinctLifts.PositiveEigenvaluesUnique, OAI.DistinctLifts.additionMatrix
def OAI.DistinctLifts.blockVector line 117
Source documentation
Vectors constant on the groups of three and four remaining labels.
```
def blockVector (a b : ℝ) : Remaining → ℝ := fun i => if i.val < 3 then a else b
```
Mentions: OAI.DistinctLifts.Remaining
theorem OAI.DistinctLifts.restricted_quadratic line 119

theorem OAI.DistinctLifts.factorial_lift_counterexample line 128

Source documentation

Full finite counterexample: the conditioned sets have the required size, the actual factorial-lift matrix is symmetric, and it has two distinct positive eigenvalues in the native linear-map API.

theorem factorial_lift_counterexample :
    (∀ i j : Remaining, i ≠ j → (conditioned i j).card = 5) ∧
    Matrix.IsSymm additionMatrix ∧
    0 < 2 + Real.sqrt 3 ∧ 0 < 2 - Real.sqrt 3 ∧
    2 + Real.sqrt 3 ≠ 2 - Real.sqrt 3 ∧
    Module.End.HasEigenvalue additionMatrix.mulVecLin (2 + Real.sqrt 3) ∧
    Module.End.HasEigenvalue additionMatrix.mulVecLin (2 - Real.sqrt 3) := by
…

Mentions: OAI.DistinctLifts.Remaining, OAI.DistinctLifts.conditioned, OAI.DistinctLifts.additionMatrix