IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumMagnitudeBridge
IndisputableMonolith/Gravity/SevenGaps/Gap5MomentumMagnitudeBridge.lean · 561 lines · 32 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity
2import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket
3
4/-!
5# Momentum-magnitude bridge: exact reduction, named residual, open discharge lead
6
7**Verdict, stated first.** The global kinetic condition `p z ^ 2 = imbalance z ^ 2`
8for all `z : LedgerState` is **not** derived from substrate structure, and this
9module does not close that gap. What is derived: on the open positive quadrant
10the kinetic condition is *exactly equivalent* to a single named physical premise,
11
12 `EnergyEqualsCost p` :=
13 `∀ k t, 0 < k → p (orbitPoint k t) ^ 2 = 2 * k * Cost.Jlog t`
14
15(the equivalence, not just the forward direction, is
16`open_positive_kinetic_iff_energy_equals_cost`), and the premise plus continuity
17yields the kinetic condition on the closed positive quadrant. The global
18statement remains strictly larger: the orbit route cannot see Q2–Q4, and
19`SwapOdd` maps the positive quadrant to itself, so it does not open them either.
20
21**The residual premise is independent of the rest of the momentum package**:
22`imbalance` satisfies it (`energy_equals_cost_of_imbalance`, the chart theorem
23rearranged), while `2 * imbalance` is continuous, swap-odd, additive, and
24balance-vanishing yet fails it (`two_imbalance_fails_energy_equals_cost`). So
25`EnergyEqualsCost` is consistent, and it is not implied by the B1 package.
26
27**The Hamiltonian discharge lead is open, not refuted.** The *named* candidates
28the library offers fail: `HamDyn` on `PhaseSpace 2` has a nonzero gradient
29sector at zero momenta (`hamDyn_gradient_sector_nonzero_at_zero_momenta`), and
30`Jlog` is not the quadratic form `t ↦ t ^ 2 / 2` (`Jlog_ne_half_sq`). Matching
31the HKT exact-cost quadratic `2 (lam * p) ^ 2` to orbit exactness is scalar
32algebra that recovers the chart product `lam * p`
33(`exact_cost_profile_recovers_chart_product`); it neither constructs nor
34discharges the ledger-level premise. No carrier map between these
35`PhaseSpace 2` objects and `LedgerState` observables is stated anywhere in the
36library, so these failures say nothing about an arbitrary Hamiltonian on an
37arbitrary carrier: a derivation of `EnergyEqualsCost` from the posting
38dynamics' action principle remains the open frontier.
39
40## What is derived
41
421. **L1 (orbit coverage).** Every state with `0 < z.1` and `0 < z.2` equals
43 `orbitPoint (casimir z) (Real.log (z.1 / z.2))`.
442. **The exact reduction.** `EnergyEqualsCost p ↔ KineticOnOpenPositiveQuadrant p`.
453. **L3 (boundary extension).** With `Continuous p`, kinetic extends to the
46 closed positive quadrant.
474. **Composition.** Residual premise + continuity ⇒ closed-positive kinetic.
485. **Balance on the positive diagonal** follows from the residual at `t = 0`.
49
50## Scope
51
52Chart carrier `LedgerState` only. No flag flip. No claim that B1 is
53unconditional. No claim that the Hamiltonian lead is closed.
54-/
55
56namespace IndisputableMonolith
57namespace Gravity
58namespace SevenGaps
59namespace MomentumMagnitudeBridge
60
61open ChartFromLedgerMomentum MomentumAdditivity
62open DynamicStructureBracket HypersurfaceDeformation
63
64private lemma sum_zmod2 (g : ZMod 2 → ℝ) : (∑ j : ZMod 2, g j) = g 0 + g 1 := by
65 have huniv : (Finset.univ : Finset (ZMod 2)) = {0, 1} := by decide
66 rw [huniv, Finset.sum_pair (by decide : (0 : ZMod 2) ≠ 1)]
67
68noncomputable section
69
70/-! ## §0. The residual premise, named -/
71
72/-- **Per-orbit energy-equals-cost.** Residual physical premise of the
73momentum-magnitude bridge. -/
74def EnergyEqualsCost (p : LedgerState → ℝ) : Prop :=
75 ∀ k t : ℝ, 0 < k → p (orbitPoint k t) ^ 2 = 2 * k * Cost.Jlog t
76
77def KineticOnOpenPositiveQuadrant (p : LedgerState → ℝ) : Prop :=
78 ∀ z : LedgerState, 0 < z.1 → 0 < z.2 → p z ^ 2 = imbalance z ^ 2
79
80def KineticOnClosedPositiveQuadrant (p : LedgerState → ℝ) : Prop :=
81 ∀ z : LedgerState, 0 ≤ z.1 → 0 ≤ z.2 → p z ^ 2 = imbalance z ^ 2
82
83/-! ## §1. L1: orbit coverage -/
84
85private theorem exp_log_div_two {a : ℝ} (ha : 0 < a) :
86 Real.exp (Real.log a / 2) = Real.sqrt a := by
87 have hmul : Real.exp (Real.log a / 2) * Real.exp (Real.log a / 2) = a := by
88 rw [← Real.exp_add, show Real.log a / 2 + Real.log a / 2 = Real.log a from by ring,
89 Real.exp_log ha]
90 have hsq : (Real.exp (Real.log a / 2)) ^ 2 = (Real.sqrt a) ^ 2 := by
91 rw [pow_two, hmul, pow_two, Real.mul_self_sqrt ha.le]
92 exact (sq_eq_sq_iff_eq_or_eq_neg.mp hsq).resolve_right (by
93 intro hneg
94 linarith [Real.exp_pos (Real.log a / 2), Real.sqrt_nonneg a])
95
96private theorem sqrt_mul_sqrt_div {d c : ℝ} (hd : 0 < d) (hc : 0 < c) :
97 Real.sqrt (d * c) * Real.sqrt (d / c) = d := by
98 have hprod : 0 ≤ d * c := (mul_pos hd hc).le
99 have hquot : 0 < d / c := div_pos hd hc
100 have hsq : (Real.sqrt (d * c) * Real.sqrt (d / c)) ^ 2 = d ^ 2 := by
101 calc (Real.sqrt (d * c) * Real.sqrt (d / c)) ^ 2
102 = (Real.sqrt (d * c)) ^ 2 * (Real.sqrt (d / c)) ^ 2 := by ring
103 _ = (d * c) * (d / c) := by rw [Real.sq_sqrt hprod, Real.sq_sqrt hquot.le]
104 _ = d ^ 2 := by field_simp
105 exact (sq_eq_sq_iff_eq_or_eq_neg.mp hsq).resolve_right (by
106 intro hneg
107 have hpos : 0 < Real.sqrt (d * c) * Real.sqrt (d / c) :=
108 mul_pos (Real.sqrt_pos.mpr (mul_pos hd hc)) (Real.sqrt_pos.mpr hquot)
109 linarith)
110
111private theorem exp_neg_log_div_two {d c : ℝ} (hd : 0 < d) (hc : 0 < c) :
112 Real.exp (-(Real.log (d / c) / 2)) = Real.sqrt (c / d) := by
113 have hqi : 0 < c / d := div_pos hc hd
114 have hlog : -(Real.log (d / c)) = Real.log (c / d) := by
115 rw [← Real.log_inv, inv_div]
116 have hform : -(Real.log (d / c) / 2) = (-Real.log (d / c)) / 2 := by ring
117 rw [hform, hlog]
118 exact exp_log_div_two hqi
119
120private theorem orbit_fst (d c : ℝ) (hd : 0 < d) (hc : 0 < c) :
121 Real.sqrt (d * c) * Real.exp (Real.log (d / c) / 2) = d := by
122 rw [exp_log_div_two (div_pos hd hc), sqrt_mul_sqrt_div hd hc]
123
124private theorem orbit_snd (d c : ℝ) (hd : 0 < d) (hc : 0 < c) :
125 Real.sqrt (d * c) * Real.exp (-(Real.log (d / c)) / 2) = c := by
126 have hform : -(Real.log (d / c)) / 2 = -(Real.log (d / c) / 2) := by ring
127 rw [hform, exp_neg_log_div_two hd hc]
128 have h := sqrt_mul_sqrt_div hc hd
129 rwa [mul_comm c d] at h
130
131/-- **L1.** Every open-positive-quadrant state lies on its Casimir orbit. -/
132theorem orbit_coverage (z : LedgerState) (hd : 0 < z.1) (hc : 0 < z.2) :
133 z = orbitPoint (casimir z) (Real.log (z.1 / z.2)) := by
134 apply Prod.ext
135 · -- fst
136 have h := orbit_fst z.1 z.2 hd hc
137 simpa [orbitPoint, casimir] using h.symm
138 · -- snd: align `orbitPoint`'s `exp (-t/2)` spelling
139 have h := orbit_snd z.1 z.2 hd hc
140 have hform : (-(Real.log (z.1 / z.2)) / 2) = -(Real.log (z.1 / z.2) / 2) := by
141 ring
142 simpa [orbitPoint, casimir, hform] using h.symm
143
144/-! ## §2. L2: per-orbit reduction -/
145
146/-- **L2.** Under `EnergyEqualsCost`, kinetic holds on the open positive quadrant. -/
147theorem energy_equals_cost_implies_kinetic_on_open_positive
148 {p : LedgerState → ℝ} (hE : EnergyEqualsCost p) :
149 KineticOnOpenPositiveQuadrant p := by
150 intro z hd hc
151 have hz := orbit_coverage z hd hc
152 have hk : 0 < casimir z := mul_pos hd hc
153 have hke := hE (casimir z) (Real.log (z.1 / z.2)) hk
154 have hkin := kinetic_on_orbit (casimir z) (Real.log (z.1 / z.2)) hk hke
155 rw [hz]; exact hkin
156
157theorem balance_vanishing_on_positive_diagonal_of_energy_equals_cost
158 {p : LedgerState → ℝ} (hE : EnergyEqualsCost p) (k : ℝ) (hk : 0 < k) :
159 p (orbitPoint k 0) = 0 := by
160 have hke := hE k 0 hk
161 have hJ : Cost.Jlog 0 = 0 := by
162 rw [Cost.Jlog_as_cosh, Real.cosh_zero]; norm_num
163 rw [hJ, mul_zero] at hke
164 exact sq_eq_zero_iff.mp hke
165
166/-! ## §3. L3: continuous extension -/
167
168theorem continuous_imbalance : Continuous (imbalance : LedgerState → ℝ) :=
169 continuous_fst.sub continuous_snd
170
171/-- **L3.** Continuity extends open-positive kinetic to the closed positive quadrant. -/
172theorem kinetic_extends_to_closed_positive_quadrant
173 {p : LedgerState → ℝ} (hcont : Continuous p)
174 (hopen : KineticOnOpenPositiveQuadrant p) :
175 KineticOnClosedPositiveQuadrant p := by
176 intro z hd hc
177 by_cases hstrict : 0 < z.1 ∧ 0 < z.2
178 · exact hopen z hstrict.1 hstrict.2
179 · let w : ℕ → LedgerState := fun n =>
180 (z.1 + 1 / (n + 1 : ℝ), z.2 + 1 / (n + 1 : ℝ))
181 have hw_open : ∀ n, 0 < (w n).1 ∧ 0 < (w n).2 := by
182 intro n
183 have hpos : (0 : ℝ) < 1 / (n + 1 : ℝ) := by positivity
184 exact ⟨by linarith [hd, hpos], by linarith [hc, hpos]⟩
185 have hkin_w : ∀ n, p (w n) ^ 2 = imbalance (w n) ^ 2 := fun n =>
186 hopen (w n) (hw_open n).1 (hw_open n).2
187 have hw_tendsto : Filter.Tendsto w Filter.atTop (nhds z) := by
188 have h1 : Filter.Tendsto (fun n : ℕ => z.1 + 1 / (n + 1 : ℝ)) Filter.atTop
189 (nhds z.1) := by
190 convert tendsto_one_div_add_atTop_nhds_zero_nat.const_add z.1 using 1
191 simp
192 have h2 : Filter.Tendsto (fun n : ℕ => z.2 + 1 / (n + 1 : ℝ)) Filter.atTop
193 (nhds z.2) := by
194 convert tendsto_one_div_add_atTop_nhds_zero_nat.const_add z.2 using 1
195 simp
196 exact h1.prodMk_nhds h2
197 have hp_lim := (hcont.tendsto _).comp hw_tendsto
198 have hi_lim := (continuous_imbalance.tendsto _).comp hw_tendsto
199 have hpsq := (continuous_pow 2).continuousAt.tendsto.comp hp_lim
200 have hisq := (continuous_pow 2).continuousAt.tendsto.comp hi_lim
201 exact tendsto_nhds_unique hpsq (hisq.congr fun n => (hkin_w n).symm)
202
203theorem energy_equals_cost_continuous_implies_kinetic_on_closed
204 {p : LedgerState → ℝ} (hE : EnergyEqualsCost p) (hcont : Continuous p) :
205 KineticOnClosedPositiveQuadrant p :=
206 kinetic_extends_to_closed_positive_quadrant hcont
207 (energy_equals_cost_implies_kinetic_on_open_positive hE)
208
209/-! ## §4. SwapOdd / quadrant coverage -/
210
211theorem swap_odd_preserves_kinetic_pointwise {p : LedgerState → ℝ}
212 (hswap : SwapOdd p) (z : LedgerState)
213 (hkin : p z ^ 2 = imbalance z ^ 2) :
214 p (z.2, z.1) ^ 2 = imbalance (z.2, z.1) ^ 2 := by
215 rw [hswap z, imbalance_swap z, neg_sq, neg_sq, hkin]
216
217theorem swap_maps_open_positive_to_itself {z : LedgerState}
218 (hd : 0 < z.1) (hc : 0 < z.2) :
219 0 < (z.2, z.1).1 ∧ 0 < (z.2, z.1).2 :=
220 ⟨hc, hd⟩
221
222theorem orbitPoint_nonneg (k t : ℝ) (_hk : 0 ≤ k) :
223 0 ≤ (orbitPoint k t).1 ∧ 0 ≤ (orbitPoint k t).2 := by
224 simp only [orbitPoint]
225 exact ⟨mul_nonneg (Real.sqrt_nonneg _) (Real.exp_nonneg _),
226 mul_nonneg (Real.sqrt_nonneg _) (Real.exp_nonneg _)⟩
227
228theorem negative_quadrant_not_on_orbit (z : LedgerState)
229 (hd : z.1 < 0) (_hc : z.2 < 0) (k t : ℝ) (hk : 0 ≤ k) :
230 orbitPoint k t ≠ z := by
231 intro heq
232 have hnn := (orbitPoint_nonneg k t hk).1
233 have h1 : (orbitPoint k t).1 = z.1 := congrArg Prod.fst heq
234 linarith
235
236/-! ## §5. Named candidate failures -/
237
238/-- Gradient-only decoy: zero momenta, configurations `(0,1)`, lapse `N ≡ 2`. -/
239theorem hamDyn_decoy_value :
240 HamDyn (fun _ : ZMod 2 => (2 : ℝ))
241 (fun j : ZMod 2 => if j = (0 : ZMod 2) then (0 : ℝ) else 1,
242 fun _ : ZMod 2 => (0 : ℝ)) = 3 := by
243 simp only [HamDyn]
244 have h01 : (0 : ZMod 2) + 1 = 1 := by decide
245 have h10 : (1 : ZMod 2) + 1 = 0 := by decide
246 rw [sum_zmod2]
247 simp [h01, h10]
248 norm_num
249
250/-- **The named candidate `HamDyn` has a gradient sector at zero momenta.**
251This is a fact about `HamDyn` on `PhaseSpace 2` only: no carrier map from
252`PhaseSpace 2` objects to `LedgerState` observables is stated anywhere in the
253library, so this theorem neither refutes nor discharges
254`EnergyEqualsCost`, and no "is a `Jlog` Hamiltonian" predicate is formalized
255for it to speak to. The general lead, some Hamiltonian on some carrier
256deriving the residual premise, remains open. -/
257theorem hamDyn_gradient_sector_nonzero_at_zero_momenta :
258 ∃ (N : ZMod 2 → ℝ) (x : PhaseSpace 2),
259 (∀ i : ZMod 2, x.2 i = 0) ∧ HamDyn N x ≠ 0 := by
260 refine ⟨fun _ => 2, (fun j => if j = (0 : ZMod 2) then (0 : ℝ) else 1,
261 fun _ => 0), fun _ => rfl, ?_⟩
262 rw [hamDyn_decoy_value]; norm_num
263
264/-- **Quadratic kinetic form is not Jlog.** Witness: at `t = 1`, equality would
265force `sinh (1/2) ^ 2 = 1/4`, but `sinh` is strictly increasing through a
266positive value smaller than `1/2` at a smaller argument, contradicting
267`sinh x > x` failure — use the chart module's comparison style instead. -/
268theorem Jlog_ne_half_sq : Cost.Jlog ≠ fun t : ℝ => t ^ 2 / 2 := by
269 intro h
270 have h1 := congrFun h 1
271 rw [Jlog_eq_two_sinh_half_sq] at h1
272 -- 2 * sinh(1/2)^2 = 1/2 ⇒ sinh(1/2)^2 = 1/4
273 have hsq : Real.sinh (1 / 2 : ℝ) ^ 2 = (1 : ℝ) / 4 := by
274 have : (2 : ℝ) * Real.sinh (1 / 2) ^ 2 = 1 / 2 := by
275 convert h1 using 1; norm_num
276 linarith
277 -- sinh(1/2) > 0 and sinh(1/2) ≠ 1/2: compare to sinh of a smaller positive arg
278 have hpos : 0 < Real.sinh (1 / 2 : ℝ) := by
279 have := Real.sinh_lt_sinh.mpr (by norm_num : (0 : ℝ) < 1 / 2)
280 simpa using this
281 have hne : Real.sinh (1 / 2 : ℝ) ≠ 1 / 2 := by
282 -- From cosh² - sinh² = 1: if sinh = 1/2 then cosh² = 5/4, cosh = √(5/4)
283 -- and exp(1/2) = cosh + sinh. Use exp(1/2)^2 = exp 1 > 2.7, while
284 -- (√(5/4) + 1/2)^2 = 5/4 + √(5/4) + 1/4 = 3/2 + √(5/4) < 3/2 + 1.2 = 2.7.
285 intro hs
286 have hid := Real.cosh_sq_sub_sinh_sq (1 / 2 : ℝ)
287 rw [hs] at hid
288 have hcosh_sq : Real.cosh (1 / 2) ^ 2 = 5 / 4 := by
289 norm_num at hid; linarith
290 have hcosh_pos : 0 < Real.cosh (1 / 2) := Real.cosh_pos _
291 have hcosh_val : Real.cosh (1 / 2) = Real.sqrt (5 / 4) := by
292 have h := sq_eq_sq_iff_eq_or_eq_neg.mp
293 (hcosh_sq.trans (Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 5 / 4)).symm)
294 exact h.resolve_right (by intro hneg; linarith [hcosh_pos, Real.sqrt_nonneg (5/4:ℝ)])
295 have hexp : Real.exp (1 / 2) = Real.cosh (1 / 2) + Real.sinh (1 / 2) := by
296 rw [Real.cosh_eq, Real.sinh_eq]; ring
297 rw [hs, hcosh_val] at hexp
298 have hexp_sq : (Real.exp (1 / 2)) ^ 2 = Real.exp 1 := by
299 rw [← Real.exp_nat_mul]; norm_num
300 have hexp1_gt : (2.7 : ℝ) < Real.exp 1 := by linarith [Real.exp_one_gt_d9]
301 -- √(5/4) < 1.2, so (√(5/4)+1/2)^2 < (1.2+0.5)^2 = 2.89, need tighter:
302 -- √(5/4) = √1.25 < 1.12 since 1.12^2 = 1.2544 > 1.25
303 have hsqrt_lt : Real.sqrt (5 / 4) < 1.12 := by
304 apply (Real.sqrt_lt' (by norm_num)).2
305 norm_num
306 have hrhs_sq : (Real.sqrt (5 / 4) + 1 / 2) ^ 2 < 2.7 := by
307 nlinarith [hsqrt_lt]
308 have : (Real.exp (1 / 2)) ^ 2 < 2.7 := by
309 rw [hexp]; exact hrhs_sq
310 rw [hexp_sq] at this
311 linarith
312 -- From hsq, sinh = ±1/2; positivity kills the minus; hne kills the plus
313 have : Real.sinh (1 / 2) = 1 / 2 ∨ Real.sinh (1 / 2) = -(1 / 2) := by
314 have := sq_eq_sq_iff_eq_or_eq_neg.mp (hsq.trans (by norm_num :
315 ((1 : ℝ) / 4) = (1 / 2) ^ 2))
316 simpa using this
317 rcases this with hpos' | hneg
318 · exact hne hpos'
319 · linarith [hpos]
320
321private theorem chart_product_sq_form (k m : ℝ) (hk : 0 < k) :
322 (m / (2 * Real.sqrt k)) ^ 2 = m ^ 2 / (4 * k) := by
323 have hden : (2 * Real.sqrt k) ^ 2 = 4 * k := by
324 calc (2 * Real.sqrt k) ^ 2
325 = (2 : ℝ) ^ 2 * (Real.sqrt k) ^ 2 := by rw [mul_pow]
326 _ = 4 * k := by rw [Real.sq_sqrt hk.le]; norm_num
327 calc (m / (2 * Real.sqrt k)) ^ 2
328 = m ^ 2 / (2 * Real.sqrt k) ^ 2 := by rw [div_pow]
329 _ = m ^ 2 / (4 * k) := by rw [hden]
330
331/-- **Profile-parameter matching is the chart product, stated as scalar
332algebra.** Matching `2 (lam * p_val) ^ 2` to orbit exactness, for a *scalar*
333`p_val`, is equivalent to the chart product form. This neither constructs nor
334discharges the ledger-level `EnergyEqualsCost` premise: `p_val` here is a real
335parameter, not a `LedgerState → ℝ` observable, and `EnergyEqualsCost` does not
336appear in the statement. -/
337theorem exact_cost_profile_recovers_chart_product
338 (k t lam p_val : ℝ) (hk : 0 < k) :
339 (2 * (lam * p_val) ^ 2 = imbalance (orbitPoint k t) ^ 2 / (2 * k)) ↔
340 (lam * p_val) ^ 2 =
341 (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) ^ 2 := by
342 have hrhs := chart_product_sq_form k (imbalance (orbitPoint k t)) hk
343 constructor
344 · intro h
345 calc (lam * p_val) ^ 2
346 = (2 * (lam * p_val) ^ 2) / 2 := by ring
347 _ = (imbalance (orbitPoint k t) ^ 2 / (2 * k)) / 2 := by rw [h]
348 _ = imbalance (orbitPoint k t) ^ 2 / (4 * k) := by ring
349 _ = (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) ^ 2 := hrhs.symm
350 · intro h
351 calc 2 * (lam * p_val) ^ 2
352 = 2 * (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) ^ 2 := by rw [h]
353 _ = 2 * (imbalance (orbitPoint k t) ^ 2 / (4 * k)) := by rw [hrhs]
354 _ = imbalance (orbitPoint k t) ^ 2 / (2 * k) := by ring
355
356theorem energy_equals_cost_of_imbalance : EnergyEqualsCost imbalance := by
357 intro k t hk
358 have h := Jlog_eq_imbalance_sq_div_two_casimir k t hk
359 have hk2 : (2 : ℝ) * k ≠ 0 := mul_ne_zero two_ne_zero hk.ne'
360 calc imbalance (orbitPoint k t) ^ 2
361 = Cost.Jlog t * (2 * k) := by rw [h]; field_simp
362 _ = 2 * k * Cost.Jlog t := by ring
363
364theorem chart_product_fails_for_imbalance_at_unit_lam
365 (k t : ℝ) (hk : 0 < k) (hkne : 4 * k ≠ 1)
366 (hm : imbalance (orbitPoint k t) ≠ 0) :
367 ¬ ((1 : ℝ) * imbalance (orbitPoint k t)) ^ 2 =
368 (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) ^ 2 := by
369 intro h
370 have hrhs := chart_product_sq_form k (imbalance (orbitPoint k t)) hk
371 have h' : imbalance (orbitPoint k t) ^ 2 =
372 imbalance (orbitPoint k t) ^ 2 / (4 * k) := by
373 rw [← hrhs]
374 simpa only [one_mul] using h
375 have hk4 : (4 : ℝ) * k ≠ 0 := mul_ne_zero (by norm_num) hk.ne'
376 have hmul : imbalance (orbitPoint k t) ^ 2 * (4 * k) =
377 imbalance (orbitPoint k t) ^ 2 :=
378 (eq_div_iff hk4).mp h'
379 have hfac : (4 : ℝ) * k = 1 :=
380 mul_left_cancel₀ (pow_ne_zero 2 hm) (hmul.trans (mul_one _).symm)
381 exact hkne hfac
382
383/-! ## §5b. The reduction is an equivalence, and the residual is independent -/
384
385/-- Orbit points at positive Casimir lie in the open positive quadrant. -/
386theorem orbitPoint_pos (k t : ℝ) (hk : 0 < k) :
387 0 < (orbitPoint k t).1 ∧ 0 < (orbitPoint k t).2 := by
388 simp only [orbitPoint]
389 exact ⟨mul_pos (Real.sqrt_pos.mpr hk) (Real.exp_pos _),
390 mul_pos (Real.sqrt_pos.mpr hk) (Real.exp_pos _)⟩
391
392/-- **The reduction is exact on the open positive quadrant.** The kinetic
393condition there holds *if and only if* `EnergyEqualsCost p` holds: the premise
394is a rewrite of the quadrant condition, not a strictly weaker residue. The
395global gap (Q2–Q4, axes beyond continuity) is unchanged. -/
396theorem open_positive_kinetic_iff_energy_equals_cost {p : LedgerState → ℝ} :
397 KineticOnOpenPositiveQuadrant p ↔ EnergyEqualsCost p := by
398 constructor
399 · intro h k t hk
400 have hpos := orbitPoint_pos k t hk
401 have hk2 := h (orbitPoint k t) hpos.1 hpos.2
402 have hchart := Jlog_eq_imbalance_sq_div_two_casimir k t hk
403 have hne : (2 : ℝ) * k ≠ 0 := mul_ne_zero two_ne_zero hk.ne'
404 calc p (orbitPoint k t) ^ 2
405 = imbalance (orbitPoint k t) ^ 2 := hk2
406 _ = Cost.Jlog t * (2 * k) := by rw [hchart]; field_simp
407 _ = 2 * k * Cost.Jlog t := by ring
408 · exact energy_equals_cost_implies_kinetic_on_open_positive
409
410/-- **Independence countermodel.** Twice the imbalance fails the residual
411premise: at `k = t = 1` the premise would force `8 * Jlog 1 = 2 * Jlog 1`,
412but `Jlog 1 > 0`. -/
413theorem two_imbalance_fails_energy_equals_cost :
414 ¬ EnergyEqualsCost (fun z : LedgerState => 2 * imbalance z) := by
415 intro h
416 have h1 := h 1 1 one_pos
417 change (2 * imbalance (orbitPoint (1:ℝ) (1:ℝ))) ^ 2 =
418 2 * (1:ℝ) * Cost.Jlog 1 at h1
419 have hsq : imbalance (orbitPoint (1:ℝ) (1:ℝ)) ^ 2 = 2 * Cost.Jlog 1 := by
420 have hc := Jlog_eq_imbalance_sq_div_two_casimir (1:ℝ) 1 one_pos
421 calc imbalance (orbitPoint (1:ℝ) (1:ℝ)) ^ 2
422 = Cost.Jlog 1 * (2 * 1) := by rw [hc]; field_simp
423 _ = 2 * Cost.Jlog 1 := by ring
424 have hsin : 0 < Real.sinh (1 / 2 : ℝ) := by
425 have := Real.sinh_lt_sinh.mpr (by norm_num : (0 : ℝ) < 1 / 2)
426 simpa using this
427 have hJpos : 0 < Cost.Jlog 1 := by
428 rw [Jlog_eq_two_sinh_half_sq]
429 have hsq_pos : 0 < Real.sinh (1 / 2 : ℝ) ^ 2 :=
430 sq_pos_of_ne_zero (ne_of_gt hsin)
431 linarith
432 rw [show (2 * imbalance (orbitPoint (1:ℝ) (1:ℝ))) ^ 2 =
433 4 * (imbalance (orbitPoint (1:ℝ) (1:ℝ)) ^ 2) from by ring, hsq] at h1
434 have hz : Cost.Jlog 1 = 0 := by linarith
435 linarith
436
437/-- **The residual is independent of the momentum package.** `2 * imbalance`
438satisfies every derived property of the B1 package (continuity, swap-oddness,
439additivity, balance-vanishing) and fails `EnergyEqualsCost`. -/
440theorem two_imbalance_package :
441 Continuous (fun z : LedgerState => 2 * imbalance z) ∧
442 SwapOdd (fun z : LedgerState => 2 * imbalance z) ∧
443 (∀ z w : LedgerState,
444 2 * imbalance (z + w) = 2 * imbalance z + 2 * imbalance w) ∧
445 (∀ z : LedgerState, Balanced z → 2 * imbalance z = 0) ∧
446 ¬ EnergyEqualsCost (fun z : LedgerState => 2 * imbalance z) :=
447 ⟨continuous_const.mul continuous_imbalance,
448 fun z => by
449 show 2 * imbalance (z.2, z.1) = -(2 * imbalance z)
450 rw [imbalance_swap]; ring,
451 fun z w => by
452 rw [imbalance_add]; ring,
453 fun z hz => by
454 show 2 * (z.1 - z.2) = 0
455 have hz' : z.1 = z.2 := hz
456 rw [hz', sub_self, mul_zero],
457 two_imbalance_fails_energy_equals_cost⟩
458
459/-! ## §6. Certificate -/
460
461structure MomentumMagnitudeBridgeVerdict : Prop where
462 orbit_coverage_holds : ∀ z : LedgerState, 0 < z.1 → 0 < z.2 →
463 z = orbitPoint (casimir z) (Real.log (z.1 / z.2))
464 energy_equals_cost_implies_open_kinetic :
465 ∀ p : LedgerState → ℝ, EnergyEqualsCost p → KineticOnOpenPositiveQuadrant p
466 continuous_extends_kinetic : ∀ p : LedgerState → ℝ, Continuous p →
467 KineticOnOpenPositiveQuadrant p → KineticOnClosedPositiveQuadrant p
468 composition : ∀ p : LedgerState → ℝ, EnergyEqualsCost p → Continuous p →
469 KineticOnClosedPositiveQuadrant p
470 balance_on_positive_diagonal_from_residual :
471 ∀ p : LedgerState → ℝ, EnergyEqualsCost p → ∀ k : ℝ, 0 < k →
472 p (orbitPoint k 0) = 0
473 swap_preserves_kinetic_stays_in_quadrant :
474 (∀ p : LedgerState → ℝ, SwapOdd p → ∀ z : LedgerState,
475 p z ^ 2 = imbalance z ^ 2 →
476 p (z.2, z.1) ^ 2 = imbalance (z.2, z.1) ^ 2) ∧
477 (∀ z : LedgerState, 0 < z.1 → 0 < z.2 →
478 0 < (z.2, z.1).1 ∧ 0 < (z.2, z.1).2)
479 negative_quadrant_uncovered :
480 ∀ z : LedgerState, z.1 < 0 → z.2 < 0 → ∀ k t : ℝ, 0 ≤ k → orbitPoint k t ≠ z
481 /-- The reduction is an exact equivalence on the open positive quadrant. -/
482 reduction_exact_on_open_quadrant : ∀ p : LedgerState → ℝ,
483 KineticOnOpenPositiveQuadrant p ↔ EnergyEqualsCost p
484 /-- The residual is independent of the momentum package: `2 * imbalance`
485 satisfies continuity, swap-oddness, additivity, and balance-vanishing, and
486 fails the premise. -/
487 residual_independent :
488 Continuous (fun z : LedgerState => 2 * imbalance z) ∧
489 SwapOdd (fun z : LedgerState => 2 * imbalance z) ∧
490 (∀ z w : LedgerState,
491 2 * imbalance (z + w) = 2 * imbalance z + 2 * imbalance w) ∧
492 (∀ z : LedgerState, Balanced z → 2 * imbalance z = 0) ∧
493 ¬ EnergyEqualsCost (fun z : LedgerState => 2 * imbalance z)
494 /-- The *named* Hamiltonian candidates fail: `HamDyn` has a gradient sector
495 at zero momenta, and `Jlog` is not the quadratic form. These are facts about
496 named objects on their own carriers; the general lead (an arbitrary
497 Hamiltonian deriving the premise) is neither discharged nor refuted. -/
498 named_bracket_candidates_fail :
499 (∃ (N : ZMod 2 → ℝ) (x : PhaseSpace 2),
500 (∀ i : ZMod 2, x.2 i = 0) ∧ HamDyn N x ≠ 0) ∧
501 Cost.Jlog ≠ fun t : ℝ => t ^ 2 / 2
502 /-- Profile-parameter matching is the chart product (scalar algebra; the
503 ledger-level premise is not mentioned). -/
504 profile_matching_recovers_chart_product : ∀ (k t lam p_val : ℝ), 0 < k →
505 ((2 * (lam * p_val) ^ 2 = imbalance (orbitPoint k t) ^ 2 / (2 * k)) ↔
506 (lam * p_val) ^ 2 =
507 (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) ^ 2)
508 residual_inhabited_and_not_discharged_by_unit_lam_profile :
509 EnergyEqualsCost imbalance ∧
510 (∀ k t : ℝ, 0 < k → 4 * k ≠ 1 → imbalance (orbitPoint k t) ≠ 0 →
511 ¬ ((1 : ℝ) * imbalance (orbitPoint k t)) ^ 2 =
512 (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) ^ 2)
513
514theorem momentumMagnitudeBridgeVerdict : MomentumMagnitudeBridgeVerdict where
515 orbit_coverage_holds := orbit_coverage
516 energy_equals_cost_implies_open_kinetic := fun _ =>
517 energy_equals_cost_implies_kinetic_on_open_positive
518 continuous_extends_kinetic := fun _ => kinetic_extends_to_closed_positive_quadrant
519 composition := fun _ => energy_equals_cost_continuous_implies_kinetic_on_closed
520 balance_on_positive_diagonal_from_residual := fun _ =>
521 balance_vanishing_on_positive_diagonal_of_energy_equals_cost
522 swap_preserves_kinetic_stays_in_quadrant :=
523 ⟨fun _ => swap_odd_preserves_kinetic_pointwise,
524 fun _ => swap_maps_open_positive_to_itself⟩
525 negative_quadrant_uncovered := negative_quadrant_not_on_orbit
526 reduction_exact_on_open_quadrant := fun _ =>
527 open_positive_kinetic_iff_energy_equals_cost
528 residual_independent := two_imbalance_package
529 named_bracket_candidates_fail :=
530 ⟨hamDyn_gradient_sector_nonzero_at_zero_momenta, Jlog_ne_half_sq⟩
531 profile_matching_recovers_chart_product := exact_cost_profile_recovers_chart_product
532 residual_inhabited_and_not_discharged_by_unit_lam_profile :=
533 ⟨energy_equals_cost_of_imbalance, chart_product_fails_for_imbalance_at_unit_lam⟩
534
535/-! ## Axiom audit -/
536
537#print axioms orbit_coverage
538#print axioms energy_equals_cost_implies_kinetic_on_open_positive
539#print axioms balance_vanishing_on_positive_diagonal_of_energy_equals_cost
540#print axioms kinetic_extends_to_closed_positive_quadrant
541#print axioms energy_equals_cost_continuous_implies_kinetic_on_closed
542#print axioms swap_odd_preserves_kinetic_pointwise
543#print axioms negative_quadrant_not_on_orbit
544#print axioms orbitPoint_pos
545#print axioms open_positive_kinetic_iff_energy_equals_cost
546#print axioms two_imbalance_fails_energy_equals_cost
547#print axioms two_imbalance_package
548#print axioms hamDyn_gradient_sector_nonzero_at_zero_momenta
549#print axioms hamDyn_decoy_value
550#print axioms Jlog_ne_half_sq
551#print axioms exact_cost_profile_recovers_chart_product
552#print axioms energy_equals_cost_of_imbalance
553#print axioms chart_product_fails_for_imbalance_at_unit_lam
554#print axioms momentumMagnitudeBridgeVerdict
555
556end
557end MomentumMagnitudeBridge
558end SevenGaps
559end Gravity
560end IndisputableMonolith
561