EllipsoidDiscoveryP63.lean

1 import KomorebiLSM.EllipsoidDiscovery
2 import KomorebiLSM.EllipsoidPolynomial
3 
4 /-! P63 separates the operator-only geometry proposal from acceptance. The
5 actual fitted family supplies the ratio and rank-one anchor; probability
6 meaning is obtained only from the full P62 quadratic/orientation witnesses,
7 exact integrated mass, and a normalized initial state in the proposed cone. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.EllipsoidDiscoveryP63
10 open EllipsoidDiscovery MeasureTheory ProbabilityTheory
11 open scoped BigOperators Matrix
12 
13 variable {D A : Type*} [Fintype D] [DecidableEq D]
14 
15 /-- Evaluation is the literal matrix polynomial of the fitted coefficients. -/
16 noncomputable def evaluatedBranch {n : ℕ}
17     (B : A → Fin n → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) (a : A) (u : ℝ) :
18     Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ :=
19   PolynomialGram.evalMatrix (OrientedEllipsoid.matrixPolynomial (B a)) u
20 
21 noncomputable def fittedRatio {n : ℕ}
22     (B : A → Fin n → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) (a b : A) (u : ℝ) :
23     Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ :=
24   ratio (evaluatedBranch B a u) (evaluatedBranch B b u)
25 
26 noncomputable def proposedCenter {n : ℕ}
27     (B : A → Fin n → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) (a b : A) (u : ℝ) : D → ℝ :=
28   fixedCenter (spatialBlock (fittedRatio B a b u)) (translation (fittedRatio B a b u))
29 
30 noncomputable def anchorDisplacement {n : ℕ}
31     (B : A → Fin n → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
32     (a b k : A) (u v : ℝ) (z : State D) : D → ℝ :=
33   spatial (normalizedImage (evaluatedBranch B k v).mulVecLin z)-proposedCenter B a b u
34 
35 noncomputable def proposedMetric {n : ℕ}
36     (B : A → Fin n → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
37     (a b k : A) (u v : ℝ) (z : State D) (H₀ : Matrix D D ℝ) : Matrix D D ℝ :=
38   normalizedMetric H₀ (anchorDisplacement B a b k u v z)
39 
40 variable [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
41 variable {n : ℕ} (B : A → Fin n → Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
42 variable (a b k : A) (u v : ℝ) (z : State D) (H₀ : Matrix D D ℝ)
43 
44 local notation "F" => fittedRatio B a b u
45 local notation "c" => proposedCenter B a b u
46 local notation "L" => Matrix.mulVecLin (evaluatedBranch B k v)
47 local notation "δ" => anchorDisplacement B a b k u v z
48 local notation "H" => proposedMetric B a b k u v z H₀
49 
50 /-- Full P63 acceptance retains every P62 hypothesis on the complete fitted
51 family. Neither ratio invariance nor a chosen boundary image is used as a
52 substitute for the oriented quadratic certificate. -/
53 theorem conditional_operator_only_ellipsoid_discovery
54     (hu : u∈Set.Icc (-1 : ℝ) 1) (hv : v∈Set.Icc (-1 : ℝ) 1)
55     (hₐ : IsUnit (evaluatedBranch B a u).det) (hratio : IsUnit F)
56     (hmass : mass.comp (F).mulVecLin=mass) (hcenter : IsUnit (1-spatialBlock F).det)
57     (hdim : Module.finrank ℝ (invariantForms (spatialBlock F))=1)
58     (hinvariant : H₀∈invariantForms (spatialBlock F)) (hpositive : H₀.PosDef)
59     (hrank : Module.finrank ℝ (L).range=1) (hanchor : mass (L z)≠0)
60     (hdisplacement : spatial (normalizedImage L z)≠c)
61     (branches : ∀ action obs,obs∈Set.Icc (-1 : ℝ) 1 →
62       OrientedEllipsoid.BranchCertificate c H (evaluatedBranch B action obs))
63     (hmoments : ∀ action x,OrientedEllipsoid.mass
64       ((∑ j : Fin n,UniformIntervalMoments.moment j • OrientedEllipsoid.matrixOperator (B action j)) x)=
65         OrientedEllipsoid.mass x)
66     (z₀ : State D) (hinitial : z₀∈OrientedEllipsoid.cone c H ∧ OrientedEllipsoid.mass z₀=1) :
67     let hH : (H).PosDef := normalizedMetric_posDef hpositive (sub_ne_zero.mpr hdisplacement)
68     let I := OrientedEllipsoid.polynomialDensityInstrument c H hH B branches hmoments
69     (u∈Set.Icc (-1 : ℝ) 1 ∧ v∈Set.Icc (-1 : ℝ) 1) ∧
70     IsUnit F ∧ F=affineMatrix (translation F) (spatialBlock F) ∧
71     (∃! x : D → ℝ,F *ᵥ point 1 x=point 1 x) ∧
72     normalizedImage L z=point 1 (spatial (normalizedImage L z)) ∧
73     H∈invariantForms (spatialBlock F) ∧ (H).PosDef ∧ quadratic H δ=1 ∧
74     (∀ K : Matrix D D ℝ,K∈invariantForms (spatialBlock F) → quadratic K δ=1 → K=H) ∧
75     (∀ scale : ℝ,0<scale → normalizedMetric (scale • H₀) δ=H) ∧
76     (∀ action obs,obs∈Set.Icc (-1 : ℝ) 1 → ∀ x∈OrientedEllipsoid.cone c H,
77       evaluatedBranch B action obs *ᵥ x∈OrientedEllipsoid.cone c H) ∧
78     (∀ action obs x,I.op action obs x=evaluatedBranch B action obs *ᵥ x) ∧
79     (∀ action,IsMarkovKernel (I.kernel action)) ∧
80     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ T,
81       IsProbabilityMeasure (ContinuousRecords.recordLaw I π z₀ T)) ∧
82     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ T,
83       (ContinuousRecords.recordLaw I π z₀ (T+1)).fst=ContinuousRecords.recordLaw I π z₀ T) ∧
84     (∀ actions : ℕ → A,∀ T,
85       IsProbabilityMeasure (ContinuousRecords.observationLaw I actions z₀ T)) ∧
86     (∀ actions : ℕ → A,∀ T,
87       (ContinuousRecords.observationLaw I actions z₀ (T+1)).fst=
88         ContinuousRecords.observationLaw I actions z₀ T) ∧
89     (∀ actions : ℕ → A,∀ T (S : Set (ContinuousRecords.History ℝ T)),MeasurableSet S →
90       ContinuousRecords.observationLaw I actions z₀ T S=
91         ∫⁻ h in S,ENNReal.ofReal (OrientedEllipsoid.mass (ContinuousRecords.observationRun I actions z₀ T h))
92           ∂ContinuousRecords.reference UniformIntervalMoments.measure T) := by
93   dsimp only
94   have hH : (H).PosDef := normalizedMetric_posDef hpositive (sub_ne_zero.mpr hdisplacement)
95   let I := OrientedEllipsoid.polynomialDensityInstrument c H hH B branches hmoments
96   have hbase : z₀∈(OrientedEllipsoid.probabilityCone c H hH).base := hinitial
97   have hᵦ : IsUnit (evaluatedBranch B b u).det := by
98     have hprod := hratio.mul ((Matrix.isUnit_iff_isUnit_det _).mpr hₐ)
99     have he : F * evaluatedBranch B a u=evaluatedBranch B b u :=
100       ratio_reconstructs _ _ hₐ
101     rw [he] at hprod
102     exact (Matrix.isUnit_iff_isUnit_det _).mp hprod
103   rcases operator_only_proposal (evaluatedBranch B a u) (evaluatedBranch B b u)
104     hₐ hᵦ hmass hcenter H₀ hdim hinvariant hpositive L hrank z hanchor hdisplacement with
105     ⟨hunit,hblock,hfixed,_,hnormalized,_,hform,hpd,hboundary,hunique⟩
106   refine ⟨⟨hu,hv⟩,hunit,hblock,hfixed,hnormalized,hform,hpd,hboundary,hunique,?_,?_,?_,?_,?_,?_,?_,?_,?_⟩
107   · intro scale hscale
108     exact positive_scale_independent scale hscale hpositive (sub_ne_zero.mpr hdisplacement)
109   · intro action obs hobs x hx
110     exact (branches action obs hobs).preserves hH hx
111   · intro action obs x
112     change OrientedEllipsoid.polynomialOperator (B action) obs x=evaluatedBranch B action obs *ᵥ x
113     rw [OrientedEllipsoid.polynomialOperator_matrix,OrientedEllipsoid.matrixOperator_apply]
114     rfl
115   · intro action
116     infer_instance
117   · intro π T
118     exact ContinuousRecords.recordLaw_probability I π ⟨z₀,hbase⟩ T
119   · intro π T
120     exact ContinuousRecords.recordLaw_consistent I π hbase.1 T
121   · intro actions T
122     exact ContinuousRecords.observationLaw_probability I actions ⟨z₀,hbase⟩ T
123   · intro actions T
124     exact ContinuousRecords.observationLaw_consistent I actions hbase.1 T
125   · intro actions T S hS
126     exact ContinuousRecords.observationLaw_product_density I actions z₀ T S hS
127 
128 /-- A replayed finite P62 SOS/Gram/coefficient certificate for the computed
129 geometry discharges the whole-family tests. Probability validity still needs
130 the explicit normalized initial state, and is separate from proposal success. -/
131 theorem finite_certificate_all_horizons
132     (hpositive : H₀.PosDef) (hdisplacement : spatial (normalizedImage L z)≠c)
133     {q bound : ℕ} (cert : OrientedEllipsoid.PolynomialCertificate c H B q bound)
134     (z₀ : State D) (hinitial : z₀∈OrientedEllipsoid.cone c H ∧ OrientedEllipsoid.mass z₀=1) :
135     let hH : (H).PosDef := normalizedMetric_posDef hpositive (sub_ne_zero.mpr hdisplacement)
136     (∀ word : List (A × ℝ),(∀ s∈word,s.2∈Set.Icc (-1 : ℝ) 1) →
137       0≤OrientedEllipsoid.mass (FiniteInstruments.wordAction
138         (fun s : A × ℝ => (OrientedEllipsoid.polynomialOperator (B s.1) s.2).toLinearMap) word z₀)) ∧
139     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ T,
140       IsProbabilityMeasure (ContinuousRecords.recordLaw (cert.instrument hH) π z₀ T)) ∧
141     (∀ actions : ℕ → A,∀ T,
142       IsProbabilityMeasure (ContinuousRecords.observationLaw (cert.instrument hH) actions z₀ T)) ∧
143     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ T extra,
144       (ContinuousRecords.recordLaw (cert.instrument hH) π z₀ (T+extra)).map
145         (ContinuousRecords.truncate T extra)=ContinuousRecords.recordLaw (cert.instrument hH) π z₀ T) := by
146   dsimp only
147   let hH : (H).PosDef := normalizedMetric_posDef hpositive (sub_ne_zero.mpr hdisplacement)
148   exact ⟨fun word hword => cert.word_mass_nonneg hH word hword hinitial.1,
149     fun π T => cert.record_law_probability hH π z₀ hinitial.1 hinitial.2 T,
150     fun actions T => cert.observation_law_probability hH actions z₀ hinitial.1 hinitial.2 T,
151     fun π T extra => cert.record_law_prefix hH π z₀ hinitial.1 T extra⟩
152 
153 end Komorebi.LSM.EllipsoidDiscoveryP63

Back to source controls