RationalBernsteinTermination.lean

1 import KomorebiLSM.RationalBernsteinMargin
2 import KomorebiLSM.DyadicBernsteinCertificate
3 import KomorebiLSM.BernsteinCellPositivity
4 
5 /-! Strict actual margin guarantees eventual success of complete rational dyadic certificates. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RationalBernsteinTermination
8 open TensorBernsteinCertificate RationalBernsteinMargin RationalSemicircle
9 open LorentzCylinder RobustOrientedMargin
10 noncomputable section
11 
12 /-- The coefficient convergence is derived in BernsteinCellPositivity from exact rational coordinates. -/
13 theorem positive_polynomial_eventual (p : Polynomial₂)
14     (hp : ∀ x∈square.domain,0<value p x) :
15     ∃ N : ℕ,∀ M : ℕ,N≤M → Nonempty (UniformCertificate p square M) := by
16   obtain ⟨delta,hdelta,hcell⟩ := BernsteinCellPositivity.exists_small_positive p hp
17   exact eventually_uniform_dyadic delta hdelta hcell
18 
19 /-- Finitely many polynomials share one sufficiently fine depth, and every finer depth succeeds. -/
20 theorem finite_family_eventual {I : Type*} [Fintype I] (p : I → Polynomial₂)
21     (hp : ∀ i x,x∈square.domain → 0<value (p i) x) :
22     ∃ N : ℕ,∀ M : ℕ,N≤M → ∀ i,Nonempty (UniformCertificate (p i) square M) := by
23   classical
24   have he (i : I) := positive_polynomial_eventual (p i) (hp i)
25   choose depth hdepth using he
26   refine ⟨Finset.univ.sup depth,?_⟩
27   intro M hM i
28   exact hdepth i M ((Finset.le_sup (Finset.mem_univ i)).trans hM)
29 
30 variable {n : ℕ}
31 
32 theorem strict_polynomials_positive (G : Fin n → RationalMatrix) (kappa : ℚ)
33     (hmargin : ∀ u∈Set.Icc (-1 : ℝ) 1,
34       (kappa : ℝ)<sigma (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) u))
35     (left : Bool) :
36     (∀ x∈square.domain,0<value (orientationPolynomial G kappa left) x) ∧
37       (∀ x∈square.domain,0<value (squareGapPolynomial G kappa left) x) := by
38   have h (x : Fin 2 → ℝ) (hx : x∈square.domain) :=
39     strict_chart_tests (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) (x 0))
40       kappa (hmargin (x 0) ((square_domain x).mp hx 0)) left (x 1)
41   have he (x : Fin 2 → ℝ) : x=![x 0,x 1] := by
42     funext i
43     fin_cases i <;> rfl
44   constructor
45   · intro x hx
46     rw [he x,value_orientationPolynomial]
47     exact (h x hx).1
48   · intro x hx
49     rw [he x,value_squareGapPolynomial]
50     exact (h x hx).2
51 
52 /-- The selector is only a finite indexing of the two required tests; neither test is dropped. -/
53 def testPolynomial (G : Fin n → RationalMatrix) (kappa : ℚ) (which left : Bool) : Polynomial₂ :=
54   if which then squareGapPolynomial G kappa left else orientationPolynomial G kappa left
55 
56 /-- The same finite dyadic grid eventually certifies all actions and both tests in both charts. -/
57 theorem strict_family_eventual {A : Type*} [Fintype A]
58     (G : A → Fin n → RationalMatrix) (kappa : ℚ)
59     (hmargin : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 →
60       (kappa : ℝ)<sigma (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G a k)) u)) :
61     ∃ N : ℕ,∀ M : ℕ,N≤M → ∀ a which left,
62       Nonempty (UniformCertificate (testPolynomial (G a) kappa which left) square M) := by
63   have hp (q : A × Bool × Bool) (x : Fin 2 → ℝ) (hx : x∈square.domain) :
64       0<value (testPolynomial (G q.1) kappa q.2.1 q.2.2) x := by
65     have h := strict_polynomials_positive (G q.1) kappa (hmargin q.1) q.2.2
66     cases hwhich : q.2.1
67     · simpa [testPolynomial,hwhich] using h.1 x hx
68     · simpa [testPolynomial,hwhich] using h.2 x hx
69   obtain ⟨N,hN⟩ := finite_family_eventual
70     (fun q : A × Bool × Bool => testPolynomial (G q.1) kappa q.2.1 q.2.2) hp
71   exact ⟨N,fun M hM a which left => hN M hM (a,which,left)⟩
72 
73 /-- A strict actual curved margin supplies finite exact rational witnesses, with complete tree coverage. -/
74 theorem strict_family_certificate_exists {A : Type*} [Fintype A]
75     (G : A → Fin n → RationalMatrix) (kappa : ℚ)
76     (hmargin : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 →
77       (kappa : ℝ)<sigma (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G a k)) u)) :
78     Nonempty (∀ a,Certificate (G a) kappa) := by
79   obtain ⟨N,hN⟩ := strict_family_eventual G kappa hmargin
80   refine ⟨fun a => { orientationWitness := fun left => ?_,squareGapWitness := fun left => ?_ }⟩
81   · exact (hN N le_rfl a false left).some.toSubdivision
82   · exact (hN N le_rfl a true left).some.toSubdivision
83 
84 end
85 end Komorebi.LSM.RationalBernsteinTermination

Back to source controls