OAI/NumberTheory/Ostmann/Construction/WordTransferReplay.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.wordTransferLeafValue line 11

   Source documentation

   At a leaf, the state contains the original word whose Fourier factor is evaluated. Internal states are never queried by the leaf list.

   noncomputable def wordTransferLeafValue {σ : Type*} : WordTransferState σ → ℕ
     | ⟨0, .leaf word, x⟩ => (word.map x).prod
     | ⟨_ + 1, _, _⟩ => 1

   Mentions: OAI.Ostmann.WordTransferState

2. def OAI.Ostmann.wordTransferSignedLeaf line 15
3. theorem OAI.Ostmann.WordTransferTemplate.branching_valid line 19
4. theorem OAI.Ostmann.wordTransferSignedLeaf_flip line 37
5. theorem OAI.Ostmann.WordTransferTemplate.branching_leaves line 44
6. theorem OAI.Ostmann.WordTransferTemplate.polynomial_gates line 71

   Source documentation

   Thus the actual arithmetic history has the explicitly constructed polynomial divisibility gates needed by the one-sided estimate.

   theorem WordTransferTemplate.polynomial_gates {σ : Type*} {n : ℕ}
       (template : WordTransferTemplate σ n) (x : σ → ℕ) (t : FrequencyTree ℤ n)
       (hn : NonzeroInternalFrequencies n t)
       (hv : ValidTransferHistory (wordTransferSystem σ) n (template.state x) t) :
       ∀ F ∈ (template.branching t hn).pivotFormulas .prime,
         F.cleared.denominator ∣ MvPolynomial.eval₂Hom (RingHom.id ℤ)
           (fun i => (x i : ℤ)) F.cleared.numerator :=
   …

   Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem