Incidence.lean`

70 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Release075.expect_pi_product line 12

Source documentation

Independence of coordinates under the uniform average on a finite product.

theorem expect_pi_product {I D : Type*} [Fintype I] [DecidableEq I] [Fintype D]
    (f : I → D → ℝ) :
    (𝔼 ω : I → D, ∏ i, f i (ω i)) = ∏ i, 𝔼 d, f i d := by
…

theorem OAI.Release075.expect_coordinate line 21

Source documentation

A coordinate of a uniform product has the uniform marginal.

theorem expect_coordinate {I D : Type*} [Fintype I] [DecidableEq I] [Fintype D] [Nonempty D]
    (i : I) (f : D → ℝ) : (𝔼 ω : I → D, f (ω i)) = 𝔼 d, f d := by
…

theorem OAI.Release075.expect_two_coordinates line 31

Source documentation

Distinct coordinate functions have a factorized second moment.

theorem expect_two_coordinates {I D : Type*} [Fintype I] [DecidableEq I] [Fintype D] [Nonempty D]
    (i j : I) (hij : i ≠ j) (f g : D → ℝ) :
    (𝔼 ω : I → D, f (ω i) * g (ω j)) = (𝔼 d, f d) * (𝔼 d, g d) := by
…

theorem OAI.Release075.expect_low_indicator_le line 51

theorem OAI.Release075.exists_of_expect_lt line 67

Source documentation

Existence from a strict finite average bound, without measure-theoretic null sets.

theorem exists_of_expect_lt {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    (X : Ω → ℝ) (a : ℝ) (h : (𝔼 ω, X ω) < a) : ∃ ω, X ω < a := by
…

theorem OAI.Release075.expect_centered_sum_sq line 73

Source documentation

Variance of a sum of independent coordinates, proved by a finite double sum.

theorem expect_centered_sum_sq {I D : Type*} [Fintype I] [DecidableEq I]
    [Fintype D] [Nonempty D] (b : I → D → ℝ) (p : I → ℝ)
    (hp : ∀ i, (𝔼 d, b i d) = p i) :
    (𝔼 ω : I → D, ((∑ i, b i (ω i)) - ∑ i, p i)^2) =
      ∑ i, (𝔼 d, (b i d - p i)^2) := by
…

theorem OAI.Release075.expect_bernoulli_sum_sq_le line 101

theorem OAI.Release075.expect_selected_product line 125

Source documentation

Joint moments of any injectively selected coordinates.

theorem expect_selected_product {A I D : Type*} [Fintype A] [Fintype I]
    [DecidableEq I] [Fintype D] [Nonempty D]
    (e : A ↪ I) (f : A → D → ℝ) :
    (𝔼 ω : I → D, ∏ a, f a (ω (e a))) = ∏ a, 𝔼 d, f a d := by
…

def OAI.Release075.OnChosenLine line 147
Source documentation
A line through a mark, chosen by its projective direction.
```
def OnChosenLine (a z : V) (d : Projectivization K V) : Prop :=
…
```
def OAI.Release075.PuncturedIncidence line 151
Source documentation
Only the chosen line's own mark is punctured.
```
def PuncturedIncidence (a z : V) (d : Projectivization K V) : Prop :=
…
```
theorem OAI.Release075.puncturedIncidence_iff line 155
Source documentation
At a point different from the mark, exactly one direction gives incidence.
```
theorem puncturedIncidence_iff (a z : V) (hza : z ≠ a) (d : Projectivization K V) :
    PuncturedIncidence a z d ↔ d = Projectivization.mk K (z-a) (sub_ne_zero.mpr hza) := by
…
```
Mentions: OAI.Release075.PuncturedIncidence

theorem OAI.Release075.lineMap_injective line 173

Source documentation

Each geometric line contains exactly |K| points.

theorem lineMap_injective (a : V) (d : Projectivization K V) :
    Function.Injective (fun t : K => a + t • d.rep) := by
…

theorem OAI.Release075.expect_puncturedIncidence line 179

Source documentation

The exact Bernoulli parameter of a uniformly chosen direction.

theorem expect_puncturedIncidence [Fintype (Projectivization K V)]
    (a z : V) (hza : z ≠ a) :
    (𝔼 d : Projectivization K V, if PuncturedIncidence a z d then (1 : ℝ) else 0) =
      1 / Fintype.card (Projectivization K V) := by
…

Mentions: OAI.Release075.PuncturedIncidence

def OAI.Release075.candidateMark line 193
Source documentation
An attempted mark on the geometric line joining consecutive point vertices.
```
def candidateMark (σ : A → A) (p : A → V) (t : A → K) (a : A) : V :=
…
```
def OAI.Release075.CycleCandidate line 198
Source documentation
An over-count of short cycles: parameters, rather than marks, are enumerated. Marks at punctured endpoints are deliberately permitted for the upper bound.
```
def CycleCandidate (S : Finset V) (σ : A → A) :=
…
```
instance OAI.Release075.(instance at line 204) line 204
def OAI.Release075.CycleCandidate.marks line 210
def OAI.Release075.CycleCandidate.direction line 214
def OAI.Release075.CycleCandidate.Occurs line 217
theorem OAI.Release075.CycleCandidate.expect_occurs line 222
Source documentation
The displayed upper count still has independent prescribed directions because its candidate marks are distinct.
```
theorem expect_occurs [Fintype A] [Fintype (Projectivization K V)] [Nontrivial V]
    (c : CycleCandidate (K := K) S σ) :
…
```
Mentions: OAI.Release075.CycleCandidate

def OAI.Release075.badCycles line 247

Source documentation

All occurring encoded cycles for a given random outcome.

def badCycles [Fintype A] [Fintype K] [Fintype V]
    (S : Finset V) (σ : A → A) (ω : S → Projectivization K V) : Finset (CycleCandidate (K := K) S σ) :=
…

Mentions: OAI.Release075.CycleCandidate

theorem OAI.Release075.expect_badCycles_le line 252

Source documentation

Expected cycle bound before specializing the finite field cardinalities.

theorem expect_badCycles_le [Fintype A] [Fintype K] [Fintype V]
    [Fintype (Projectivization K V)] [Nontrivial V]
    (S : Finset V) (σ : A → A) :
    (𝔼 ω : S → Projectivization K V, ((badCycles S σ ω).card : ℝ)) ≤
      (Fintype.card V : ℝ)^Fintype.card A * (Fintype.card K : ℝ)^Fintype.card A *
        (1 / Fintype.card (Projectivization K V) : ℝ)^Fintype.card A := by
…

Mentions: OAI.Release075.badCycles

def OAI.Release075.pointDegree line 283
Source documentation
Incidence degree before alteration, with the marked point removed from its line.
```
def pointDegree (S : Finset V) (ω : S → Projectivization K V) (z : V) : ℕ :=
…
```
def OAI.Release075.pointMean line 287
Source documentation
Exact mean, including the missing self-mark when the point belongs to the grid.
```
def pointMean (S : Finset V) (z : V) : ℝ :=
…
```
theorem OAI.Release075.pointMean_formula line 291
theorem OAI.Release075.expect_pointDegree line 301
theorem OAI.Release075.variance_pointDegree_le line 316

theorem OAI.Release075.expect_lowDegree_le line 331

Source documentation

Expected size of the exceptional low-degree set in a completely finite form.

theorem expect_lowDegree_le [Fintype V] (S : Finset V) (T : ℕ) (μ : ℝ)
    (hμ : 0 < μ) (hT : 2 * (T : ℝ) ≤ μ)
    (hlower : ∀ z : V, μ ≤ pointMean (K := K) S z) :
…

Mentions: OAI.Release075.pointMean

def OAI.Release075.relationGraph line 364
Source documentation
The simple bipartite graph of a relation (the same definition used by the links).
```
def relationGraph {A B : Type*} (R : A → B → Prop) : SimpleGraph (A ⊕ B) where
…
```
def OAI.Release075.relationColoring line 372
theorem OAI.Release075.relationGraph_even_getVert line 376
theorem OAI.Release075.relationGraph_odd_getVert line 387

theorem OAI.Release075.relationGraph_cycle_encoding line 398

Source documentation

The concrete alternating normal form of any simple bipartite cycle.

theorem relationGraph_cycle_encoding {A B : Type*} (R : A → B → Prop)
    {a : A} (w : (relationGraph R).Walk (.inl a) (.inl a)) (hw : w.IsCycle) :
    ∃ (s : ℕ) (_ : 2 ≤ s) (p : Fin s → A) (l : Fin s → B),
      w.length = 2*s ∧ Function.Injective p ∧ Function.Injective l ∧
      ∀ i, R (p i) (l i) ∧ R (p (finRotate s i)) (l i) := by
…

Mentions: OAI.Release075.relationGraph

theorem OAI.Release075.relationGraph_any_cycle_encoding line 447

Source documentation

The same encoding without a restriction on the chosen starting vertex.

theorem relationGraph_any_cycle_encoding {A B : Type*} (R : A → B → Prop)
    {a : A ⊕ B} (w : (relationGraph R).Walk a a) (hw : w.IsCycle) :
    ∃ (s : ℕ) (_ : 2 ≤ s) (p : Fin s → A) (l : Fin s → B),
      w.length = 2*s ∧ Function.Injective p ∧ Function.Injective l ∧
      ∀ i, R (p i) (l i) ∧ R (p (finRotate s i)) (l i) := by
…

Mentions: OAI.Release075.relationGraph

theorem OAI.Release075.line_two_points line 469

Source documentation

Two distinct points determine their direction and every mark on their line.

theorem line_two_points (a z z' : V) (d : Projectivization K V) (hzz : z' ≠ z)
    (hz : OnChosenLine a z d) (hz' : OnChosenLine a z' d) :
    ∃ t : K, a = z + t • (z'-z) ∧
      d = Projectivization.mk K (z'-z) (sub_ne_zero.mpr hzz) := by
…

Mentions: OAI.Release075.OnChosenLine

theorem OAI.Release075.finRotate_ne_self line 488
Source documentation
Rotation has no fixed point on a cycle with at least two entries.
```
theorem finRotate_ne_self {s : ℕ} (hs : 2 ≤ s) (i : Fin s) : finRotate s i ≠ i := by
…
```

theorem OAI.Release075.cycleCandidate_of_incidence line 504

Source documentation

Any actual simple incidence cycle yields one of the counted attempts.

theorem cycleCandidate_of_incidence {S : Finset V} (ω : S → Projectivization K V)
    {s : ℕ} (hs : 2 ≤ s) (p : Fin s → V) (l : Fin s → S)
    (hp : Function.Injective p) (hl : Function.Injective l)
    (h : ∀ i, PuncturedIncidence (l i).val (p i) (ω (l i)) ∧
      PuncturedIncidence (l i).val (p (finRotate s i)) (ω (l i))) :
    ∃ c : CycleCandidate (K := K) S (finRotate s), c.Occurs ω ∧ ∀ i, c.marks i = l i := by
…

Mentions: OAI.Release075.PuncturedIncidence, OAI.Release075.CycleCandidate

def OAI.Release075.deletedMarks line 530
Source documentation
All marks lying on an occurring short-cycle attempt are discarded.
```
def deletedMarks (S : Finset V) (ω : S → Projectivization K V) : Finset S :=
…
```
theorem OAI.Release075.deletedMarks_card_le line 534
def OAI.Release075.Retained line 552
theorem OAI.Release075.retained_girth line 556
Source documentation
Deletion creates no cycle; exact girth >12 is obtained, including repeated geometric lines with distinct labels.
```
theorem retained_girth (S : Finset V) (ω : S → Projectivization K V)
    (a : V ⊕ Retained S ω)
    (w : (relationGraph (fun z (i : Retained S ω) =>
      PuncturedIncidence i.val.val z (ω i.val))).Walk a a) (hw : w.IsCycle) : 12 < w.length := by
…
```
Mentions: OAI.Release075.Retained, OAI.Release075.relationGraph, OAI.Release075.PuncturedIncidence
instance OAI.Release075.(instance at line 582) line 582
def OAI.Release075.chosenLinePoints line 586
theorem OAI.Release075.mem_chosenLinePoints line 590
theorem OAI.Release075.chosenLinePoints_card line 595
def OAI.Release075.deletedPoints line 599
theorem OAI.Release075.deletedPoints_card_le line 602
def OAI.Release075.exceptionalPoints line 608
theorem OAI.Release075.exceptionalPoints_card_le line 611
def OAI.Release075.retainedIncidence line 617
theorem OAI.Release075.incidence_not_deleted line 620
theorem OAI.Release075.retainedIncidence_card line 628
Source documentation
Outside the discarded geometric lines, no incidence is changed by alteration.
```
theorem retainedIncidence_card (S : Finset V) (ω : S → Projectivization K V) (z : V)
    (hz : z ∉ deletedPoints S ω) : (retainedIncidence S ω z).card = pointDegree S ω z := by
…
```
Mentions: OAI.Release075.deletedPoints, OAI.Release075.retainedIncidence, OAI.Release075.pointDegree
theorem OAI.Release075.retainedIncidence_card_ge line 640
Source documentation
The exact degree threshold needed for the two-block partition.
```
theorem retainedIncidence_card_ge (S : Finset V) (ω : S → Projectivization K V) (T : ℕ)
    (z : V) (hz : z ∉ exceptionalPoints S ω T) : T ≤ (retainedIncidence S ω z).card := by
…
```
Mentions: OAI.Release075.exceptionalPoints, OAI.Release075.retainedIncidence
theorem OAI.Release075.retained_card line 647

theorem OAI.Release075.expect_deletedMarks_le line 659

Source documentation

A uniform expectation bound for all removed labels.

theorem expect_deletedMarks_le (S : Finset V) (q : ℝ)
    (hcycle : ∀ s ∈ Finset.Icc 2 6,
      (Fintype.card V : ℝ)^s * (Fintype.card K : ℝ)^s *
        (1 / Fintype.card (Projectivization K V) : ℝ)^s ≤ q^12) :
    (𝔼 ω : S → Projectivization K V, ((deletedMarks S ω).card : ℝ)) ≤ 30*q^12 := by
…

Mentions: OAI.Release075.deletedMarks

theorem OAI.Release075.exists_alteration_budget line 686
Source documentation
One finite averaging step obtains simultaneously the strict rank budget, the degree bound, and the cycle-free alteration; no asymptotic or external probabilistic result is being assumed.
```
theorem exists_alteration_budget (S : Finset V) (r T : ℕ) (μ B : ℝ)
    (hμ : 0 < μ) (hT : 2 * (T : ℝ) ≤ μ)
    (hlower : ∀ z : V, μ ≤ pointMean (K := K) S z)
…
```
Mentions: OAI.Release075.pointMean

theorem OAI.Release075.geom_sum_twenty_bounds line 728

Source documentation

The direction-count bounds used in dimension twenty.

theorem geom_sum_twenty_bounds {q : ℝ} (hq : 2 ≤ q) :
    q^19 ≤ ∑ i ∈ Finset.range 20, q^i ∧
      ∑ i ∈ Finset.range 20, q^i ≤ 2*q^19 := by
…

theorem OAI.Release075.cycle_numeric_bound line 742

Source documentation

A concrete bound for every short-cycle contribution.

theorem cycle_numeric_bound {q J : ℝ} (hq : 1 ≤ q) (hJ : q^19 ≤ J)
    {s : ℕ} (hs : s ≤ 6) : (q^20)^s * q^s * (1/J)^s ≤ q^12 := by
…

theorem OAI.Release075.incidence_numeric_budget line 756

theorem OAI.Release075.floor_grid_lower line 798

Source documentation

The grid is large enough uniformly in the prime.

theorem floor_grid_lower {q : ℕ} (hq : 200 ≤ q) :
    (q : ℝ)^20 ≤ (200 : ℝ)^20 * ((q/100 : ℕ) : ℝ)^20 := by
…

def OAI.Release075.gridMarks line 808
theorem OAI.Release075.gridMarks_card line 812
theorem OAI.Release075.directions_twenty_card line 815
theorem OAI.Release075.mean_grid_lower line 824

theorem OAI.Release075.large_prime_grid_outcome line 867

Source documentation

For a sufficiently large fixed prime, the alteration really attains the strict finite rank budget. Every subsequent quotient uses this same prime.

theorem large_prime_grid_outcome (r : ℕ) (hr : r = 200*200^20)
    (hq200 : 200 ≤ q) (hq : 1000*200^20*r^2 ≤ q)
    (S : Finset (ZMod q)) (hS : S.card = q/100) :
    ∃ ω : gridMarks q S → Projectivization (ZMod q) (Fin 20 → ZMod q),
      4 * (2 * Fintype.card (Fin 20 → ZMod q) +
        r * (exceptionalPoints (gridMarks q S) ω (4*r^2)).card) <
      Fintype.card (Retained (gridMarks q S) ω) * r := by
…

Mentions: OAI.Release075.gridMarks, OAI.Release075.exceptionalPoints, OAI.Release075.Retained

structure OAI.Release075.MarkedLineData line 899
Source documentation
Exact finite data fixed once for all before any finite quotient is chosen. No geometric or group-theoretic conclusion is part of these data.
```
structure MarkedLineData (q r : ℕ) [Fact q.Prime] where
…
```
theorem OAI.Release075.exists_markedLineData line 917
theorem OAI.Release075.MarkedLineData.card_labels_le line 954
Source documentation
The marking grid gives an a priori upper bound on the number of labels.
```
theorem card_labels_le : Fintype.card d.Label ≤ q^20 := by
…
```
theorem OAI.Release075.MarkedLineData.exists_regular line 958
theorem OAI.Release075.MarkedLineData.degree_cutoff line 970