BlockCounting.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact field-line count for the quadratic block's erasure probability.

abbrev OAI.UniqueGamesTheorem.Quadratic.FieldLine line 14
Source documentation
Actual one-dimensional field directions, with proportional nonzero vectors identified.
```
abbrev FieldLine (F : Type*) [Field F] := Projectivization F (Vec F)
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
def OAI.UniqueGamesTheorem.Quadratic.lineGenerator line 19
Source documentation
A chosen nonzero generator, only used with generator-independent data.
```
noncomputable def lineGenerator (A : FieldLine F) : Vec F := A.rep
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.lineGenerator_ne_zero line 21
theorem OAI.UniqueGamesTheorem.Quadratic.line_lineGenerator line 24
theorem OAI.UniqueGamesTheorem.Quadratic.fieldLine_finrank line 27
theorem OAI.UniqueGamesTheorem.Quadratic.card_FieldLine line 33
Source documentation
The denominator of the block erasure probability is exactly q²+q+1.
```
theorem card_FieldLine : Nat.card (FieldLine F) = Nat.card F ^ 2 + Nat.card F + 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.FieldLine
theorem OAI.UniqueGamesTheorem.Quadratic.card_fieldLine_submodules line 40
Source documentation
The same count on one-dimensional submodules, rather than representatives.
```
theorem card_fieldLine_submodules :
    Nat.card {A : Submodule F (Vec F) // Module.finrank F A = 1} =
      Nat.card F ^ 2 + Nat.card F + 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.card_FieldLine_pos line 46
theorem OAI.UniqueGamesTheorem.Quadratic.reciprocal_card_FieldLine line 51
Source documentation
Written over rationals, as needed for the finite rational noise law.
```
theorem reciprocal_card_FieldLine :
    (Nat.card (FieldLine F) : ℚ)⁻¹ =
      ((Nat.card F : ℚ) ^ 2 + Nat.card F + 1)⁻¹ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.FieldLine