IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore
IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean · 690 lines · 28 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cost
3import IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge
4
5/-!
6# Seven Gaps: hinge stationarity core (the sourced stationary ratio)
7
8## Status: THEOREM for every proved statement below (0 sorry, 0 RS-internal
9axiom, no `native_decide`). The import set is exactly: Mathlib,
10`IndisputableMonolith.Cost`, and
11`IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge` (which
12transitively brings `Gravity.RecognitionLedger` and the bridge's own
13hinge-data definitions such as `quadraticCurvatureEnergy`); no
14Regge/mesh/simplicial geometry module is imported. MODEL for the sourced
15coupling term itself, as flagged below.
16
17This module records, kernel-checked, exactly how much of the paper's bridge
18relation "log x_sigma = kappa_sigma * delta_sigma + O(h^3)" is derivable
19from J-cost stationarity, and exactly where a constitutive MODEL input
20enters. The panel-adjudicated verdict:
21
22* **Kill record C6 (raw Stokes route).**
23 `closedCycle_coboundary_sum_eq_zero` proves that exact/coboundary
24 substrate strains telescope to ZERO around every closed cycle of cells.
25 A nonzero hinge deficit can never be sourced by summing coboundary
26 strains around a closed hinge link. This is the kernel-checked
27 obstruction that killed the raw Stokes route.
28
29* **Kill record raw 1b (budget circularity).**
30 `budget_implies_ratio_without_stationarity` proves that the naive
31 formulation (impose the holonomy budget sum t_i = kappa*delta, minimize,
32 conclude the ratio) is CIRCULAR: the budget hypothesis already IS the
33 conclusion, and stationarity contributes nothing. The proof term is the
34 budget hypothesis itself, which is the whole point.
35
36* **The honest mechanism (sourced stationary ratio).** Minimizing
37 Phi(t) = sum_i (cosh t_i - 1) - (kappa*delta/n) * sum_i t_i
38 (J-cost plus an explicit deficit-source coupling; the cost term IS the
39 summed J-cost of the exponential strain ratios by the kernel equation
40 `sourcedAction_eq_jcost_sum`) has the unique global
41 minimizer t_i = arsinh(kappa*delta/n) (`sourced_unique_minimizer`),
42 giving n * arsinh(kappa*delta/n) = kappa*delta + O((kappa*delta)^3) with
43 the explicit constant 1/6 (`sourced_ratio_cubic_error`). The constrained
44 variant (equal split under a fixed budget) is
45 `constrained_equal_split` / `constrained_equal_split_eq_iff`.
46
47* **The admissibility target is a uniform small-h FAMILY predicate**
48 (`RecognitionRatioFamily.IsAdmissible`): constants are quantified
49 OUTSIDE the mesh scale, per the panel; a fixed-h existential-constant
50 form is vacuous and is not stated here. The sourced construction closes
51 it end-to-end (`sourced_ratio_isAdmissible`) with the explicit constant
52 C_R = |kappa|^3 * C_K^3 * h0^3 / (6 n^2). Two disclosures, spelled out
53 in that theorem's docstring: the curvature conjunct of the conclusion is
54 a passthrough of the curvature hypothesis, and no 0 < h0 hypothesis is
55 taken because for h0 <= 0 the predicate is vacuously true, so the
56 theorem carries content exactly when 0 < h0.
57
58## Honest tiers
59
60* **THEOREM**: every named statement in this file (items 1 through 8 of
61 the lane spec): `closedCycle_coboundary_sum_eq_zero`,
62 `budget_implies_ratio_without_stationarity`,
63 `sourced_unique_minimizer` (with `sourced_minimizer_le`,
64 `sourced_minimizer_unique`), `sourced_ratio_cubic_error`,
65 `constrained_equal_split`, `constrained_equal_split_eq_iff`,
66 `sourced_ratio_isAdmissible`, `J_exp_quadratic_band`, `valueFn_deriv`
67 (with `sourced_costTerm_hasDerivAt`), together with the supporting
68 lemmas (`cosh_tangent_line_le`/`lt`, `sourced_pointwise_le`/`lt`,
69 `arsinh_le_self_of_nonneg`, `self_sub_cube_le_arsinh`,
70 `abs_arsinh_sub_self_le`, `sourcedAction_eq_sum`,
71 `sourcedAction_eq_jcost_sum`, `sourcedValue_eq_action_min`).
72* **MODEL**: the sourced coupling term -(kappa*delta/n) * sum_i t_i inside
73 `sourcedAction` is an explicit deficit-source constitutive choice. It is
74 NOT derived from the bare RecognitionLedger, and no such derivation is
75 claimed anywhere in this file.
76
77Any promotion language must read: derived from an explicit deficit-source
78constitutive action plus J-stationarity, never: derived from the bare
79RecognitionLedger. The J-cost identification inside that phrase is itself
80a kernel equation (`sourcedAction_eq_jcost_sum`), not a docstring gloss.
81
82## Constants achieved (spec deviations, recorded honestly)
83
84* Item 4: the target constant 1/6 IS achieved:
85 |arsinh y - y| <= |y|^3 / 6 (`abs_arsinh_sub_self_le`), hence
86 |n * arsinh(c/n) - c| <= |c|^3 / (6 n^2).
87* Item 7: the spec's optional constant cosh(r)/24 was not pursued; the
88 achieved two-sided band constant is cosh(r)/4 on |u| <= r
89 (`J_exp_quadratic_band`), via `cosh_remainder_le`. The spec marks the
90 exact constant as not load-bearing.
91* Item 8: the spec's suggested derivative value
92 kappa * sinh(arsinh(kappa*delta/n)) for the optimal-cost term is not the
93 chain-rule value; the correct derivative is
94 kappa * tanh(arsinh(kappa*delta/n)) = kappa*(kappa*delta/n)/sqrt(1+...)
95 (`sourced_costTerm_hasDerivAt`). The clean envelope identity that does
96 come out is for the full optimal VALUE V(delta) = Phi(t*):
97 V'(delta) = -kappa * arsinh(kappa*delta/n) (`valueFn_deriv`), which is
98 exactly the envelope-theorem partial of the coupling term at the
99 minimizer. Recorded as the panel requested; it never promotes alone.
100-/
101
102namespace IndisputableMonolith
103namespace Gravity
104namespace SevenGaps
105
106/-! ## §1. Kill record C6: the closed-cycle coboundary obstruction -/
107
108/-- **THEOREM (kill record C6, the raw Stokes route).** For a coboundary
109strain s i j = f i - f j and any cyclic chain of cells v 0, v 1, ..., v m
110with v m = v 0, the sum of strains around the cycle telescopes to zero.
111Exact/coboundary substrate strains can NEVER sum to a nonzero deficit
112around a closed hinge link: the raw Stokes route to the bridge relation is
113dead, kernel-checked. -/
114theorem closedCycle_coboundary_sum_eq_zero {Λ : Type*} {s : Λ → Λ → ℝ}
115 (hs : IsCoboundary s) (v : ℕ → Λ) (m : ℕ) (hcycle : v m = v 0) :
116 ∑ k ∈ Finset.range m, s (v k) (v (k + 1)) = 0 := by
117 obtain ⟨f, hf⟩ := hs
118 calc ∑ k ∈ Finset.range m, s (v k) (v (k + 1))
119 = ∑ k ∈ Finset.range m,
120 ((fun j => f (v j)) k - (fun j => f (v j)) (k + 1)) :=
121 Finset.sum_congr rfl fun k _ => hf (v k) (v (k + 1))
122 _ = f (v 0) - f (v m) := Finset.sum_range_sub' (fun j => f (v j)) m
123 _ = 0 := by rw [hcycle]; ring
124
125/-! ## §2. Kill record raw 1b: the budget circularity -/
126
127/-- The naive "log ratio" of the raw 1b formulation: nothing but the sum
128of the per-tick strains. -/
129def naiveLogRatio (n : ℕ) (t : Fin n → ℝ) : ℝ := ∑ i, t i
130
131/-- **THEOREM (kill record raw 1b, the budget circularity).** If the
132holonomy budget sum_i t_i = kappa*delta is IMPOSED, then the "conclusion"
133log ratio = kappa*delta holds with NO optimization used: the proof term is
134the budget hypothesis itself. This records, kernel-checked, that the naive
1351b formulation (impose budget, minimize, conclude ratio) is CIRCULAR: the
136budget already contains the conclusion; stationarity added nothing. -/
137theorem budget_implies_ratio_without_stationarity {n : ℕ} (t : Fin n → ℝ)
138 (kappa delta : ℝ) (hbudget : ∑ i, t i = kappa * delta) :
139 naiveLogRatio n t = kappa * delta := hbudget
140
141/-! ## §3. The tangent-line core of cosh (strict convexity, elementary)
142
143cosh t >= cosh u + sinh u * (t - u), strict for t ≠ u. Proved from the
144exponential tangent bound exp z >= 1 + z (strict for z ≠ 0); no integrals,
145no convexity library. -/
146
147/-- **THEOREM (cosh tangent-line bound).** For all u, t:
148cosh u + sinh u * (t - u) <= cosh t. -/
149theorem cosh_tangent_line_le (u t : ℝ) :
150 Real.cosh u + Real.sinh u * (t - u) ≤ Real.cosh t := by
151 have h1 : Real.exp u * (1 + (t - u)) ≤ Real.exp t := by
152 calc Real.exp u * (1 + (t - u)) = Real.exp u * (t - u + 1) := by ring
153 _ ≤ Real.exp u * Real.exp (t - u) :=
154 mul_le_mul_of_nonneg_left (Real.add_one_le_exp (t - u))
155 (Real.exp_pos u).le
156 _ = Real.exp t := by rw [← Real.exp_add]; congr 1; ring
157 have h2 : Real.exp (-u) * (1 - (t - u)) ≤ Real.exp (-t) := by
158 calc Real.exp (-u) * (1 - (t - u)) = Real.exp (-u) * (u - t + 1) := by
159 ring
160 _ ≤ Real.exp (-u) * Real.exp (u - t) :=
161 mul_le_mul_of_nonneg_left (Real.add_one_le_exp (u - t))
162 (Real.exp_pos (-u)).le
163 _ = Real.exp (-t) := by rw [← Real.exp_add]; congr 1; ring
164 rw [Real.cosh_eq, Real.sinh_eq, Real.cosh_eq]
165 nlinarith [h1, h2]
166
167/-- **THEOREM (strict cosh tangent-line bound).** For t ≠ u:
168cosh u + sinh u * (t - u) < cosh t. This is the strict-convexity kernel
169behind uniqueness of every minimizer in this file. -/
170theorem cosh_tangent_line_lt (u t : ℝ) (hne : t ≠ u) :
171 Real.cosh u + Real.sinh u * (t - u) < Real.cosh t := by
172 have h1 : Real.exp u * (1 + (t - u)) < Real.exp t := by
173 calc Real.exp u * (1 + (t - u)) = Real.exp u * (t - u + 1) := by ring
174 _ < Real.exp u * Real.exp (t - u) :=
175 mul_lt_mul_of_pos_left
176 (Real.add_one_lt_exp (sub_ne_zero.mpr hne)) (Real.exp_pos u)
177 _ = Real.exp t := by rw [← Real.exp_add]; congr 1; ring
178 have h2 : Real.exp (-u) * (1 - (t - u)) ≤ Real.exp (-t) := by
179 calc Real.exp (-u) * (1 - (t - u)) = Real.exp (-u) * (u - t + 1) := by
180 ring
181 _ ≤ Real.exp (-u) * Real.exp (u - t) :=
182 mul_le_mul_of_nonneg_left (Real.add_one_le_exp (u - t))
183 (Real.exp_pos (-u)).le
184 _ = Real.exp (-t) := by rw [← Real.exp_add]; congr 1; ring
185 rw [Real.cosh_eq, Real.sinh_eq, Real.cosh_eq]
186 nlinarith [h1, h2]
187
188/-- **THEOREM (one-variable sourced minimum).** For every source strength
189a, the map t ↦ cosh t - 1 - a*t attains its global minimum at
190t = arsinh a (where sinh t = a). -/
191theorem sourced_pointwise_le (a t : ℝ) :
192 Real.cosh (Real.arsinh a) - 1 - a * Real.arsinh a
193 ≤ Real.cosh t - 1 - a * t := by
194 have h := cosh_tangent_line_le (Real.arsinh a) t
195 rw [Real.sinh_arsinh] at h
196 nlinarith [h]
197
198/-- **THEOREM (one-variable sourced minimum, strict).** The minimum of
199t ↦ cosh t - 1 - a*t is attained ONLY at t = arsinh a. -/
200theorem sourced_pointwise_lt (a t : ℝ) (hne : t ≠ Real.arsinh a) :
201 Real.cosh (Real.arsinh a) - 1 - a * Real.arsinh a
202 < Real.cosh t - 1 - a * t := by
203 have h := cosh_tangent_line_lt (Real.arsinh a) t hne
204 rw [Real.sinh_arsinh] at h
205 nlinarith [h]
206
207/-! ## §4. The sourced stationary ratio (item 3)
208
209MODEL input flag: the coupling term -(c/n) * sum_i t_i below is an
210explicit deficit-source constitutive choice, not derived from the bare
211RecognitionLedger. Everything proved ABOUT `sourcedAction` is THEOREM. -/
212
213/-- The sourced action Phi(t) = sum_i (cosh t_i - 1) - (c/n) * sum_i t_i:
214the J-cost of the per-tick strains (via J(exp t) = cosh t - 1,
215`Cost.Jcost_exp_cosh`) plus an explicit deficit-source coupling of total
216strength c = kappa*delta, split evenly across the n ticks. The coupling
217term is the MODEL input; see the module header. -/
218noncomputable def sourcedAction (n : ℕ) (c : ℝ) (t : Fin n → ℝ) : ℝ :=
219 (∑ i, (Real.cosh (t i) - 1)) - c / n * ∑ i, t i
220
221/-- The claimed unique minimizer of the sourced action: the uniform
222configuration t_i = arsinh(c/n). -/
223noncomputable def sourcedMinimizer (n : ℕ) (c : ℝ) : Fin n → ℝ :=
224 fun _ => Real.arsinh (c / n)
225
226/-- **THEOREM.** The sourced action decomposes into independent per-tick
227terms cosh t_i - 1 - (c/n) * t_i. -/
228theorem sourcedAction_eq_sum (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
229 sourcedAction n c t
230 = ∑ i, (Real.cosh (t i) - 1 - c / n * t i) := by
231 unfold sourcedAction
232 rw [Finset.mul_sum, ← Finset.sum_sub_distrib]
233
234/-- **THEOREM (kernel J-cost identification).** The cost term of the
235sourced action IS the summed J-cost of the exponential per-tick strain
236ratios: Phi(t) = sum_i J(exp t_i) - (c/n) * sum_i t_i, via
237`Cost.Jcost_exp_cosh` (J(exp t) = cosh t - 1). This puts the promotion
238phrase "derived from an explicit deficit-source constitutive action plus
239J-stationarity" on a kernel equation rather than a docstring gloss: the
240J-cost part of the action is identified with `Cost.Jcost` inside the
241kernel, and ONLY the coupling term remains MODEL. -/
242theorem sourcedAction_eq_jcost_sum (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
243 sourcedAction n c t
244 = (∑ i, Cost.Jcost (Real.exp (t i))) - c / n * ∑ i, t i := by
245 unfold sourcedAction
246 simp only [Cost.Jcost_exp_cosh]
247
248/-- **THEOREM (global minimality).** The uniform configuration
249t_i = arsinh(c/n) minimizes the sourced action over ALL configurations. -/
250theorem sourced_minimizer_le (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
251 sourcedAction n c (sourcedMinimizer n c) ≤ sourcedAction n c t := by
252 rw [sourcedAction_eq_sum, sourcedAction_eq_sum]
253 refine Finset.sum_le_sum fun i _ => ?_
254 simp only [sourcedMinimizer]
255 exact sourced_pointwise_le (c / n) (t i)
256
257/-- **THEOREM (uniqueness).** Any configuration achieving the minimum of
258the sourced action IS the uniform configuration t_i = arsinh(c/n). -/
259theorem sourced_minimizer_unique (n : ℕ) (c : ℝ) (t : Fin n → ℝ)
260 (heq : sourcedAction n c t = sourcedAction n c (sourcedMinimizer n c)) :
261 t = sourcedMinimizer n c := by
262 by_contra hne
263 obtain ⟨i₀, hi₀⟩ := Function.ne_iff.mp hne
264 have hlt : sourcedAction n c (sourcedMinimizer n c)
265 < sourcedAction n c t := by
266 rw [sourcedAction_eq_sum, sourcedAction_eq_sum]
267 simp only [sourcedMinimizer]
268 refine Finset.sum_lt_sum (fun i _ => sourced_pointwise_le (c / n) (t i))
269 ⟨i₀, Finset.mem_univ i₀, ?_⟩
270 exact sourced_pointwise_lt (c / n) (t i₀) hi₀
271 linarith [heq, hlt]
272
273/-- **THEOREM (item 3, sourced unique minimizer).** For every n (no
274n >= 1 hypothesis is needed; at n = 0 both conjuncts are trivially true
275on the empty tick set) and every total source strength c, the sourced
276action
277Phi(t) = sum_i (cosh t_i - 1) - (c/n) * sum_i t_i over t : Fin n → ℝ has
278the unique global minimizer t_i = arsinh(c/n) for all i. The stationarity
279condition sinh t_i = c/n is genuinely FORCED here (contrast with the
280circular raw 1b route, `budget_implies_ratio_without_stationarity`), but
281only because the deficit-source coupling was supplied as a MODEL input. -/
282theorem sourced_unique_minimizer (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
283 sourcedAction n c (sourcedMinimizer n c) ≤ sourcedAction n c t ∧
284 (sourcedAction n c t = sourcedAction n c (sourcedMinimizer n c) →
285 t = sourcedMinimizer n c) :=
286 ⟨sourced_minimizer_le n c t, sourced_minimizer_unique n c t⟩
287
288/-! ## §5. The cubic error of the sourced ratio (item 4) -/
289
290/-- **THEOREM.** arsinh y <= y for y >= 0 (since y <= sinh y and arsinh is
291monotone). -/
292theorem arsinh_le_self_of_nonneg {y : ℝ} (hy : 0 ≤ y) :
293 Real.arsinh y ≤ y := by
294 calc Real.arsinh y ≤ Real.arsinh (Real.sinh y) :=
295 Real.arsinh_le_arsinh.mpr (Real.self_le_sinh_iff.mpr hy)
296 _ = y := Real.arsinh_sinh y
297
298/-- **THEOREM (cubic lower bound).** y - y^3/6 <= arsinh y for y >= 0.
299Proved by showing x ↦ arsinh x - x + x^3/6 is monotone (its derivative
3001/sqrt(1+x^2) - 1 + x^2/2 is nonnegative everywhere) and vanishes at 0. -/
301theorem self_sub_cube_le_arsinh {y : ℝ} (hy : 0 ≤ y) :
302 y - y ^ 3 / 6 ≤ Real.arsinh y := by
303 have hderiv : ∀ x : ℝ,
304 HasDerivAt (fun z => Real.arsinh z - z + z ^ 3 / 6)
305 ((Real.sqrt (1 + x ^ 2))⁻¹ - 1 + (3 : ℕ) * x ^ 2 / 6) x := by
306 intro x
307 have h1 := Real.hasDerivAt_arsinh x
308 have h2 : HasDerivAt (fun z : ℝ => z) 1 x := hasDerivAt_id x
309 have h3 : HasDerivAt (fun z : ℝ => z ^ 3 / 6)
310 ((3 : ℕ) * x ^ 2 / 6) x := by
311 have h := (hasDerivAt_pow 3 x).div_const 6
312 norm_num at h ⊢
313 exact h
314 exact (h1.sub h2).add h3
315 have hmono : Monotone (fun z : ℝ => Real.arsinh z - z + z ^ 3 / 6) := by
316 refine monotone_of_deriv_nonneg (fun x => (hderiv x).differentiableAt)
317 fun x => ?_
318 rw [(hderiv x).deriv]
319 have hs_pos : 0 < Real.sqrt (1 + x ^ 2) :=
320 Real.sqrt_pos.mpr (by positivity)
321 have hs_sq : Real.sqrt (1 + x ^ 2) ^ 2 = 1 + x ^ 2 :=
322 Real.sq_sqrt (by positivity)
323 have hs_inv : Real.sqrt (1 + x ^ 2) * (Real.sqrt (1 + x ^ 2))⁻¹ = 1 :=
324 mul_inv_cancel₀ hs_pos.ne'
325 rcases le_or_gt (1 - x ^ 2 / 2) 0 with hcase | hcase
326 · have hpos : 0 < (Real.sqrt (1 + x ^ 2))⁻¹ := inv_pos.mpr hs_pos
327 push_cast
328 nlinarith [hpos, hcase]
329 · have hx2 : x ^ 2 < 2 := by nlinarith [hcase]
330 have hP : Real.sqrt (1 + x ^ 2) * (1 - x ^ 2 / 2) ≤ 1 := by
331 nlinarith [hs_sq, hs_pos.le, sq_nonneg x, sq_nonneg (x ^ 2),
332 sq_nonneg (Real.sqrt (1 + x ^ 2) * (1 - x ^ 2 / 2) - 1)]
333 push_cast
334 nlinarith [hP, hs_inv, hs_pos]
335 have h0 : (fun z : ℝ => Real.arsinh z - z + z ^ 3 / 6) 0 = 0 := by
336 simp only [Real.arsinh_zero]
337 norm_num
338 have hle := hmono hy
339 rw [h0] at hle
340 simp only at hle
341 linarith [hle]
342
343/-- **THEOREM (cubic error of arsinh, constant 1/6).**
344|arsinh y - y| <= |y|^3 / 6 for ALL y (nonnegative branch from the two
345bounds above, negative branch by oddness of arsinh). -/
346theorem abs_arsinh_sub_self_le (y : ℝ) :
347 |Real.arsinh y - y| ≤ |y| ^ 3 / 6 := by
348 rcases le_or_gt 0 y with hy | hy
349 · have h1 := arsinh_le_self_of_nonneg hy
350 have h2 := self_sub_cube_le_arsinh hy
351 rw [abs_of_nonneg hy,
352 abs_of_nonpos (by linarith : Real.arsinh y - y ≤ 0)]
353 linarith
354 · have hy' : 0 ≤ -y := by linarith
355 have h1 := arsinh_le_self_of_nonneg hy'
356 have h2 := self_sub_cube_le_arsinh hy'
357 rw [Real.arsinh_neg] at h1 h2
358 have hcube : (-y) ^ 3 = -(y ^ 3) := by ring
359 rw [hcube] at h2
360 rw [abs_of_neg hy,
361 abs_of_nonneg (by linarith : 0 ≤ Real.arsinh y - y)]
362 have hgoal : (-y) ^ 3 = -(y ^ 3) := by ring
363 rw [hgoal]
364 linarith
365
366/-- **THEOREM (item 4, cubic error of the sourced ratio, constant 1/6).**
367|n * arsinh(c/n) - c| <= |c|^3 / (6 n^2) for n >= 1. This is the honest
368form of the bridge expansion: the sourced stationary log ratio
369n * arsinh(c/n) equals the deficit source c = kappa*delta up to an
370explicitly bounded cubic error. -/
371theorem sourced_ratio_cubic_error (n : ℕ) (hn : 1 ≤ n) (c : ℝ) :
372 |(n : ℝ) * Real.arsinh (c / n) - c|
373 ≤ |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by
374 have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
375 have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
376 have hkey : (n : ℝ) * Real.arsinh (c / n) - c
377 = (n : ℝ) * (Real.arsinh (c / n) - c / n) := by
378 field_simp
379 rw [hkey, abs_mul, abs_of_pos hn0]
380 have hcn : |c / (n : ℝ)| ^ 3 = |c| ^ 3 / (n : ℝ) ^ 3 := by
381 rw [abs_div, abs_of_pos hn0, div_pow]
382 calc (n : ℝ) * |Real.arsinh (c / n) - c / n|
383 ≤ (n : ℝ) * (|c / (n : ℝ)| ^ 3 / 6) :=
384 mul_le_mul_of_nonneg_left (abs_arsinh_sub_self_le (c / n)) hn0.le
385 _ = |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by
386 rw [hcn]
387 field_simp
388
389/-! ## §6. The constrained equal split (item 5) -/
390
391/-- **THEOREM (item 5, constrained equal split, lower bound).** Over the
392constraint set {t | sum_i t_i = c}, the J-cost sum_i (cosh t_i - 1) is at
393least n * (cosh(c/n) - 1): the equal split is optimal. Proved by summing
394the tangent-line bound of cosh at c/n; the linear terms cancel against the
395budget. NOTE the honest reading: this theorem extracts the equal-split
396VALUE from the budget; it does not, and cannot, produce the budget itself
397(see `budget_implies_ratio_without_stationarity`). -/
398theorem constrained_equal_split (n : ℕ) (hn : 1 ≤ n) (c : ℝ)
399 (t : Fin n → ℝ) (hbudget : ∑ i, t i = c) :
400 (n : ℝ) * (Real.cosh (c / n) - 1) ≤ ∑ i, (Real.cosh (t i) - 1) := by
401 have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
402 have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
403 have hL : ∑ _i : Fin n,
404 (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
405 = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n)) := by
406 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
407 have hsum : ∑ i : Fin n,
408 (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
409 ≤ ∑ i : Fin n, Real.cosh (t i) :=
410 Finset.sum_le_sum fun i _ => cosh_tangent_line_le (c / n) (t i)
411 have hsplit : ∑ i : Fin n,
412 (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
413 = (n : ℝ) * Real.cosh (c / n) := by
414 calc ∑ i : Fin n,
415 (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
416 = ∑ i : Fin n,
417 ((Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
418 + Real.sinh (c / n) * t i) :=
419 Finset.sum_congr rfl fun i _ => by ring
420 _ = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
421 + Real.sinh (c / n) * c := by
422 rw [Finset.sum_add_distrib, hL, ← Finset.mul_sum, hbudget]
423 _ = (n : ℝ) * Real.cosh (c / n) := by
424 field_simp
425 ring
426 have hR : ∑ i : Fin n, (Real.cosh (t i) - 1)
427 = (∑ i : Fin n, Real.cosh (t i)) - (n : ℝ) := by
428 rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
429 Fintype.card_fin, nsmul_eq_mul, mul_one]
430 rw [hR]
431 rw [hsplit] at hsum
432 nlinarith [hsum]
433
434/-- **THEOREM (item 5, equality characterization).** Under the budget
435constraint, the constrained minimum n * (cosh(c/n) - 1) is attained IFF
436the configuration is exactly the equal split t_i = c/n. -/
437theorem constrained_equal_split_eq_iff (n : ℕ) (hn : 1 ≤ n) (c : ℝ)
438 (t : Fin n → ℝ) (hbudget : ∑ i, t i = c) :
439 (∑ i, (Real.cosh (t i) - 1) = (n : ℝ) * (Real.cosh (c / n) - 1)) ↔
440 t = fun _ => c / n := by
441 have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
442 have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
443 constructor
444 · intro heq
445 by_contra hnef
446 obtain ⟨i₀, hi₀⟩ := Function.ne_iff.mp hnef
447 have hlt : ∑ i : Fin n,
448 (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
449 < ∑ i : Fin n, Real.cosh (t i) :=
450 Finset.sum_lt_sum (fun i _ => cosh_tangent_line_le (c / n) (t i))
451 ⟨i₀, Finset.mem_univ i₀,
452 cosh_tangent_line_lt (c / n) (t i₀) hi₀⟩
453 have hL : ∑ _i : Fin n,
454 (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
455 = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n)) := by
456 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin,
457 nsmul_eq_mul]
458 have hsplit : ∑ i : Fin n,
459 (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
460 = (n : ℝ) * Real.cosh (c / n) := by
461 calc ∑ i : Fin n,
462 (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
463 = ∑ i : Fin n,
464 ((Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
465 + Real.sinh (c / n) * t i) :=
466 Finset.sum_congr rfl fun i _ => by ring
467 _ = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
468 + Real.sinh (c / n) * c := by
469 rw [Finset.sum_add_distrib, hL, ← Finset.mul_sum, hbudget]
470 _ = (n : ℝ) * Real.cosh (c / n) := by
471 field_simp
472 ring
473 have hR : ∑ i : Fin n, (Real.cosh (t i) - 1)
474 = (∑ i : Fin n, Real.cosh (t i)) - (n : ℝ) := by
475 rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
476 Fintype.card_fin, nsmul_eq_mul, mul_one]
477 rw [hsplit] at hlt
478 rw [hR] at heq
479 nlinarith [hlt, heq]
480 · intro ht
481 subst ht
482 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
483
484/-! ## §7. The uniform small-h admissible family (item 6)
485
486Per the panel: the admissibility target is a FAMILY predicate with the
487constants quantified OUTSIDE the mesh scale h. A fixed-h
488existential-constant form is vacuous (any single h admits fitted
489constants) and is deliberately NOT stated in this file. -/
490
491/-- A family of hinge ratio data indexed by mesh scale h: the recognition
492ratio x(h) and the hinge deficit delta(h). -/
493structure RecognitionRatioFamily where
494 /-- The recognition ratio x(h) at mesh scale h. -/
495 ratio : ℝ → ℝ
496 /-- The hinge deficit delta(h) at mesh scale h. -/
497 deficit : ℝ → ℝ
498
499/-- **The uniform small-h admissibility predicate (item 6).** A family is
500admissible for (h0, kappa, C_K, C_R) iff UNIFORMLY over all mesh scales
501h in (0, h0): the deficit obeys the curvature bound |delta(h)| <= C_K h^2
502AND the bridge relation holds with cubic error
503|log x(h) - kappa * delta(h)| <= C_R h^3. The constants are quantified
504outside the family, per the panel; this is what makes the predicate
505non-vacuous. -/
506def RecognitionRatioFamily.IsAdmissible (F : RecognitionRatioFamily)
507 (h₀ kappa C_K C_R : ℝ) : Prop :=
508 ∀ h ∈ Set.Ioo (0 : ℝ) h₀,
509 |F.deficit h| ≤ C_K * h ^ 2 ∧
510 |Real.log (F.ratio h) - kappa * F.deficit h| ≤ C_R * h ^ 3
511
512/-- The sourced-stationary ratio family: at each mesh scale h, the ratio
513is x(h) = exp(n * arsinh(kappa * delta(h) / n)), i.e. the exponential of
514the optimal total strain of the sourced action with source
515c = kappa * delta(h) (`sourced_unique_minimizer`). -/
516noncomputable def sourcedRatioFamily (n : ℕ) (kappa : ℝ) (δ : ℝ → ℝ) :
517 RecognitionRatioFamily where
518 ratio := fun h => Real.exp ((n : ℝ) * Real.arsinh (kappa * δ h / n))
519 deficit := δ
520
521/-- **THEOREM (item 6, end-to-end admissibility of the sourced ratio).**
522Under the curvature bound |delta(h)| <= C_K h^2 on (0, h0), the
523sourced-stationary construction yields an admissible family with the
524EXPLICIT uniform constant C_R = |kappa|^3 * C_K^3 * h0^3 / (6 n^2),
525computed from the cubic error bound `sourced_ratio_cubic_error`:
526|log x(h) - kappa*delta(h)| = |n*arsinh(kappa*delta(h)/n) - kappa*delta(h)|
527<= |kappa*delta(h)|^3/(6n^2) <= (|kappa| C_K h^2)^3/(6n^2)
528<= (|kappa|^3 C_K^3 h0^3/(6n^2)) * h^3 for h in (0, h0).
529
530Two honest disclosures. (a) The curvature conjunct |delta(h)| <= C_K h^2
531of the conclusion is a PASSTHROUGH of the hypothesis `hδ`, restated inside
532the predicate only so the admissibility record is self-contained; the new
533content of this theorem is entirely the bridge conjunct. (b) There is no
5340 < h0 hypothesis: for h0 <= 0 the interval (0, h0) is empty and the
535predicate is vacuously true, so adding positivity would not strengthen
536the conclusion; the statement carries content exactly when 0 < h0. -/
537theorem sourced_ratio_isAdmissible (n : ℕ) (hn : 1 ≤ n)
538 (h₀ kappa C_K : ℝ) (δ : ℝ → ℝ)
539 (hδ : ∀ h ∈ Set.Ioo (0 : ℝ) h₀, |δ h| ≤ C_K * h ^ 2) :
540 (sourcedRatioFamily n kappa δ).IsAdmissible h₀ kappa C_K
541 (|kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 / (6 * (n : ℝ) ^ 2)) := by
542 intro h hh
543 obtain ⟨hh1, hh2⟩ := hh
544 have hδh := hδ h ⟨hh1, hh2⟩
545 refine ⟨hδh, ?_⟩
546 have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
547 have hCK : 0 ≤ C_K := by
548 have hsq : (0 : ℝ) < h ^ 2 := by positivity
549 nlinarith [abs_nonneg (δ h), hδh, hsq]
550 have hh3 : h ^ 3 ≤ h₀ ^ 3 := pow_le_pow_left₀ hh1.le hh2.le 3
551 show |Real.log (Real.exp ((n : ℝ) * Real.arsinh (kappa * δ h / n)))
552 - kappa * δ h| ≤ _
553 rw [Real.log_exp]
554 have hnum : |kappa * δ h| ^ 3
555 ≤ |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3 := by
556 have h1 : |kappa * δ h| ^ 3 = |kappa| ^ 3 * |δ h| ^ 3 := by
557 rw [abs_mul, mul_pow]
558 have h2 : |δ h| ^ 3 ≤ (C_K * h ^ 2) ^ 3 :=
559 pow_le_pow_left₀ (abs_nonneg _) hδh 3
560 have h3 : (C_K * h ^ 2) ^ 3 = C_K ^ 3 * (h ^ 3 * h ^ 3) := by ring
561 have h4 : C_K ^ 3 * (h ^ 3 * h ^ 3) ≤ C_K ^ 3 * (h₀ ^ 3 * h ^ 3) := by
562 refine mul_le_mul_of_nonneg_left ?_ (by positivity)
563 exact mul_le_mul_of_nonneg_right hh3 (by positivity)
564 calc |kappa * δ h| ^ 3 = |kappa| ^ 3 * |δ h| ^ 3 := h1
565 _ ≤ |kappa| ^ 3 * (C_K ^ 3 * (h₀ ^ 3 * h ^ 3)) := by
566 refine mul_le_mul_of_nonneg_left ?_ (by positivity)
567 calc |δ h| ^ 3 ≤ (C_K * h ^ 2) ^ 3 := h2
568 _ = C_K ^ 3 * (h ^ 3 * h ^ 3) := h3
569 _ ≤ C_K ^ 3 * (h₀ ^ 3 * h ^ 3) := h4
570 _ = |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3 := by ring
571 calc |(n : ℝ) * Real.arsinh (kappa * δ h / n) - kappa * δ h|
572 ≤ |kappa * δ h| ^ 3 / (6 * (n : ℝ) ^ 2) :=
573 sourced_ratio_cubic_error n hn (kappa * δ h)
574 _ ≤ (|kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3) / (6 * (n : ℝ) ^ 2) := by
575 have hden : (0 : ℝ) ≤ (6 * (n : ℝ) ^ 2)⁻¹ := by positivity
576 rw [div_eq_mul_inv, div_eq_mul_inv]
577 exact mul_le_mul_of_nonneg_right hnum hden
578 _ = |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 / (6 * (n : ℝ) ^ 2) * h ^ 3 := by
579 ring
580
581/-! ## §8. The two-sided quadratic band (item 7) -/
582
583/-- **THEOREM (item 7, two-sided quadratic band, constant cosh(r)/4).**
584|J(exp u) - u^2/2| <= (cosh r / 4) * u^4 for |u| <= r. Generalizes the
585radius of `Jcost_exp_sub_half_sq_abs_le` (which is the case r = 1 with
586the numeric constant 1/2) via `cosh_remainder_le`. The spec's optional
587sharper constant cosh(r)/24 was not pursued; the constant is recorded and
588is not load-bearing. -/
589theorem J_exp_quadratic_band (r u : ℝ) (hu : |u| ≤ r) :
590 |Cost.Jcost (Real.exp u) - u ^ 2 / 2| ≤ Real.cosh r / 4 * u ^ 4 := by
591 rw [Cost.Jcost_exp_cosh]
592 have h0 := cosh_remainder_nonneg u
593 have h1 := cosh_remainder_le u
594 have hr0 : 0 ≤ r := le_trans (abs_nonneg u) hu
595 have hcosh : Real.cosh u ≤ Real.cosh r := by
596 rw [Real.cosh_le_cosh, abs_of_nonneg hr0]
597 exact hu
598 rw [abs_of_nonneg h0]
599 have h2 : u ^ 4 / 4 * Real.cosh u ≤ u ^ 4 / 4 * Real.cosh r :=
600 mul_le_mul_of_nonneg_left hcosh (by positivity)
601 nlinarith [h1, h2]
602
603/-! ## §9. The envelope corollary (item 8)
604
605The panel wants the derivative structure of the optimal value recorded;
606it never promotes alone. The spec's suggested derivative
607kappa * sinh(arsinh(kappa*delta/n)) for the cost term is not the
608chain-rule value; the correct values are proved below and the correction
609is recorded in the module header. -/
610
611/-- The optimal VALUE of the sourced problem as a function of the deficit:
612V(delta) = Phi(t*) = n*(cosh(arsinh(kappa*delta/n)) - 1)
613- kappa*delta*arsinh(kappa*delta/n). -/
614noncomputable def sourcedValue (n : ℕ) (kappa : ℝ) (d : ℝ) : ℝ :=
615 (n : ℝ) * (Real.cosh (Real.arsinh (kappa * d / n)) - 1)
616 - kappa * d * Real.arsinh (kappa * d / n)
617
618/-- **THEOREM.** The optimal value function IS the sourced action
619evaluated at its unique minimizer (with source c = kappa*d). -/
620theorem sourcedValue_eq_action_min (n : ℕ) (hn : 1 ≤ n) (kappa d : ℝ) :
621 sourcedValue n kappa d
622 = sourcedAction n (kappa * d) (sourcedMinimizer n (kappa * d)) := by
623 have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
624 have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
625 unfold sourcedValue sourcedAction sourcedMinimizer
626 rw [Finset.sum_const, Finset.sum_const, Finset.card_univ,
627 Fintype.card_fin, nsmul_eq_mul, nsmul_eq_mul]
628 field_simp
629
630/-- **THEOREM (chain-rule derivative of the optimal cost term).** The
631derivative of delta ↦ n*(cosh(arsinh(kappa*delta/n)) - 1) is
632kappa * tanh(arsinh(kappa*delta/n)) = kappa*(kappa*delta/n)/sqrt(1+(kappa*delta/n)^2).
633This CORRECTS the spec's suggested value kappa*sinh(arsinh(.)): the
634arsinh chain factor 1/sqrt(1+y^2) turns sinh into tanh. -/
635theorem sourced_costTerm_hasDerivAt (n : ℕ) (hn : 1 ≤ n) (kappa d : ℝ) :
636 HasDerivAt
637 (fun z => (n : ℝ) * (Real.cosh (Real.arsinh (kappa * z / n)) - 1))
638 (kappa * Real.tanh (Real.arsinh (kappa * d / n))) d := by
639 have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
640 have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
641 have hs_pos : 0 < Real.sqrt (1 + (kappa * d / n) ^ 2) :=
642 Real.sqrt_pos.mpr (by positivity)
643 have hinner : HasDerivAt (fun z : ℝ => kappa * z / (n : ℝ))
644 (kappa / n) d := by
645 have h := ((hasDerivAt_id d).const_mul kappa).div_const (n : ℝ)
646 simpa using h
647 have harsinh := hinner.arsinh
648 have hcosh := harsinh.cosh
649 have htotal := (hcosh.sub_const 1).const_mul (n : ℝ)
650 convert htotal using 1
651 rw [Real.tanh_arsinh, smul_eq_mul, Real.sinh_arsinh]
652 field_simp
653
654/-- **THEOREM (item 8, the envelope corollary).** The optimal value
655V(delta) of the sourced problem is differentiable in the deficit with
656V'(delta) = -kappa * arsinh(kappa*delta/n): exactly the envelope-theorem
657partial derivative of the MODEL coupling term
658-(kappa*delta/n) * sum_i t_i at the minimizer t_i = arsinh(kappa*delta/n)
659(the direct derivatives of the cost term cancel against the coupling
660term's dependence through t*). Recorded per the panel; it never promotes
661alone. -/
662theorem valueFn_deriv (n : ℕ) (hn : 1 ≤ n) (kappa d : ℝ) :
663 HasDerivAt (fun z => sourcedValue n kappa z)
664 (-(kappa * Real.arsinh (kappa * d / n))) d := by
665 have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
666 have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
667 have hs_pos : 0 < Real.sqrt (1 + (kappa * d / n) ^ 2) :=
668 Real.sqrt_pos.mpr (by positivity)
669 have hinner : HasDerivAt (fun z : ℝ => kappa * z / (n : ℝ))
670 (kappa / n) d := by
671 have h := ((hasDerivAt_id d).const_mul kappa).div_const (n : ℝ)
672 simpa using h
673 have harsinh := hinner.arsinh
674 have hcosh := harsinh.cosh
675 have hterm1 := (hcosh.sub_const 1).const_mul (n : ℝ)
676 have hlin : HasDerivAt (fun z : ℝ => kappa * z) kappa d := by
677 have h := (hasDerivAt_id d).const_mul kappa
678 simpa using h
679 have hterm2 := hlin.mul harsinh
680 have htotal := hterm1.sub hterm2
681 simp only [sourcedValue]
682 convert htotal using 1
683 rw [smul_eq_mul, Real.sinh_arsinh]
684 field_simp
685 ring
686
687end SevenGaps
688end Gravity
689end IndisputableMonolith
690