OAI/RingTheory/DirectFiniteness/PrescribedIncidence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KaplanskyCounterexample.Prescription.Successful line 10
2. lemma OAI.KaplanskyCounterexample.Prescription.DirectionFrame.tradeLine_injective line 29
3. lemma OAI.KaplanskyCounterexample.Prescription.successful_of_indexed line 48

   Source documentation

   A faithful set of full lines from the successful geometric trade; the bijection retains degrees and ordinary incidence girth exactly.

   lemma successful_of_indexed {Q : Type} [Field Q] [Fintype Q] {q n ℓ : ℕ}
       (a : Fin q ≃ Q) (O : Finset (Fin n → Q))
       (hO : O ⊆ simplexPoints a n ((q-2)/2))
       (hlow : 2*q^n ≤ O.card*(ℓ+1)^2) (hhigh : O.card*(ℓ+1)^2 ≤ 7*q^n)
       {I : Type} [Fintype I] (L : I → Finset (Fin n → Q)) (hinj : Function.Injective L)
       (hfull : ∀ i, FullLine (Q := Q) (L i))
   …

   Mentions: OAI.KaplanskyCounterexample.Prescription.Q

4. lemma OAI.KaplanskyCounterexample.Prescription.succeeds_217 line 88

   Source documentation

   Uniformity in every enumeration and realization of F_(2^217), required by the literal outer search (whose field is the lexicographic quotient).

   lemma succeeds_217 (Q : Type) [Field Q] [Fintype Q] [CharP Q 2]
       (hq : Fintype.card Q=sourceQ) (a : Fin sourceQ ≃ Q) :
       ∃ pair : Finset (Fin 1200 → Q) × Finset (Finset (Fin 1200 → Q)),
         Successful a sourcePrime pair := by
   …

   Mentions: OAI.KaplanskyCounterexample.Prescription.Q, OAI.KaplanskyCounterexample.Prescription.Successful