ExteriorBounds.lean`

66 declarations, 0 contain sorry, 0 declared as axioms

Exterior monomials, color counts and finite stable-graph bounds

The color-incidence set indexes slots in triples of colors. Its lexicographic enumeration defines the color word and is used to count occurrences and word-preserving permutations. The exterior-algebra constructions prove nonvanishing of a factorial-scaled monomial, not a detector evaluation.

The strata class Y, its realizations, Pixton relation span, detector pairing and geometric vanishing are not defined here. These combinatorial results therefore do not assert the geometric main theorem or cohomological corollary.

def OAI.PixtonChow.genus line 26
def OAI.PixtonChow.entryCount line 30
Source documentation
Computed by the falling-factorial formula to avoid expanding Pascal's recursion at 10^60; entryCount_eq_choose proves the specified value.
```
def entryCount : ℕ := genus.descFactorial 3 / 6
```
theorem OAI.PixtonChow.entryCount_eq_choose line 32
def OAI.PixtonChow.markingCount line 36
theorem OAI.PixtonChow.parameter_bounds line 39
Source documentation
The elementary numerical bounds needed for the parameters.
```
theorem parameter_bounds (g d : ℕ) (hg : 2 ≤ g) :
    2 < 2 * g + 3 * d ∧ 2 * d < 3 * g - 3 + 3 * d := by
…
```
theorem OAI.PixtonChow.parameters_stable line 44
Source documentation
Stability of the specific pair in the source, in the form 2g + n > 2.
```
theorem parameters_stable : 2 < 2 * genus + markingCount :=
…
```
Mentions: OAI.PixtonChow.genus, OAI.PixtonChow.markingCount
theorem OAI.PixtonChow.proposed_codimension_lt_dimension line 49
Source documentation
The proposed codimension is below the moduli dimension. This says nothing about the existence or the degree of a strata-algebra element.
```
theorem proposed_codimension_lt_dimension :
    2 * entryCount < 3 * genus - 3 + markingCount :=
…
```
Mentions: OAI.PixtonChow.entryCount, OAI.PixtonChow.genus, OAI.PixtonChow.markingCount
abbrev OAI.PixtonChow.Triple line 56
Source documentation
A set of three distinct colors; sorting it gives its unique increasing triple.
```
abbrev Triple (g : ℕ) := Set.powersetCard (Fin g) 3
```
abbrev OAI.PixtonChow.ColorSlot line 59
Source documentation
Slots indexed by a triple together with one of its colors.
```
abbrev ColorSlot (g : ℕ) := (s : Triple g) × {c : Fin g // c ∈ s.val}
```
Mentions: OAI.PixtonChow.Triple
def OAI.PixtonChow.incidenceColor line 62
Source documentation
The color of a slot.
```
def incidenceColor {g : ℕ} (p : ColorSlot g) : Fin g := p.2.val
```
Mentions: OAI.PixtonChow.ColorSlot
theorem OAI.PixtonChow.triple_card line 64
theorem OAI.PixtonChow.block_card line 69
Source documentation
Each block contains exactly three slots.
```
theorem block_card {g : ℕ} (s : Triple g) :
    Fintype.card {c : Fin g // c ∈ s.val} = 3 := by
…
```
Mentions: OAI.PixtonChow.Triple
theorem OAI.PixtonChow.colorSlot_card line 73
def OAI.PixtonChow.colorFiberEquiv line 80
Source documentation
Erasing the choice of a distinguished color in a fiber of incidenceColor leaves precisely a triple containing that color.
```
def colorFiberEquiv {g : ℕ} (c : Fin g) :
    {p : ColorSlot g // incidenceColor p = c} ≃ {s : Triple g // c ∈ s.val} where
…
```
Mentions: OAI.PixtonChow.ColorSlot, OAI.PixtonChow.incidenceColor, OAI.PixtonChow.Triple

def OAI.PixtonChow.containingTripleEquiv line 94

Source documentation

Repackaging as the finite set of three-element supersets of {c}.

def containingTripleEquiv {g : ℕ} (c : Fin g) :
    {s : Triple g // c ∈ s.val} ≃
      {s // s ∈ ((Finset.univ : Finset (Fin g)).powersetCard 3).filter
        ({c} ⊆ ·)} where
…

Mentions: OAI.PixtonChow.Triple

theorem OAI.PixtonChow.containingTriple_card line 105
Source documentation
Every color belongs to choose (g-1) 2 of the triples.
```
theorem containingTriple_card {g : ℕ} (c : Fin g) :
    Fintype.card {s : Triple g // c ∈ s.val} = (g - 1).choose 2 := by
…
```
Mentions: OAI.PixtonChow.Triple
theorem OAI.PixtonChow.colorFiber_card line 111
abbrev OAI.PixtonChow.ColorStabilizer line 116
Source documentation
A permutation of slots preserving their colors.
```
abbrev ColorStabilizer (g : ℕ) :=
…
```
theorem OAI.PixtonChow.colorStabilizer_card line 121
Source documentation
The factorial multiplicity appearing in eq:detector-candidate-value. This counts permutations only: no equality involving the detector is asserted.
```
theorem colorStabilizer_card (g : ℕ) :
    Fintype.card (ColorStabilizer g) = ((g - 1).choose 2).factorial ^ g := by
…
```
Mentions: OAI.PixtonChow.ColorStabilizer
theorem OAI.PixtonChow.reindexed_stabilizer_card line 129
Source documentation
Counts are unchanged by any enumeration of the slots, including the lexicographic enumeration used in Definition def:candidate.
```
theorem reindexed_stabilizer_card (g : ℕ) {A : Type*} [Fintype A] [DecidableEq A]
    (e : A ≃ ColorSlot g) :
    Fintype.card {p : Equiv.Perm A // (incidenceColor ∘ e) ∘ p = incidenceColor ∘ e} =
      ((g - 1).choose 2).factorial ^ g := by
…
```
Mentions: OAI.PixtonChow.ColorSlot, OAI.PixtonChow.incidenceColor
def OAI.PixtonChow.tripleLexOrder line 146
Source documentation
Lexicographic order on the sorted lists representing the triples.
```
@[instance_reducible] def tripleLexOrder (g : ℕ) : LinearOrder (Triple g) :=
…
```
Mentions: OAI.PixtonChow.Triple
def OAI.PixtonChow.tripleEnumeration line 157
Source documentation
Increasing enumeration of all three-color blocks in lexicographic order.
```
def tripleEnumeration (g : ℕ) : Fin (g.choose 3) ≃ Triple g :=
…
```
Mentions: OAI.PixtonChow.Triple
def OAI.PixtonChow.blockSlotEquiv line 161
Source documentation
Each block is enumerated in increasing color order.
```
def blockSlotEquiv (g : ℕ) : Fin (g.choose 3) × Fin 3 ≃ ColorSlot g :=
…
```
Mentions: OAI.PixtonChow.ColorSlot
def OAI.PixtonChow.orderedSlotEquiv line 170
Source documentation
The first three positions are the first lexicographic block, etc.
```
def orderedSlotEquiv (g : ℕ) : Fin (3 * g.choose 3) ≃ ColorSlot g :=
…
```
Mentions: OAI.PixtonChow.ColorSlot
def OAI.PixtonChow.colorWord line 176
Source documentation
The concatenation of the increasing triples, with colors numbered 0,...,g-1 instead of 1,...,g.
```
def colorWord (g : ℕ) : Fin (3 * g.choose 3) → Fin g :=
…
```
theorem OAI.PixtonChow.colorWord_fiber_card line 179
theorem OAI.PixtonChow.colorWord_stabilizer_card line 187
abbrev OAI.PixtonChow.ExteriorCoefficients line 197
Source documentation
The exterior algebra on a freely specified set of generators.
```
abbrev ExteriorCoefficients (I : Type*) := ExteriorAlgebra ℚ (I →₀ ℚ)
```
def OAI.PixtonChow.theta line 200
Source documentation
The generator indexed by i.
```
def theta {I : Type*} (i : I) : ExteriorCoefficients I :=
…
```
Mentions: OAI.PixtonChow.ExteriorCoefficients
def OAI.PixtonChow.topExteriorProduct line 204
Source documentation
The product of all generators, in the given increasing order.
```
def topExteriorProduct (I : Type*) [Fintype I] [LinearOrder I] :
    ExteriorCoefficients I :=
…
```
Mentions: OAI.PixtonChow.ExteriorCoefficients
theorem OAI.PixtonChow.topExteriorProduct_eq_ordered_product line 210
theorem OAI.PixtonChow.topExteriorProduct_eq_basis line 218
Source documentation
Identifying the ordered monomial with an actual exterior-algebra basis vector, not positing its nonvanishing.
```
theorem topExteriorProduct_eq_basis (I : Type*) [Fintype I] [LinearOrder I] :
    topExteriorProduct I =
      (Finsupp.basisSingleOne : Module.Basis I ℚ (I →₀ ℚ)).ExteriorAlgebra Finset.univ := by
…
```
Mentions: OAI.PixtonChow.topExteriorProduct
theorem OAI.PixtonChow.topExteriorProduct_ne_zero line 224
theorem OAI.PixtonChow.factorial_multiple_topExteriorProduct_ne_zero line 231
Source documentation
The proposed detector's final scalar-multiple monomial is nonzero over ℚ. The crucial claim that it equals a pairing with t_n(Y) is not formalized.
```
theorem factorial_multiple_topExteriorProduct_ne_zero (g : ℕ) (I : Type*)
    [Fintype I] [LinearOrder I] :
    (((((g - 1).choose 2).factorial : ℕ) : ℚ) ^ g) • topExteriorProduct I ≠ 0 := by
…
```
Mentions: OAI.PixtonChow.topExteriorProduct
def OAI.PixtonChow.candidateTheta line 240
Source documentation
The monomial Θ indexed by all triples in lexicographic order, in the exterior algebra from Section 3.
```
def candidateTheta (g : ℕ) : ExteriorCoefficients (Triple g) :=
…
```
Mentions: OAI.PixtonChow.ExteriorCoefficients, OAI.PixtonChow.Triple
theorem OAI.PixtonChow.candidateTheta_ne_zero line 244
theorem OAI.PixtonChow.candidateTheta_multiple_ne_zero line 250
Source documentation
The unsigned right side of eq:detector-candidate-value is nonzero. No equality with a value of the candidate class is claimed here.
```
theorem candidateTheta_multiple_ne_zero (g : ℕ) :
    (((((g - 1).choose 2).factorial : ℕ) : ℚ) ^ g) • candidateTheta g ≠ 0 := by
…
```
Mentions: OAI.PixtonChow.candidateTheta
abbrev OAI.PixtonChow.GraphFlag line 263
Source documentation
The two flags at each edge, together with the labeled legs.
```
abbrev GraphFlag (E : Type*) (n : ℕ) := (E × Fin 2) ⊕ Fin n
```
def OAI.PixtonChow.EdgeAdjacent line 266
Source documentation
Undirected adjacency in a graph presentation.
```
def EdgeAdjacent {V E : Type*} {n : ℕ} (atVertex : GraphFlag E n → V)
    (u v : V) : Prop :=
…
```
Mentions: OAI.PixtonChow.GraphFlag
structure OAI.PixtonChow.StableGraph line 274
Source documentation
A finite connected stable graph of type (g,n), given by vertices, edges, flag incidences, and nonnegative vertex genera. The integer genus equation avoids truncated subtraction in |E| - |V| + 1.
```
structure StableGraph (g n : ℕ) (V E : Type*) [Fintype V] [Fintype E]
    [DecidableEq V] where
…
```
def OAI.PixtonChow.StableGraph.valence line 288
Source documentation
Number of flags, including legs, incident to a vertex.
```
def valence (Γ : StableGraph g n V E) (v : V) : ℕ :=
…
```
Mentions: OAI.PixtonChow.StableGraph
theorem OAI.PixtonChow.StableGraph.sum_valence line 291
theorem OAI.PixtonChow.StableGraph.sum_stability line 298
Source documentation
Summing the stability weights cancels the individual vertex genera.
```
theorem sum_stability (Γ : StableGraph g n V E) :
    ∑ v, (2 * (Γ.vertexGenus v : ℤ) - 2 + Γ.valence v) = 2 * g - 2 + n := by
…
```
Mentions: OAI.PixtonChow.StableGraph
theorem OAI.PixtonChow.StableGraph.vertex_bound line 307
Source documentation
The usual bound on the number of vertices, including marked graphs.
```
theorem vertex_bound (Γ : StableGraph g n V E) :
    (Fintype.card V : ℤ) ≤ 2 * g - 2 + n := by
…
```
Mentions: OAI.PixtonChow.StableGraph
theorem OAI.PixtonChow.StableGraph.edge_bound line 319
def OAI.PixtonChow.StableGraph.noiseCount line 326
Source documentation
R_Γ from lem:elementary-entry-tests.
```
def noiseCount (_Γ : StableGraph g n V E) : ℕ :=
…
```
Mentions: OAI.PixtonChow.StableGraph
theorem OAI.PixtonChow.StableGraph.noiseCount_bound line 330
Source documentation
The unmarked global noise bound eq:global-noise-bound.
```
theorem noiseCount_bound (Γ : StableGraph g 0 V E) :
    (Γ.noiseCount : ℤ) ≤ 10 * g := by
…
```
Mentions: OAI.PixtonChow.StableGraph
theorem OAI.PixtonChow.StableGraph.other_vertices_bound line 340
Source documentation
For any distinguished vertex, the first small-deficit bound. It does not require that this vertex have maximum genus.
```
theorem other_vertices_bound (Γ : StableGraph g 0 V E) (v : V) :
    (Fintype.card V : ℤ) - 1 ≤ 2 * ((g : ℤ) - Γ.vertexGenus v) := by
…
```
Mentions: OAI.PixtonChow.StableGraph
theorem OAI.PixtonChow.StableGraph.small_deficit_edge_bound line 360
Source documentation
The edge part of eq:small-graph-size.
```
theorem small_deficit_edge_bound (Γ : StableGraph g 0 V E) (v : V) :
    (Fintype.card E : ℤ) ≤ 3 * ((g : ℤ) - Γ.vertexGenus v) := by
…
```
Mentions: OAI.PixtonChow.StableGraph
theorem OAI.PixtonChow.StableGraph.small_deficit_noise_bound line 367
Source documentation
The noise budget when the genus deficit at a distinguished vertex is small.
```
theorem small_deficit_noise_bound (Γ : StableGraph g 0 V E) (v : V) :
    (Γ.noiseCount : ℤ) ≤ 10 * ((g : ℤ) - Γ.vertexGenus v) + 2 := by
…
```
Mentions: OAI.PixtonChow.StableGraph
def OAI.PixtonChow.ColorBudget.K line 382
def OAI.PixtonChow.ColorBudget.blockSize line 384
def OAI.PixtonChow.ColorBudget.blockCount line 386
def OAI.PixtonChow.ColorBudget.C line 389
Source documentation
C_K, computed without recursion in the upper argument of choose.
```
def C : ℕ := (2 * K).descFactorial 3 / 6
```
Mentions: OAI.PixtonChow.ColorBudget.K
def OAI.PixtonChow.ColorBudget.D₀ line 392
Source documentation
D_0, computed by the same falling-factorial formula.
```
def D₀ : ℕ := blockSize.descFactorial 3 / 6
```
theorem OAI.PixtonChow.ColorBudget.C_eq_choose line 394
theorem OAI.PixtonChow.ColorBudget.D₀_eq_choose line 398
theorem OAI.PixtonChow.ColorBudget.block_scale line 403
Source documentation
10^40 is the integer value required for g^(2/3) at this genus.
```
theorem block_scale : (10 ^ 40 : ℕ) ^ 3 = genus ^ 2 := by
…
```
Mentions: OAI.PixtonChow.genus
theorem OAI.PixtonChow.ColorBudget.reservation_bound line 407
Source documentation
Fewer than one tenth of the colors are needed for the reserved blocks.
```
theorem reservation_bound : 10 * (blockCount * blockSize) < genus := by
…
```
Mentions: OAI.PixtonChow.ColorBudget.blockCount, OAI.PixtonChow.ColorBudget.blockSize, OAI.PixtonChow.genus
theorem OAI.PixtonChow.ColorBudget.remaining_bound line 411
Source documentation
The remaining number of colors is strictly greater than 0.9 g.
```
theorem remaining_bound : 9 * genus < 10 * (genus - blockCount * blockSize) := by
…
```
Mentions: OAI.PixtonChow.genus, OAI.PixtonChow.ColorBudget.blockCount, OAI.PixtonChow.ColorBudget.blockSize
theorem OAI.PixtonChow.ColorBudget.C_bound line 415
theorem OAI.PixtonChow.ColorBudget.block_entry_bound line 418
theorem OAI.PixtonChow.ColorBudget.ordinary_small_cost line 421
theorem OAI.PixtonChow.ColorBudget.small_loss_bounds line 426
Source documentation
The two numerical inequalities in eq:small-loss, with the second one multiplied by 100 to stay in natural numbers.
```
theorem small_loss_bounds :
    3 * genus * (C + 1) + genus * (10 * K + 2) + 2 * K * C < 10 ^ 17 * genus ∧
      100 * (10 ^ 17 * genus) < D₀ := by
…
```
Mentions: OAI.PixtonChow.genus, OAI.PixtonChow.ColorBudget.C, OAI.PixtonChow.ColorBudget.K, OAI.PixtonChow.ColorBudget.D₀
theorem OAI.PixtonChow.ColorBudget.expensive_count_bounds line 433
Source documentation
Bounds on the number of reserved blocks; no existence of an advancement is assumed or derived from these numerical comparisons.
```
theorem expensive_count_bounds :
    4 * (genus - K - 2) > 3 * genus - 3 ∧ 3 * K + 5 < blockCount := by
…
```
Mentions: OAI.PixtonChow.genus, OAI.PixtonChow.ColorBudget.K, OAI.PixtonChow.ColorBudget.blockCount
theorem OAI.PixtonChow.ColorBudget.ordinary_cost_bounds line 437