theorem
proved
tactic proof
eulerScalarProxy_defect_bounded
show as:
view Lean formalization →
formal statement (Lean)
197theorem eulerScalarProxy_defect_bounded (sensor : DefectSensor) :
198 ∃ K : ℝ, ∀ N : ℕ,
199 IndisputableMonolith.Foundation.LawOfExistence.defect
200 (eulerScalarProxy sensor N) ≤ K := by
proof body
Tactic-mode proof.
201 refine ⟨(eulerScalarGap sensor) ^ 2 / 2, ?_⟩
202 intro N
203 let t : ℝ := eulerScalarGap sensor / (N + 1 : ℝ)
204 have ht_nonneg : 0 ≤ t := by
205 unfold t
206 exact div_nonneg (le_of_lt (eulerScalarGap_pos sensor)) (by positivity)
207 rw [eulerScalarProxy, defect_one_div_one_add t ht_nonneg]
208 have hden :
209 (2 : ℝ) ≤ 2 * (1 + t) := by
210 nlinarith [ht_nonneg]
211 have hstep1 :
212 t ^ 2 / (2 * (1 + t)) ≤ t ^ 2 / 2 := by
213 exact div_le_div_of_nonneg_left (sq_nonneg t) (by positivity) hden
214 have ht_le_gap :
215 t ≤ eulerScalarGap sensor := by
216 unfold t
217 have hgap_nonneg : 0 ≤ eulerScalarGap sensor := le_of_lt (eulerScalarGap_pos sensor)
218 have hone_le_nat : (1 : ℕ) ≤ N + 1 := by
219 exact Nat.succ_le_succ (Nat.zero_le N)
220 have hone_le : (1 : ℝ) ≤ (N + 1 : ℝ) := by
221 exact_mod_cast hone_le_nat
222 exact div_le_self hgap_nonneg hone_le
223 have hsq :
224 t ^ 2 ≤ (eulerScalarGap sensor) ^ 2 := by
225 nlinarith [ht_nonneg, le_of_lt (eulerScalarGap_pos sensor), ht_le_gap]
226 have hstep2 :
227 t ^ 2 / 2 ≤ (eulerScalarGap sensor) ^ 2 / 2 := by
228 exact div_le_div_of_nonneg_right hsq (by positivity)
229 exact le_trans hstep1 hstep2
230
231/-- A physically realizable ledger attached to a sensor carries a scalar proxy
232state `x_N > 0` whose T1 defect stays uniformly bounded along the realized
233trajectory.
234
235This is the formal interface for the ontology route:
236
237* `admissible` records that the ledger really comes from an admissible Euler trace.
238* `scalarState N` is the scalar proxy state at refinement depth `N`.
239* `scalarDefectBounded` says the realized scalar path never enters the
240 infinite-cost regime of the T1 defect functional.
241
242The key theorem below proves that such a ledger can never approach the T1
243boundary `x = 0`, because `nothing_cannot_exist` would make the defect exceed
244the uniform bound. -/