PatternCount.lean`

86 declarations, 0 contain sorry, 0 declared as axioms

Exact finite geometry and type system over the field with 128 elements.

theorem OAI.TorsionFreeZeroDivisors.PatternCount.contains_prescriptions line 16

Source documentation

A prescribed undirected edge can be read in either orientation.

theorem contains_prescriptions (r : Matching label bar) (ports : E → D × D) :
    r.Contains (Finset.univ.image (fun e => s((ports e).1,(ports e).2))) ↔
      ∀ e, r (ports e).1 = (ports e).2 := by
…

theorem OAI.TorsionFreeZeroDivisors.PatternCount.sum_realizations_eq line 32
Source documentation
The expectation numerator counts each vertex realization in each matching exactly once; prescriptions retain every edge, rather than path occurrences.
```
theorem sum_realizations_eq (origin : D → V) (N : ℕ) (C : F → Finset (Sym2 D)) :
    (∑ r ∈ Matching.conditioned (label := label) (bar := bar) origin N ∅,
…
```

theorem OAI.TorsionFreeZeroDivisors.PatternCount.expectation_bound line 49

Source documentation

Finite first-moment bound for a fixed labelled actual-image pattern. Distinct edges, not occurrences, supply the power of the matching denominator.

theorem expectation_bound [DecidableEq D] (origin : D → V) (N : ℕ)
    (hbar : ∀ t, bar t ≠ t) (d : ℕ) (h2 : 2 ≤ d)
    (hd : ∀ v, Nat.card {e : D // origin e = v} ≤ d)
    (C : F → Finset (Sym2 D)) (E R : ℕ) (hcard : ∀ f, (C f).card = E)
    (hR : 0 < R)
    (hsize : ∀ x, R + E + 4*d^(2*N+1) ≤ Nat.card {e : D // label e = label x})
    (hΩ : (Matching.conditioned (label := label) (bar := bar) origin N ∅).Nonempty) :
…

theorem OAI.TorsionFreeZeroDivisors.PatternCount.vertex_assignments_card line 84
Source documentation
Independent vertex carrier restrictions count by an exact product. This is an upper bound for injective vertex maps, without assuming independence of sampled edges.
```
theorem vertex_assignments_card [Fintype A]
    (allowed : A → Finset V) :
    Fintype.card {f : A → V // ∀ a, f a ∈ allowed a} =
      ∏ a : A, (allowed a).card := by
…
```
abbrev OAI.TorsionFreeZeroDivisors.PatternEmbeddings.Dart line 104
def OAI.TorsionFreeZeroDivisors.PatternEmbeddings.origin line 105
def OAI.TorsionFreeZeroDivisors.PatternEmbeddings.label line 106
def OAI.TorsionFreeZeroDivisors.PatternEmbeddings.edges line 108
abbrev OAI.TorsionFreeZeroDivisors.PatternEmbeddings.VertexMap line 111
def OAI.TorsionFreeZeroDivisors.PatternEmbeddings.dartMap line 120
Source documentation
Every candidate is injective on actual-image vertices; the letters uniquely specify the target ports before the random matching is chosen.
```
def dartMap (f : VertexMap allowed) (d : PD) : Dart outgoing :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PatternEmbeddings.VertexMap, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.Dart
theorem OAI.TorsionFreeZeroDivisors.PatternEmbeddings.dartMap_injective line 124
def OAI.TorsionFreeZeroDivisors.PatternEmbeddings.prescriptions line 135
Source documentation
Each undirected actual edge is prescribed once, regardless of its number of occurrences in the paths. This prevents the independence fallacy.
```
def prescriptions (f : VertexMap allowed) : Finset (Sym2 (Dart outgoing)) :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PatternEmbeddings.VertexMap, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.Dart
theorem OAI.TorsionFreeZeroDivisors.PatternEmbeddings.prescriptions_card line 139
theorem OAI.TorsionFreeZeroDivisors.PatternEmbeddings.contains_iff line 149
Source documentation
A matching contains the prescriptions precisely when the vertex map is an edge-respecting labelled graph embedding.
```
theorem contains_iff (bar : T → T) (f : VertexMap allowed)
    (r : Matching (label outgoing) bar) :
    r.Contains (prescriptions Γ plabel outgoing allowed hallowed f) ↔
      ∀ d, r.val (dartMap Γ plabel outgoing allowed hallowed f d) =
        dartMap Γ plabel outgoing allowed hallowed f (Γ.reverse d) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PatternEmbeddings.VertexMap, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.label, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.prescriptions, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.dartMap
theorem OAI.TorsionFreeZeroDivisors.PatternEmbeddings.vertexMap_card line 166

theorem OAI.TorsionFreeZeroDivisors.PatternEmbeddings.expectation_bound line 179

Source documentation

Fixed-label stage first moment with all graph-embedding hypotheses explicit. The only counting input on vertices is their literal carrier sets.

theorem expectation_bound (bar : T → T) (hbar : ∀ t, bar t ≠ t)
    (himm : Function.Injective (fun d => (Γ.origin d,plabel d)))
    (N d R : ℕ) (h2 : 2 ≤ d) (hR : 0 < R)
    (hd : ∀ v, Nat.card {e : Dart outgoing // origin outgoing e = v} ≤ d)
    (hsize : ∀ x : Dart outgoing,
      R + (edges Γ).card + 4*d^(2*N+1) ≤
        Nat.card {e : Dart outgoing // label outgoing e = label outgoing x})
    (hΩ : (Matching.conditioned (label := label outgoing) (bar := bar)
…

Mentions: OAI.TorsionFreeZeroDivisors.PatternEmbeddings.Dart, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.origin, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.edges, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.label

abbrev OAI.TorsionFreeZeroDivisors.Types.Field128 line 213
instance OAI.TorsionFreeZeroDivisors.Types.(instance at line 215) line 215
instance OAI.TorsionFreeZeroDivisors.Types.(instance at line 216) line 216
abbrev OAI.TorsionFreeZeroDivisors.Types.Point line 218
abbrev OAI.TorsionFreeZeroDivisors.Types.Line line 219
instance OAI.TorsionFreeZeroDivisors.Types.(instance at line 221) line 221
instance OAI.TorsionFreeZeroDivisors.Types.(instance at line 222) line 222
instance OAI.TorsionFreeZeroDivisors.Types.(instance at line 224) line 224
theorem OAI.TorsionFreeZeroDivisors.Types.field_card line 226
theorem OAI.TorsionFreeZeroDivisors.Types.point_card line 229
theorem OAI.TorsionFreeZeroDivisors.Types.order_eq line 236
def OAI.TorsionFreeZeroDivisors.Types.pointsOn line 246
Source documentation
Ordinary labels carried by a line type.
```
def pointsOn (l : Line) : Finset Point := Finset.univ.filter (· ∈ l)
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.Line, OAI.TorsionFreeZeroDivisors.Types.Point
def OAI.TorsionFreeZeroDivisors.Types.linesOn line 248
theorem OAI.TorsionFreeZeroDivisors.Types.mem_pointsOn line 250
theorem OAI.TorsionFreeZeroDivisors.Types.mem_linesOn line 253
theorem OAI.TorsionFreeZeroDivisors.Types.pointsOn_card line 256
theorem OAI.TorsionFreeZeroDivisors.Types.linesOn_card line 261
theorem OAI.TorsionFreeZeroDivisors.Types.pointsOn_inter_card line 266
theorem OAI.TorsionFreeZeroDivisors.Types.linesOn_inter_card line 275

theorem OAI.TorsionFreeZeroDivisors.Types.card_prod_fst line 285

Source documentation

Counting a predicate depending only on the first coordinate.

theorem card_prod_fst {U V : Type*} [Fintype U] [Fintype V]
    (p : U → Prop) [DecidablePred p] :
    Fintype.card {x : U × V // p x.1} = Fintype.card {u : U // p u} * Fintype.card V := by
…

theorem OAI.TorsionFreeZeroDivisors.Types.card_prod_snd line 295
abbrev OAI.TorsionFreeZeroDivisors.Types.SlotA line 307
abbrev OAI.TorsionFreeZeroDivisors.Types.SlotB line 308
abbrev OAI.TorsionFreeZeroDivisors.Types.VertexA line 309
abbrev OAI.TorsionFreeZeroDivisors.Types.VertexB line 310
abbrev OAI.TorsionFreeZeroDivisors.Types.Letter line 311
def OAI.TorsionFreeZeroDivisors.Types.extrasA line 313
def OAI.TorsionFreeZeroDivisors.Types.extrasB line 317
def OAI.TorsionFreeZeroDivisors.Types.outgoingA line 321
def OAI.TorsionFreeZeroDivisors.Types.outgoingB line 324
theorem OAI.TorsionFreeZeroDivisors.Types.card_slotA line 327
theorem OAI.TorsionFreeZeroDivisors.Types.card_slotB line 330
theorem OAI.TorsionFreeZeroDivisors.Types.card_vertexA line 333
theorem OAI.TorsionFreeZeroDivisors.Types.card_vertexB line 337
theorem OAI.TorsionFreeZeroDivisors.Types.disjSum_inter line 341
theorem OAI.TorsionFreeZeroDivisors.Types.ordinary_inter_odd line 347
theorem OAI.TorsionFreeZeroDivisors.Types.extras_inter_even line 355
theorem OAI.TorsionFreeZeroDivisors.Types.odd_cross_intersections line 362
Source documentation
The parity condition holds on every admissible size, independently of all edge matchings, exactly as in equation odd-intersections.
```
theorem odd_cross_intersections {N : ℕ} (x : VertexA N) (y : VertexB N) :
    Odd ((outgoingA x ∩ outgoingB y).card) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.Types.outgoingA, OAI.TorsionFreeZeroDivisors.Types.outgoingB
theorem OAI.TorsionFreeZeroDivisors.Types.degreeA_bounds line 367
theorem OAI.TorsionFreeZeroDivisors.Types.degreeB_bounds line 372
theorem OAI.TorsionFreeZeroDivisors.Types.slotA_extra_frequency line 377
theorem OAI.TorsionFreeZeroDivisors.Types.slotB_extra_frequency line 393
theorem OAI.TorsionFreeZeroDivisors.Types.letter_frequencyA line 399
Source documentation
Each of the 16516 letters has exactly np carriers on each side.
```
theorem letter_frequencyA (N : ℕ) (t : Letter) :
    Fintype.card {x : VertexA N // t ∈ outgoingA x} = 4260354 * N := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.outgoingA
theorem OAI.TorsionFreeZeroDivisors.Types.letter_frequencyB line 422
abbrev OAI.TorsionFreeZeroDivisors.Types.OrdinaryCode line 447
abbrev OAI.TorsionFreeZeroDivisors.Types.Generator line 448
abbrev OAI.TorsionFreeZeroDivisors.Types.Signed line 449
def OAI.TorsionFreeZeroDivisors.Types.pointCode line 453
Source documentation
The arbitrary pairing of the remaining ordinary letters is fixed once, using a cardinality equivalence; the first three partner the extras.
```
def pointCode : Point ≃ OrdinaryCode := Fintype.equivOfCardEq (by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.Point, OAI.TorsionFreeZeroDivisors.Types.OrdinaryCode
def OAI.TorsionFreeZeroDivisors.Types.signedLetter line 457
def OAI.TorsionFreeZeroDivisors.Types.inverse line 480
theorem OAI.TorsionFreeZeroDivisors.Types.inverse_signed line 483
theorem OAI.TorsionFreeZeroDivisors.Types.inverse_inverse line 486
theorem OAI.TorsionFreeZeroDivisors.Types.inverse_ne line 490
def OAI.TorsionFreeZeroDivisors.Types.MatchingTuple line 499
Source documentation
Each inverse pair receives a bijection between its two carrier sets.
```
def MatchingTuple := (g : Generator) →
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.Generator
theorem OAI.TorsionFreeZeroDivisors.Types.matchingTuple_nonempty line 504
Source documentation
Exact empirical balance ensures the finite matching space is nonempty.
```
theorem matchingTuple_nonempty [Fintype V]
    (hfreq : ∀ t u, Fintype.card {x : V // t ∈ outgoing x} =
      Fintype.card {x : V // u ∈ outgoing x}) : Nonempty (MatchingTuple outgoing) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.MatchingTuple
def OAI.TorsionFreeZeroDivisors.Types.nextSigned line 511
Source documentation
The direction of a step is given by the signed letter. Non-carrier values are immaterial and are defined to fix the vertex.
```
def nextSigned (M : MatchingTuple outgoing) (x : V) : Signed → V
  | (g,true) => if hx : signedLetter (g,true) ∈ outgoing x then (M g ⟨x,hx⟩).val else x
  | (g,false) => if hx : signedLetter (g,false) ∈ outgoing x then ((M g).symm ⟨x,hx⟩).val else x
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.MatchingTuple, OAI.TorsionFreeZeroDivisors.Types.Signed, OAI.TorsionFreeZeroDivisors.Types.signedLetter
def OAI.TorsionFreeZeroDivisors.Types.next line 515
theorem OAI.TorsionFreeZeroDivisors.Types.next_signed line 518
theorem OAI.TorsionFreeZeroDivisors.Types.next_reverse_mem line 522
theorem OAI.TorsionFreeZeroDivisors.Types.next_reverse_next line 529
theorem OAI.TorsionFreeZeroDivisors.Types.matchingA_nonempty line 544
Source documentation
In particular both source sides have an actual matching space. This makes no girth or arrangement claim about a chosen point in that space.
```
theorem matchingA_nonempty (N : ℕ) : Nonempty (MatchingTuple (@outgoingA N)) :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.MatchingTuple, OAI.TorsionFreeZeroDivisors.Types.outgoingA
theorem OAI.TorsionFreeZeroDivisors.Types.matchingB_nonempty line 547
theorem OAI.TorsionFreeZeroDivisors.Types.card_prod_both line 553
theorem OAI.TorsionFreeZeroDivisors.Types.slotA_extra_joint line 564
theorem OAI.TorsionFreeZeroDivisors.Types.slotB_extra_joint line 587
theorem OAI.TorsionFreeZeroDivisors.Types.line_single_card line 592
theorem OAI.TorsionFreeZeroDivisors.Types.line_joint_card line 596
theorem OAI.TorsionFreeZeroDivisors.Types.joint_ordinary line 605
Source documentation
Counts of joint carriers can be computed in a general independent line-slot-replica type, so both sides use literally the same geometry.
```
theorem joint_ordinary {S : Type*} [Fintype S] (extra : S → Finset (Fin 3))
    (N : ℕ) (p q : Point) (hpq : p ≠ q) :
    Fintype.card {x : Line × S × Fin N //
      Sum.inl p ∈ (pointsOn x.1).disjSum (extra x.2.1) ∧
      Sum.inl q ∈ (pointsOn x.1).disjSum (extra x.2.1)} = Fintype.card S * N := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.Point, OAI.TorsionFreeZeroDivisors.Types.Line, OAI.TorsionFreeZeroDivisors.Types.pointsOn
theorem OAI.TorsionFreeZeroDivisors.Types.joint_mixed line 618
theorem OAI.TorsionFreeZeroDivisors.Types.joint_extras line 633