Section88CertifiedRepair.lean

1 import KomorebiLSM.Section88ProposedDirectPosOrientation
2 import KomorebiLSM.Section88ProposedDirectPosGap
3 import KomorebiLSM.Section88ProposedDirectNegOrientation
4 import KomorebiLSM.Section88ProposedDirectNegGap
5 import KomorebiLSM.Section88ProposedRotatedPosOrientation
6 import KomorebiLSM.Section88ProposedRotatedPosGap
7 import KomorebiLSM.Section88ProposedRotatedNegOrientation
8 import KomorebiLSM.Section88ProposedRotatedNegGap
9 import KomorebiLSM.Section88ComparisonDirectPosOrientation
10 import KomorebiLSM.Section88ComparisonDirectPosGap
11 import KomorebiLSM.Section88ComparisonDirectNegOrientation
12 import KomorebiLSM.Section88ComparisonDirectNegGap
13 import KomorebiLSM.Section88ComparisonRotatedPosOrientation
14 import KomorebiLSM.Section88ComparisonRotatedPosGap
15 import KomorebiLSM.Section88ComparisonRotatedNegOrientation
16 import KomorebiLSM.Section88ComparisonRotatedNegGap
17 import KomorebiLSM.Section88ComparisonBudget
18 import KomorebiLSM.MeasureTVCalculus
19 
20 /-! Full Section 88 repair: the recorded finite witnesses certify both domains,
21 the declared output uncertainty is retained, and the comparison law bound is
22 charged the actual reset cost. No empirical coverage assertion is made. -/
23 set_option autoImplicit false
24 set_option maxHeartbeats 1200000
25 namespace Komorebi.LSM.Section88CertifiedRepair
26 open scoped BigOperators
27 open LorentzCylinder RobustOrientedMargin RationalBernsteinMargin RationalLorentzMatrix
28 open PerturbedOperatorFixture ContinuousInstrument MeasureTheory UniformIntervalMoments
29 noncomputable section
30 
31 def proposedCertificate (a : Bool) : Certificate (nominalProposed a) (1/16) where
32   orientationWitness left := by
33     cases a <;> cases left
34     · exact Section88ProposedDirectPosOrientation.certifiedWitness
35     · exact Section88ProposedDirectNegOrientation.certifiedWitness
36     · exact Section88ProposedRotatedPosOrientation.certifiedWitness
37     · exact Section88ProposedRotatedNegOrientation.certifiedWitness
38   squareGapWitness left := by
39     cases a <;> cases left
40     · exact Section88ProposedDirectPosGap.certifiedWitness
41     · exact Section88ProposedDirectNegGap.certifiedWitness
42     · exact Section88ProposedRotatedPosGap.certifiedWitness
43     · exact Section88ProposedRotatedNegGap.certifiedWitness
44 
45 theorem proposed_moment_mass (a : Bool) (z : State ℂ) :
46     probabilityCone.mass ((∑ k : Fin 3,moment k • matrixOperator (nominalProposed a k)) z)=
47       probabilityCone.mass z := by
48   apply Section88ComparisonBudget.moment_mass_of_rows (nominalProposed a) (11/32) (63/32) _ _ (by norm_num) z
49   · intro j
50     cases a <;> fin_cases j <;> norm_num [Matrix.cons_val_two]
51   · intro j
52     cases a <;> fin_cases j <;> norm_num [Matrix.cons_val_two]
53 
54 def proposedInstrument : DensityInstrument (A := Bool) (probabilityCone (V := ℂ)) measure :=
55   certifiedInstrument nominalProposed (1/16) proposedCertificate (by norm_num) proposed_moment_mass
56 
57 theorem proposed_margin (a : Bool) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) :
58     (1/16 : ℝ)≤sigma (proposedInstrument.op a u) := by
59   have h := (proposedCertificate a).margin u hu
60   norm_num at h
61   exact h
62 
63 def comparisonCertificate (a : Bool) : Certificate (nominalComparison a) (1/16) where
64   orientationWitness left := by
65     cases a <;> cases left
66     · exact Section88ComparisonDirectPosOrientation.certifiedWitness
67     · exact Section88ComparisonDirectNegOrientation.certifiedWitness
68     · exact Section88ComparisonRotatedPosOrientation.certifiedWitness
69     · exact Section88ComparisonRotatedNegOrientation.certifiedWitness
70   squareGapWitness left := by
71     cases a <;> cases left
72     · exact Section88ComparisonDirectPosGap.certifiedWitness
73     · exact Section88ComparisonDirectNegGap.certifiedWitness
74     · exact Section88ComparisonRotatedPosGap.certifiedWitness
75     · exact Section88ComparisonRotatedNegGap.certifiedWitness
76 
77 theorem comparison_moment_mass (a : Bool) (z : State ℂ) :
78     probabilityCone.mass ((∑ k : Fin 3,moment k • matrixOperator (nominalComparison a k)) z)=
79       probabilityCone.mass z := by
80   apply Section88ComparisonBudget.moment_mass_of_rows (nominalComparison a) (11/32) (63/32) _ _ (by norm_num) z
81   · intro j
82     cases a <;> fin_cases j <;> norm_num [Matrix.cons_val_two]
83   · intro j
84     cases a <;> fin_cases j <;> norm_num [Matrix.cons_val_two]
85 
86 def comparisonInstrument : DensityInstrument (A := Bool) (probabilityCone (V := ℂ)) measure :=
87   certifiedInstrument nominalComparison (1/16) comparisonCertificate (by norm_num) comparison_moment_mass
88 
89 theorem comparison_margin (a : Bool) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) :
90     (1/16 : ℝ)≤sigma (comparisonInstrument.op a u) := by
91   have h := (comparisonCertificate a).margin u hu
92   norm_num at h
93   exact h
94 
95 /-- The supplied physical center has the same normalized center image in both atlases. -/
96 theorem initial_atlases :
97     matrixOperator proposedTransform (1,(⟨1/2,1/2⟩ : ℂ))=(1,0) ∧
98     matrixOperator comparisonTransform (1,(⟨1/2,1/2⟩ : ℂ))=(1,0) := by
99   constructor <;> apply coordinate_ext <;> intro i
100   all_goals rw [coordinate_matrixOperator]
101   all_goals fin_cases i <;>
102     norm_num [proposedTransform,comparisonTransform,coordinate,Fin.sum_univ_succ,Matrix.cons_val_two]
103 
104 theorem initial_mem : (1,(0 : ℂ))∈probabilityCone.base := by
105   rw [mem_base]
106   constructor <;> norm_num
107 
108 /-- Complete replay implies all-horizon internal validity, including the actual center. -/
109 theorem nominal_record_probability (policy : ContinuousRecords.Policy (A := Bool) (Y := ℝ)) (N : ℕ) :
110     IsProbabilityMeasure (ContinuousRecords.recordLaw proposedInstrument policy (1,0) N) :=
111   ContinuousRecords.recordLaw_probability proposedInstrument policy ⟨(1,0),initial_mem⟩ N
112 
113 /-- The declared output budgets leave the exact residual slack 3/64. -/
114 theorem robust_residual (Delta : State ℂ →L[ℝ] State ℂ) (a : Bool) (u : ℝ)
115     (hu : u∈Set.Icc (-1 : ℝ) 1)
116     (h0 : ∀ v : ℂ,‖v‖≤1 → |(Delta (1,v)).1|≤1/128)
117     (h1 : ∀ v : ℂ,‖v‖≤1 → ‖(Delta (1,v)).2‖≤1/128) :
118     (3/64 : ℝ)≤sigma (proposedInstrument.op a u+Delta) := by
119   have h := residual_margin _ Delta (1/16) (1/128) (1/128)
120     (proposed_margin a u hu) h0 h1
121   norm_num at h ⊢
122   exact h
123 
124 theorem uncertaintyCertificate
125     (E : Bool → Fin 3 → State ℂ →L[ℝ] State ℂ)
126     (h0 : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : ℂ,‖v‖≤1 →
127       |(PolynomialGram.operatorPolynomial (E a) u (1,v)).1|≤1/128)
128     (h1 : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : ℂ,‖v‖≤1 →
129       ‖(PolynomialGram.operatorPolynomial (E a) u (1,v)).2‖≤1/128) :
130     MarginCertificate (fun a k => matrixOperator (nominalProposed a k)) E
131       (fun _ _ => 1/16) (fun _ _ => 1/128) (fun _ _ => 1/128) where
132   margin := proposed_margin
133   mass_error := h0
134   spatial_error := h1
135   cover := by intros; norm_num
136 
137 /-- The uncertainty family is a normalized probability model only with its exact mass constraint. -/
138 def uncertainInstrument
139     (E : Bool → Fin 3 → State ℂ →L[ℝ] State ℂ)
140     (h0 : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : ℂ,‖v‖≤1 →
141       |(PolynomialGram.operatorPolynomial (E a) u (1,v)).1|≤1/128)
142     (h1 : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : ℂ,‖v‖≤1 →
143       ‖(PolynomialGram.operatorPolynomial (E a) u (1,v)).2‖≤1/128)
144     (hm : ∀ a z,probabilityCone.mass ((∑ k : Fin 3,moment k • E a k) z)=0) :
145     DensityInstrument (A := Bool) (probabilityCone (V := ℂ)) measure :=
146   RobustOrientedMargin.uncertainInstrument _ E _ _ _ (uncertaintyCertificate E h0 h1) (by
147     intro a z
148     simp only [smul_add,Finset.sum_add_distrib,add_apply,map_add]
149     rw [proposed_moment_mass,hm]
150     ring)
151 
152 /-- Every degree-two matrix-entry perturbation in the declared box obeys those output budgets. -/
153 theorem coefficient_box_output (E : Bool → Fin 3 → ComplexCoefficientBox.RealMatrix)
154     (hE : ∀ a k i j,|E a k i j|≤1/4096) (a : Bool) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
155     (v : ℂ) (hv : ‖v‖≤1) :
156     |(PolynomialGram.operatorPolynomial (fun k => ComplexCoefficientBox.matrixOperator (E a k)) u (1,v)).1|≤1/128 ∧
157     ‖(PolynomialGram.operatorPolynomial (fun k => ComplexCoefficientBox.matrixOperator (E a k)) u (1,v)).2‖≤1/128 := by
158   have h := ComplexCoefficientBox.polynomial_output_bounds (E a) (fun _ => 1/4096) (hE a) u hu v hv
159   norm_num [Fin.sum_univ_succ] at h
160   constructor <;> linarith [h.1,h.2]
161 
162 theorem uncertain_record_probability
163     (E : Bool → Fin 3 → State ℂ →L[ℝ] State ℂ)
164     (h0 : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : ℂ,‖v‖≤1 →
165       |(PolynomialGram.operatorPolynomial (E a) u (1,v)).1|≤1/128)
166     (h1 : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : ℂ,‖v‖≤1 →
167       ‖(PolynomialGram.operatorPolynomial (E a) u (1,v)).2‖≤1/128)
168     (hm : ∀ a z,probabilityCone.mass ((∑ k : Fin 3,moment k • E a k) z)=0)
169     (policy : ContinuousRecords.Policy (A := Bool) (Y := ℝ)) (N : ℕ) :
170     IsProbabilityMeasure (ContinuousRecords.recordLaw (uncertainInstrument E h0 h1 hm) policy (1,0) N) :=
171   ContinuousRecords.recordLaw_probability _ policy ⟨(1,0),initial_mem⟩ N
172 
173 
174 /-- The exact coefficient box, intersected with its mass affine subspace, is an actual all-horizon model family. -/
175 def coefficientBoxInstrument (E : Bool → Fin 3 → ComplexCoefficientBox.RealMatrix)
176     (hE : ∀ a k i j,|E a k i j|≤1/4096)
177     (hm : ∀ a z,probabilityCone.mass ((∑ k : Fin 3,moment k •
178       ComplexCoefficientBox.matrixOperator (E a k)) z)=0) :
179     DensityInstrument (A := Bool) (probabilityCone (V := ℂ)) measure :=
180   uncertainInstrument (fun a k => ComplexCoefficientBox.matrixOperator (E a k))
181     (fun a u hu v hv => (coefficient_box_output E hE a u hu v hv).1)
182     (fun a u hu v hv => (coefficient_box_output E hE a u hu v hv).2) hm
183 
184 theorem coefficient_box_record_probability (E : Bool → Fin 3 → ComplexCoefficientBox.RealMatrix)
185     (hE : ∀ a k i j,|E a k i j|≤1/4096)
186     (hm : ∀ a z,probabilityCone.mass ((∑ k : Fin 3,moment k •
187       ComplexCoefficientBox.matrixOperator (E a k)) z)=0)
188     (policy : ContinuousRecords.Policy (A := Bool) (Y := ℝ)) (N : ℕ) :
189     IsProbabilityMeasure (ContinuousRecords.recordLaw (coefficientBoxInstrument E hE hm) policy (1,0) N) :=
190   ContinuousRecords.recordLaw_probability _ policy ⟨(1,0),initial_mem⟩ N
191 
192 def resetProfile : InteriorRepair.ResetProfile (A := Bool) where
193   density _ _ := 1
194   measurable_density _ := measurable_const
195   integrable_density _ := integrable_const _
196   minimum := 1
197   minimum_positive := by norm_num
198   lower := by intros; norm_num
199   integral_one := by intro a; simp
200 
201 /-- The comparison certificate checks exactly the declared one-eighth reset of the raw fit. -/
202 theorem comparison_is_repair (a : Bool) (u : ℝ) :
203     comparisonInstrument.op a u=InteriorRepair.repair
204       (Section88ComparisonBudget.rawEstimate.op a u) (resetProfile.density a u) (1/8) := by
205   apply ContinuousLinearMap.ext
206   intro z
207   apply coordinate_ext
208   intro i
209   change coordinate i
210     (PolynomialGram.operatorPolynomial (fun k => matrixOperator (nominalComparison a k)) u z)=_
211   simp only [InteriorRepair.repair,add_apply,smul_apply,map_add,map_smul,
212     Section88ComparisonBudget.rawEstimate,InteriorRepair.EstimateFamily.ofPolynomial,
213     PolynomialGram.operatorPolynomial,sum_apply,smul_apply,map_sum,map_smul]
214   simp only [coordinate_matrixOperator]
215   cases a <;> fin_cases i <;>
216     norm_num [InteriorRepair.resetOperator,resetProfile,
217       InteriorRepair.centerReset_apply,Fin.sum_univ_succ,coordinate,Matrix.cons_val_two] <;> ring
218 
219 /-- The exact comparison discrepancy keeps both the raw error and the reset charge. -/
220 theorem comparison_integrated_error (a : Bool) (z : State ℂ) (hz : z∈probabilityCone.base) :
221     (∫ u,probabilityCone.value (comparisonInstrument.op a u z-Section88Reference.instrument.op a u z)∂measure)≤
222       81687/320000 := by
223   have h := InteriorRepair.repair_integrated_error Section88Reference.instrument
224     Section88ComparisonBudget.rawEstimate resetProfile (1/8) (by norm_num) (by norm_num)
225       (241/40000) a z hz (Section88ComparisonBudget.integrated_raw_error a z hz)
226   simp only [← comparison_is_repair] at h
227   norm_num at h ⊢
228   exact h
229 
230 /-- Full P79 finite-horizon law bound for the nominal repaired model and unchanged reference. -/
231 theorem comparison_law_bound (policy : ContinuousRecords.Policy (A := Bool) (Y := ℝ))
232     (z : DensityInstrument.State (probabilityCone (V := ℂ))) (N : ℕ) :
233     SequentialLowerCertificate.lawTV
234       (TimeRecords.recordLaw (fun _ => comparisonInstrument) policy z.1 N)
235       (TimeRecords.recordLaw (fun _ => Section88Reference.instrument) policy z.1 N)≤
236         min 1 (81687*(N : ℝ)/640000) := by
237   have h := InteriorRepair.common_policy_law_error Section88Reference.instrument comparisonInstrument
238     Section88ComparisonBudget.rawEstimate resetProfile (1/8) (by norm_num) (by norm_num)
239       (241/40000) comparison_is_repair Section88ComparisonBudget.integrated_raw_error policy z N
240   convert h using 1
241   congr 1
242   ring
243 
244 end
245 end Komorebi.LSM.Section88CertifiedRepair

Back to source controls