OAI/Geometry/PinnedDistances/ArithmeticSequence.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakPinned.graph_sequence_of_failure line 15

   Source documentation

   Diagonalized extraction of genuine configurations. The errors tend to zero and vertex numbers tend to infinity.

   theorem graph_sequence_of_failure (hfail : ¬ MainStatement) :
       ∃ c s γ : ℝ, 0<c ∧ c<γ ∧ γ<s ∧ s<1 ∧ 0<Theta s ∧
         ∃ (P : ℕ → Finset Plane) (C : ∀ j, Finset (P j)),
           (∀ j, j<(C j).card) ∧
           ∀ j, PreparedGraph (C j) ((planarFibers (P j) s).Active (cutoff s (P j).card) (C j))
             (coreGraph (P j) s (C j)) (Theta s) γ c (Theta s/(j+2)) := by
   …

   Mentions: OAI.WeakPinned.MainStatement, OAI.WeakPinned.Theta, OAI.WeakPinned.Plane, OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.planarFibers, OAI.WeakPinned.cutoff, OAI.WeakPinned.coreGraph

2. lemma OAI.WeakPinned.graph_card_tendsto line 32
3. lemma OAI.WeakPinned.graph_error_tendsto line 36
4. theorem OAI.WeakPinned.Transfer.equations line 52

   Source documentation

   A system of rational polynomial equations with a complex solution has an algebraic solution. No finite set assumption on the equations is needed.

   theorem equations {ι : Type u1} [Finite ι]
       (S : Set (MvPolynomial ι ℚ)) (x : ι → ℂ)
       (hx : ∀ p ∈ S, aeval x p = 0) :
       ∃ y : ι → AlgebraicClosure ℚ, ∀ p ∈ S, aeval y p = 0 := by
   …

5. theorem OAI.WeakPinned.Transfer.equations_and_inequations line 71

   Source documentation

   Simultaneous equations and finitely many inequations transfer to algebraic coordinates. The inverse-variable equation enforces every inequation.

   theorem equations_and_inequations {ι : Type u2} [Finite ι]
       (S : Set (MvPolynomial ι ℚ)) (T : Finset (MvPolynomial ι ℚ)) (x : ι → ℂ)
       (hx : ∀ p ∈ S, aeval x p = 0) (hT : ∀ p ∈ T, aeval x p ≠ 0) :
       ∃ y : ι → AlgebraicClosure ℚ,
         (∀ p ∈ S, aeval y p = 0) ∧ (∀ p ∈ T, aeval y p ≠ 0) := by
   …

6. theorem OAI.WeakPinned.Transfer.numberField_pattern line 107

   Source documentation

   The algebraic realization lies in a single number field generated by its finitely many coordinates. The field is not fixed in advance.

   theorem numberField_pattern {ι : Type u3} [Finite ι]
       (S : Set (MvPolynomial ι ℚ)) (T : Finset (MvPolynomial ι ℚ)) (x : ι → ℂ)
       (hx : ∀ p ∈ S, aeval x p = 0) (hT : ∀ p ∈ T, aeval x p ≠ 0) :
       ∃ K : IntermediateField ℚ (AlgebraicClosure ℚ), NumberField K ∧
         ∃ y : ι → K, (∀ p ∈ S, aeval y p = 0) ∧ (∀ p ∈ T, aeval y p ≠ 0) := by
   …

7. theorem OAI.WeakPinned.Transfer.numberField_zero_pattern line 134

   Source documentation

   Preservation of an arbitrary finite zero-pattern, simultaneously, in one number field. In particular this preserves all selected equalities exactly.

   theorem numberField_zero_pattern {ι : Type u4} [Finite ι]
       (T : Finset (MvPolynomial ι ℚ)) (x : ι → ℂ) :
       ∃ K : IntermediateField ℚ (AlgebraicClosure ℚ), NumberField K ∧
         ∃ y : ι → K, ∀ p ∈ T, aeval y p = 0 ↔ aeval x p = 0 := by
   …

8. abbrev OAI.WeakPinned.Transfer.Plane line 150
9. abbrev OAI.WeakPinned.Transfer.Variables line 154

   Source documentation

   Complexified variables; the extra variable forces a square root of -1 into the field, so every archimedean place is complex.

   abbrev Variables (ι : Type u5) := Option (Bool × ι)

10. def OAI.WeakPinned.Transfer.secondCoord line 156
11. def OAI.WeakPinned.Transfer.complexAssignment line 159
12. def OAI.WeakPinned.Transfer.distancePoly line 162
13. lemma OAI.WeakPinned.Transfer.eval_distancePoly line 166
14. theorem OAI.WeakPinned.Transfer.planar_factor_model line 178

    Source documentation

    Every finite real planar configuration has a faithful number-field model for BOTH distance factors. The real configuration is not restricted or replaced: the exact equality pattern of ALL its distances is retained. The factorization at every place does not require conjugacy in the new field.

    theorem planar_factor_model {ι : Type u9} [Finite ι]
        (x : ι → Plane) (hx : Function.Injective x) :
        ∃ K : IntermediateField ℚ (AlgebraicClosure ℚ), NumberField K ∧
          ∃ (ii : K) (Z₁ Z₂ : ι → K), ii ^ 2 = -1 ∧
            Function.Injective Z₁ ∧ Function.Injective Z₂ ∧
            ∀ a b c d, (Z₁ a - Z₁ b) * (Z₂ a - Z₂ b) =
              (Z₁ c - Z₁ d) * (Z₂ c - Z₂ d) ↔ dist (x a) (x b) = dist (x c) (x d) := by
    …

    Mentions: OAI.WeakPinned.Transfer.Plane

15. theorem OAI.WeakPinned.core_arithmetic_model line 240

    Source documentation

    The exact arithmetic model for each extracted real graph. No point is assumed algebraic; the original graph's complete distance-equality pattern is preserved by the proved finite specialization theorem.

    theorem core_arithmetic_model (P : Finset Plane) (s : ℝ) (C : Finset P)
        (hne : ∀ e, ((coreGraph P s C).targets e).Nonempty) :
        ∃ K : IntermediateField ℚ (AlgebraicClosure ℚ), NumberField K ∧
          ∃ (ii : K) (Z₁ Z₂ : C → K) (t : (planarFibers P s).Active (cutoff s P.card) C → K),
            ii^2 = -1 ∧ Function.Injective Z₁ ∧ Function.Injective Z₂ ∧
            (∀ e, t e ≠ 0) ∧
            (∀ e y, y ∈ (coreGraph P s C).targets e →
              (Z₁ ((coreGraph P s C).source e)-Z₁ y)*(Z₂ ((coreGraph P s C).source e)-Z₂ y)=t e) ∧
            (∀ a b c d : C, (Z₁ a-Z₁ b)*(Z₂ a-Z₂ b)=(Z₁ c-Z₁ d)*(Z₂ c-Z₂ d) ↔
              dist a.val.val b.val.val=dist c.val.val d.val.val) := by
    …

    Mentions: OAI.WeakPinned.Plane, OAI.WeakPinned.coreGraph, OAI.WeakPinned.planarFibers, OAI.WeakPinned.cutoff

16. lemma OAI.WeakPinned.PreparedGraph.targets_nonempty line 270
17. theorem OAI.WeakPinned.sequence_arithmetic_model line 280

    Source documentation

    Specialization is available independently for EVERY graph in the genuine counterexample sequence, over number fields of unrestricted degree.

    theorem sequence_arithmetic_model (hfail : ¬ MainStatement) :
        ∃ c s γ : ℝ, 0<c ∧ c<γ ∧ γ<s ∧ s<1 ∧ 0<Theta s ∧
          ∃ (P : ℕ → Finset Plane) (C : ∀ j, Finset (P j)),
            (∀ j, j<(C j).card) ∧
            (∀ j, PreparedGraph (C j) ((planarFibers (P j) s).Active (cutoff s (P j).card) (C j))
              (coreGraph (P j) s (C j)) (Theta s) γ c (Theta s/(j+2))) ∧
            ∀ j, ∃ K : IntermediateField ℚ (AlgebraicClosure ℚ), NumberField K ∧
              ∃ (ii : K) (Z₁ Z₂ : C j → K) (t : (planarFibers (P j) s).Active (cutoff s (P j).card) (C j) → K),
                ii^2 = -1 ∧ Function.Injective Z₁ ∧ Function.Injective Z₂ ∧
                (∀ e, t e ≠ 0) ∧
                (∀ e y, y ∈ (coreGraph (P j) s (C j)).targets e →
                  (Z₁ ((coreGraph (P j) s (C j)).source e)-Z₁ y)*(Z₂ ((coreGraph (P j) s (C j)).source e)-Z₂ y)=t e) := by
    …

    Mentions: OAI.WeakPinned.MainStatement, OAI.WeakPinned.Theta, OAI.WeakPinned.Plane, OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.planarFibers, OAI.WeakPinned.cutoff, OAI.WeakPinned.coreGraph