AntecedentCountLemmas.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Exact antecedents of quotient compression

This is the reverse-map count used in Proposition A.5. The compressed map is fixed, together with the two removed subspaces; neither a prescribed rank nor an assumed cardinality is part of the antecedent predicate.

def OAI.UniqueGamesTheorem.Appendix.AntecedentCount.IsAntecedent line 41
Source documentation
Actual quotient-compression antecedents with the complement conditions in the passage from (A.15) to (A.16).
```
def IsAntecedent (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) (X : W →ₗ[F2] V) : Prop :=
…
```
abbrev OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Antecedent line 45
abbrev OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Admissible line 51
Source documentation
Maps satisfying the geometric complement conditions, before their compression is fixed.
```
abbrev Admissible (P : Submodule F2 W) (Q : Submodule F2 V) :=
…
```
def OAI.UniqueGamesTheorem.Appendix.AntecedentCount.compressionEquiv line 55
Source documentation
Reindex the actual maps by their actual compressed frequency.
```
def compressionEquiv (P : Submodule F2 W) (Q : Submodule F2 V) :
    Admissible P Q ≃ Σ Y : P →ₗ[F2] (V ⧸ Q), Antecedent P Q Y where
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Admissible, OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Antecedent
theorem OAI.UniqueGamesTheorem.Appendix.AntecedentCount.isAntecedent_iff_subspace line 67
Source documentation
Choosing a codomain complement only changes the coordinates of the fixed compressed output.
```
theorem isAntecedent_iff_subspace (P : Submodule F2 W)
    (Q D : Submodule F2 V) (hQ : IsCompl Q D)
    (Y : P →ₗ[F2] (V ⧸ Q)) (X : W →ₗ[F2] V) :
    IsAntecedent P Q Y X ↔
      DerivativeInduction.IsSubspaceAntecedent P Q D hQ
        ((Q.quotientEquivOfIsCompl D hQ).toLinearMap.comp Y) X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.IsAntecedent, OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.IsSubspaceAntecedent
def OAI.UniqueGamesTheorem.Appendix.AntecedentCount.subspaceEquiv line 87
Source documentation
The quotient antecedents and the graph-coordinate antecedents are the same maps, with equivalent predicates.
```
def subspaceEquiv (P : Submodule F2 W) (Q D : Submodule F2 V)
    (hQ : IsCompl Q D) (Y : P →ₗ[F2] (V ⧸ Q)) :
    Antecedent P Q Y ≃ DerivativeInduction.SubspaceAntecedent P Q D hQ
      ((Q.quotientEquivOfIsCompl D hQ).toLinearMap.comp Y) where
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Antecedent, OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.SubspaceAntecedent
theorem OAI.UniqueGamesTheorem.Appendix.AntecedentCount.rank_eq line 100
Source documentation
Every admissible antecedent has the rank of its fixed compression.
```
theorem rank_eq (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) (X : Antecedent P Q Y) :
    Module.finrank F2 X.val.range = Module.finrank F2 Y.range := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Antecedent
theorem OAI.UniqueGamesTheorem.Appendix.AntecedentCount.card_antecedent line 109
Source documentation
Exact number of antecedents of a fixed quotient compression. The graph and omitted-domain parameters have rank Y * (dim Q + codim P) bits.
```
theorem card_antecedent (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) :
    Nat.card (Antecedent P Q Y) =
      2 ^ (Module.finrank F2 Y.range *
        (Module.finrank F2 Q + Module.finrank F2 (W ⧸ P))) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Antecedent

theorem OAI.UniqueGamesTheorem.Appendix.AntecedentCount.card_antecedent_le line 123

Source documentation

The actual reverse-map multiplicity fits the two graph-parameter budgets used in (A.16). No additional isomorphism factor is needed.

theorem card_antecedent_le (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) (d k : ℕ)
    (hY : Module.finrank F2 Y.range ≤ k)
    (hQ : Module.finrank F2 Q ≤ d)
    (hP : Module.finrank F2 (W ⧸ P) ≤ d) :
    Nat.card (Antecedent P Q Y) ≤ 2 ^ (2 * d * k) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Antecedent

theorem OAI.UniqueGamesTheorem.Appendix.AntecedentCount.sum_compression line 139

Source documentation

Exact finite-sum reindexing by compressed maps, with the true fiber multiplicity. This holds for signed weights as well as nonnegative energies.

theorem sum_compression [Fintype (W →ₗ[F2] V)]
    (P : Submodule F2 W) (Q : Submodule F2 V)
    [Fintype (P →ₗ[F2] (V ⧸ Q))]
    {R : Type*} [Semiring R] (weight : (P →ₗ[F2] (V ⧸ Q)) → R) :
    (∑ X : Admissible P Q, weight (compress X.val Q P)) =
      ∑ Y : P →ₗ[F2] (V ⧸ Q),
        (2 : R) ^ (Module.finrank F2 Y.range *
          (Module.finrank F2 Q + Module.finrank F2 (W ⧸ P))) * weight Y := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.Admissible

def OAI.UniqueGamesTheorem.Appendix.FullCompression.compression line 189
Source documentation
Restrict a dual map to ker X and then quotient by range X.
```
def compression (X Y : E →ₗ[F2] F) : X.ker →ₗ[F2] (F ⧸ X.range) :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.FullCompression.compression_apply line 193
def OAI.UniqueGamesTheorem.Appendix.FullCompression.Fiber line 198
Source documentation
The genuine rank-additive compression fiber. In characteristic two, Y - X and Y + X are equal.
```
def Fiber (X : E →ₗ[F2] F) (Z : X.ker →ₗ[F2] (F ⧸ X.range)) :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.FullCompression.fiber_condition_iff line 203
def OAI.UniqueGamesTheorem.Appendix.FullCompression.fiberEquiv line 240
Source documentation
Coordinate transport is a bijection on the complete rank-additive fibers.
```
def fiberEquiv (X : E →ₗ[F2] F) (Z : X.ker →ₗ[F2] (F ⧸ X.range))
    (P : Submodule F2 E) (hP : IsCompl X.ker P)
    (C : Submodule F2 F) (hC : IsCompl X.range C) :
    Fiber X Z ≃ CompressionCount.Fiber (U := X.range)
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.FullCompression.Fiber, OAI.UniqueGamesTheorem.Appendix.CompressionCount.Fiber
theorem OAI.UniqueGamesTheorem.Appendix.FullCompression.card_fiber line 251
Source documentation
Lemma A.2: every compressed rank-r map has exactly 2^(2*k*r) rank-additive lifts above an arbitrary rank-k map X.
```
theorem card_fiber (X : E →ₗ[F2] F) (Z : X.ker →ₗ[F2] (F ⧸ X.range)) :
    Nat.card (Fiber X Z) = 2 ^ (2 * finrank F2 X.range * finrank F2 Z.range) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.FullCompression.Fiber
theorem OAI.UniqueGamesTheorem.Appendix.FullCompression.fiber_rank line 260
Source documentation
Every member of a compression fiber has rank rank X + rank Z.
```
theorem fiber_rank (X : E →ₗ[F2] F)
    (Z : X.ker →ₗ[F2] (F ⧸ X.range)) (Y : Fiber X Z) :
    finrank F2 Y.val.range = finrank F2 X.range + finrank F2 Z.range := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.FullCompression.Fiber
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeEnergy.supported_fiber_energy line 299

theorem OAI.UniqueGamesTheorem.Appendix.DerivativeEnergy.coefficient_energy line 347

Source documentation

The precise merged-coefficient form of (A.10). Coefficients are arbitrary real numbers with the stated degree support, not assumed nonnegative.

theorem coefficient_energy (X : E →ₗ[F2] F)
    [Fintype (X.ker →ₗ[F2] (F ⧸ X.range))]
    (a : (E →ₗ[F2] F) → ℝ) (d : Nat)
    (hdegree : ∀ Y, d < finrank F2 Y.range → a Y = 0) :
    (∑ Z, (∑ Y, if RankBelow X Y ∧ FullCompression.compression X Y = Z
      then a Y else 0)^2) ≤
      (2 : ℝ)^(2 * finrank F2 X.range * (d - finrank F2 X.range)) *
        ∑ Y, if RankBelow X Y then a Y^2 else 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.FullCompression.compression

def OAI.UniqueGamesTheorem.Appendix.TotalPredecessorCount.predecessorEnd line 395
theorem OAI.UniqueGamesTheorem.Appendix.TotalPredecessorCount.predecessorEnd_recovery line 405
theorem OAI.UniqueGamesTheorem.Appendix.TotalPredecessorCount.predecessorEnd_injective line 415
theorem OAI.UniqueGamesTheorem.Appendix.TotalPredecessorCount.card_predecessors_le line 429
def OAI.UniqueGamesTheorem.Appendix.UpperMobius.upperQuotientEquiv line 465
def OAI.UniqueGamesTheorem.Appendix.UpperMobius.dualSubspaceEquiv line 469
theorem OAI.UniqueGamesTheorem.Appendix.UpperMobius.quotient_comap_codim line 475
theorem OAI.UniqueGamesTheorem.Appendix.UpperMobius.upperQuotientEquiv_codim line 486
def OAI.UniqueGamesTheorem.Appendix.UpperMobius.upperDualSubspaceEquiv line 495
theorem OAI.UniqueGamesTheorem.Appendix.UpperMobius.upperDualSubspaceEquiv_codim line 501
def OAI.UniqueGamesTheorem.Appendix.UpperMobius.upperWeightedTotal line 512
theorem OAI.UniqueGamesTheorem.Appendix.UpperMobius.upperWeightedTotal_eq_dual line 517
theorem OAI.UniqueGamesTheorem.Appendix.UpperMobius.quotient_finrank_zero_iff line 531
theorem OAI.UniqueGamesTheorem.Appendix.UpperMobius.binary_upper_interval_mobius line 544