IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivityComposition
IndisputableMonolith/Gravity/SevenGaps/Gap5MomentumAdditivityComposition.lean · 413 lines · 26 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap5EnergyEqualsCostDerivation
2import IndisputableMonolith.Cost.SymplecticAction
3
4/-!
5# Unconditional momentum additivity: composition-law attack
6
7**Verdict, stated first.** Of the three charged outcomes, **(b) LANDED** as the
8headline and **(c) LANDED** as the constructive corollary; **(a) is refuted by
9the no-go**, not merely unbuilt.
10
11The consumer
12`energyEqualsCost_of_additive_continuous_balanced_unit` already proves that
13additivity under ledger consolidation, continuity, balance-vanishing, and unit
14normalization `p (1,0) ^ 2 = 1` force `EnergyEqualsCost`. This module attacks
15the remaining premise: unconditional additivity, from the recognition
16composition law. B1's kinetic-conditional additivity is not an input.
17
18## (b) The no-go: the composition law does not select additivity
19
20The recognition composition law (`SatisfiesCompositionLaw`) is a constraint on
21cost functionals `F : ℝ → ℝ` of positive ledger ratios. On the stated chart
22carrier `LedgerState`, the ambient recognition cost is `Cost.Jcost`, and it
23satisfies the law (`jcost_satisfiesCompositionLaw_via_symplectic`). That fact
24is independent of any choice of momentum observable `p : LedgerState → ℝ`: the
25law never mentions `p`.
26
27The same carrier admits two continuous, balance-vanishing, unit-normalized
28momentum observables that disagree on additivity under consolidation:
29
30* `imbalance`, which is additive (`imbalance_is_additive_continuous_balanced`);
31* the absolute imbalance `z ↦ |imbalance z|`, which fails additivity at the
32 consolidation of `(1,0)` with `(0,1)` (`abs_imbalance_not_additive`).
33
34Both packages pass every companion the consumer still consumes except
35additivity itself. Hence on this stated system, no derivation whose only
36inputs are the recognition composition law (the ambient cost being an RCL
37solution) together with continuity, balance-vanishing, and unit normalization
38can conclude additivity: the data admit both packages
39(`momentum_additivity_independent_of_composition_law`).
40
41Scope (per `L-qg-witness-is-not-a-class-20260729`): the theorem is a
42two-package witness on the stated `LedgerState` chart system with ambient cost
43`Jcost`. It is not a quantified class theorem over all cost systems, and the
44prose does not say "class" or "general."
45
46A second witness in the swap-odd sector: the unit-normalized reparametrization
47`nlP ∘ imbalance / 2` is continuous, swap-odd, balance-vanishing, and
48unit-normalized, yet fails additivity (`nlP_unit_not_additive`). So even
49adding debit-credit parity to the companions does not restore additivity
50without a kinetic / EnergyEqualsCost-like hypothesis (which this module
51refuses as input).
52
53## (c) The sharper reduction: net-imbalance reading plus 1D Cauchy
54
55Full two-argument additivity on `LedgerState` is stronger than what the
56consumer needs as a named posting property. The strictly simpler package
57
581. **net-imbalance reading** `ReadsNetImbalance p`:
59 `∀ z, p z = p (imbalance z, 0)`
60 (cancelling a balanced debit-credit pair never changes the momentum),
612. **1D additivity on the debit axis**
62 `∀ m n, p (m, 0) + p (n, 0) = p (m + n, 0)`,
633. continuity of `p`,
644. unit normalization `p (1, 0) ^ 2 = 1`,
65
66already forces `p = ± imbalance`, hence full consolidation additivity, hence
67`EnergyEqualsCost p`
68(`energyEqualsCost_of_net_imbalance_reading_additive_unit`). Balance-vanishing
69is derived, not assumed. This is the chart successor's remaining named input,
70stated as a one-dimensional Cauchy problem on the net charge together with the
71structural claim that momentum reads only that charge.
72
73## What is NOT claimed
74
75* No flag flip. Flags 6 and 12 still rest on `EnergyEqualsCost`; the premise
76 is not discharged, because additivity (equivalently, the net-imbalance
77 reading package) is not derived from the composition law.
78* The no-go kills derivations from the composition law plus the consumer
79 companions alone. It does not touch a derivation that imports a further
80 non-cost structure of the ledger (for example a proof of
81 `ReadsNetImbalance` from posting axioms).
82* B1's kinetic-conditional additivity is neither used nor strengthened.
83-/
84
85namespace IndisputableMonolith
86namespace Gravity
87namespace SevenGaps
88namespace MomentumAdditivityComposition
89
90open ChartFromLedgerMomentum MomentumAdditivity MomentumMagnitudeBridge
91open EnergyEqualsCostDerivation
92open Cost.FunctionalEquation
93
94noncomputable section
95
96/-! ## §0. Ambient composition law on the stated carrier -/
97
98/-- **The chart system's recognition cost satisfies the composition law.**
99Imported from the symplectic derivation: σ = 0 area preservation supplies the
100trace identity that is `SatisfiesCompositionLaw` for `Jcost`. -/
101theorem chart_cost_satisfies_composition_law :
102 SatisfiesCompositionLaw Cost.Jcost :=
103 Cost.SymplecticAction.jcost_satisfiesCompositionLaw_via_symplectic
104
105/-- The composition law is a property of the cost alone: it holds of `Jcost`
106regardless of which momentum observable is under discussion. -/
107theorem composition_law_ignores_momentum (_p : LedgerState → ℝ) :
108 SatisfiesCompositionLaw Cost.Jcost :=
109 chart_cost_satisfies_composition_law
110
111/-! ## §1. Companions shared by the witness packages -/
112
113theorem imbalance_unit : imbalance ((1, 0) : LedgerState) ^ 2 = 1 := by
114 simp [imbalance]
115
116theorem imbalance_balance_vanishing :
117 ∀ z : LedgerState, Balanced z → imbalance z = 0 :=
118 fun z hz => show imbalance z = 0 from sub_eq_zero.mpr hz
119
120theorem abs_imbalance_continuous : Continuous fun z : LedgerState => |imbalance z| :=
121 (continuous_fst.sub continuous_snd).abs
122
123theorem abs_imbalance_balance_vanishing :
124 ∀ z : LedgerState, Balanced z → |imbalance z| = 0 := by
125 intro z hz
126 simp [imbalance, show z.1 = z.2 from hz]
127
128theorem abs_imbalance_unit :
129 (fun z : LedgerState => |imbalance z|) (1, 0) ^ 2 = 1 := by
130 simp [imbalance]
131
132/-- Absolute imbalance fails consolidation additivity: consolidating a pure
133debit with a pure credit yields the balanced state, whose absolute imbalance
134is `0 ≠ 1 + 1`. -/
135theorem abs_imbalance_not_additive :
136 ¬ ∀ z w : LedgerState,
137 |imbalance (z + w)| = |imbalance z| + |imbalance w| := by
138 intro h
139 have h1 := h (1, 0) (0, 1)
140 have heq : ((1, 0) : LedgerState) + (0, 1) = (1, 1) := by
141 apply Prod.ext <;> simp
142 rw [heq] at h1
143 norm_num [imbalance] at h1
144
145/-! ## §2. The additive package, and the consumer fires -/
146
147/-- **The additive package:** continuous, balance-vanishing, unit-normalized,
148and additive. The consumer theorem therefore yields `EnergyEqualsCost`. -/
149theorem imbalance_additive_package :
150 Continuous imbalance ∧
151 (∀ z : LedgerState, Balanced z → imbalance z = 0) ∧
152 imbalance ((1, 0) : LedgerState) ^ 2 = 1 ∧
153 (∀ z w : LedgerState, imbalance (z + w) = imbalance z + imbalance w) ∧
154 EnergyEqualsCost imbalance :=
155 ⟨continuous_imbalance, imbalance_balance_vanishing, imbalance_unit,
156 fun z w => by simp [imbalance]; ring,
157 energy_equals_cost_of_imbalance⟩
158
159/-! ## §3. The non-additive package (absolute imbalance) -/
160
161/-- **The absolute-imbalance package:** continuous, balance-vanishing,
162unit-normalized, and *not* additive. Lives on the same carrier with the same
163RCL cost as the additive package. -/
164theorem abs_imbalance_package :
165 Continuous (fun z : LedgerState => |imbalance z|) ∧
166 (∀ z : LedgerState, Balanced z → |imbalance z| = 0) ∧
167 (fun z : LedgerState => |imbalance z|) (1, 0) ^ 2 = 1 ∧
168 ¬ (∀ z w : LedgerState,
169 |imbalance (z + w)| = |imbalance z| + |imbalance w|) :=
170 ⟨abs_imbalance_continuous, abs_imbalance_balance_vanishing, abs_imbalance_unit,
171 abs_imbalance_not_additive⟩
172
173/-! ## §4. Headline no-go (scoped to the stated system) -/
174
175/-- **NO-GO (composition-law independence of additivity).** On the stated
176`LedgerState` chart system whose recognition cost `Jcost` satisfies the
177composition law, there exist two continuous, balance-vanishing,
178unit-normalized momentum observables that disagree on consolidation
179additivity: `imbalance` (additive, and therefore `EnergyEqualsCost`) and
180`|imbalance|` (not additive). The composition law plus those three companions
181therefore cannot force additivity on this system.
182
183Quantifier written first: the theorem is a conjunction of (i) the ambient cost
184satisfies RCL and (ii) two concrete packages on this one carrier. It is not a
185∀-quantified statement over a class of cost systems. -/
186theorem momentum_additivity_independent_of_composition_law :
187 SatisfiesCompositionLaw Cost.Jcost ∧
188 (Continuous imbalance ∧
189 (∀ z : LedgerState, Balanced z → imbalance z = 0) ∧
190 imbalance ((1, 0) : LedgerState) ^ 2 = 1 ∧
191 (∀ z w : LedgerState, imbalance (z + w) = imbalance z + imbalance w) ∧
192 EnergyEqualsCost imbalance) ∧
193 (Continuous (fun z : LedgerState => |imbalance z|) ∧
194 (∀ z : LedgerState, Balanced z → |imbalance z| = 0) ∧
195 (fun z : LedgerState => |imbalance z|) (1, 0) ^ 2 = 1 ∧
196 ¬ (∀ z w : LedgerState,
197 |imbalance (z + w)| = |imbalance z| + |imbalance w|)) :=
198 ⟨chart_cost_satisfies_composition_law, imbalance_additive_package,
199 abs_imbalance_package⟩
200
201/-! ## §5. Swap-odd sector: unit-normalized nlP also fails additivity -/
202
203/-- Unit-normalized reparametrization of the imbalance through `nlP`. -/
204def nlPUnit (z : LedgerState) : ℝ := nlP (imbalance z) / 2
205
206theorem nlPUnit_continuous : Continuous nlPUnit := by
207 have hb : Continuous fun z : LedgerState => imbalance z :=
208 continuous_fst.sub continuous_snd
209 exact ((hb.add (hb.pow 3)).div_const 2).congr fun z => by simp [nlPUnit, nlP]
210
211theorem nlPUnit_swap_odd : SwapOdd nlPUnit := by
212 intro z
213 show nlP (imbalance (z.2, z.1)) / 2 = -(nlP (imbalance z) / 2)
214 rw [imbalance_swap]
215 simp [nlP]
216 ring
217
218theorem nlPUnit_balance_vanishing :
219 ∀ z : LedgerState, Balanced z → nlPUnit z = 0 := by
220 intro z hz
221 have : imbalance z = 0 := sub_eq_zero.mpr hz
222 simp [nlPUnit, nlP, this]
223
224theorem nlPUnit_unit : nlPUnit (1, 0) ^ 2 = 1 := by
225 norm_num [nlPUnit, nlP, imbalance]
226
227theorem nlPUnit_not_additive :
228 ¬ ∀ z w : LedgerState, nlPUnit (z + w) = nlPUnit z + nlPUnit w := by
229 intro h
230 have h1 := h (1, 0) (1, 0)
231 have h2 : ((1, 0) : LedgerState) + (1, 0) = (2, 0) := by
232 apply Prod.ext
233 · simp; norm_num
234 · simp
235 rw [h2] at h1
236 -- nlPUnit (2,0) = nlP 2 / 2 = (2+8)/2 = 5
237 -- nlPUnit (1,0) + nlPUnit (1,0) = 1 + 1 = 2
238 norm_num [nlPUnit, nlP, imbalance] at h1
239
240/-- **Swap-odd witness.** Continuity, swap-oddness, balance-vanishing, and unit
241normalization still leave room for a non-additive momentum (`nlPUnit`). Debit-
242credit parity is not a substitute for the kinetic condition. -/
243theorem nlPUnit_package :
244 Continuous nlPUnit ∧ SwapOdd nlPUnit ∧
245 (∀ z : LedgerState, Balanced z → nlPUnit z = 0) ∧
246 nlPUnit (1, 0) ^ 2 = 1 ∧
247 ¬ (∀ z w : LedgerState, nlPUnit (z + w) = nlPUnit z + nlPUnit w) :=
248 ⟨nlPUnit_continuous, nlPUnit_swap_odd, nlPUnit_balance_vanishing, nlPUnit_unit,
249 nlPUnit_not_additive⟩
250
251/-! ## §6. Sharper reduction: net-imbalance reading + 1D Cauchy -/
252
253/-- **Net-imbalance reading.** The momentum depends only on the net charge:
254cancelling a balanced debit-credit pair leaves the observable unchanged.
255Equivalent form: `p z = p (imbalance z, 0)`. -/
256def ReadsNetImbalance (p : LedgerState → ℝ) : Prop :=
257 ∀ z : LedgerState, p z = p (imbalance z, 0)
258
259/-- 1D additivity of `p` along the pure-debit axis. -/
260def AdditiveOnDebitAxis (p : LedgerState → ℝ) : Prop :=
261 ∀ m n : ℝ, p (m, 0) + p (n, 0) = p (m + n, 0)
262
263/-- Under net-imbalance reading and 1D additivity, balance-vanishing is derived. -/
264theorem balance_vanishing_of_net_imbalance_reading
265 {p : LedgerState → ℝ} (hread : ReadsNetImbalance p)
266 (hadd1 : AdditiveOnDebitAxis p) :
267 ∀ z : LedgerState, Balanced z → p z = 0 := by
268 intro z hz
269 have himb : imbalance z = 0 := sub_eq_zero.mpr hz
270 have h0 : p (0, 0) = 0 := by
271 have h := hadd1 0 0
272 simp only [add_zero] at h
273 linarith
274 rw [hread, himb]
275 exact h0
276
277/-- Continuous additive maps `ℝ → ℝ` are multiplication by the value at `1`. -/
278private theorem continuous_additive_real
279 (f : ℝ → ℝ) (hadd : ∀ m n : ℝ, f (m + n) = f m + f n) (hcont : Continuous f) :
280 ∀ m : ℝ, f m = m * f 1 := by
281 have hzero : f 0 = 0 := by
282 have h := hadd 0 0
283 simp only [add_zero] at h
284 linarith
285 let F : ℝ →+ ℝ :=
286 { toFun := f, map_zero' := hzero, map_add' := hadd }
287 let L : ℝ →ₗ[ℝ] ℝ := F.toRealLinearMap hcont
288 intro m
289 have hL : L m = f m := rfl
290 have h1 : L 1 = f 1 := rfl
291 calc f m = L m := hL.symm
292 _ = m • L 1 := by rw [← map_smul]; simp
293 _ = m * f 1 := by rw [h1, smul_eq_mul]
294
295/-- **The sharper discharge.** Net-imbalance reading, 1D debit-axis additivity,
296continuity, and unit normalization force `p = ± imbalance`, hence full
297consolidation additivity and `EnergyEqualsCost`. No kinetic hypothesis. -/
298theorem energyEqualsCost_of_net_imbalance_reading_additive_unit
299 (p : LedgerState → ℝ)
300 (hread : ReadsNetImbalance p)
301 (hadd1 : AdditiveOnDebitAxis p)
302 (hcont : Continuous p)
303 (hunit : p (1, 0) ^ 2 = 1) :
304 (∀ z w : LedgerState, p (z + w) = p z + p w) ∧
305 (∀ z : LedgerState, Balanced z → p z = 0) ∧
306 EnergyEqualsCost p := by
307 let f : ℝ → ℝ := fun m => p (m, 0)
308 have hfadd : ∀ m n : ℝ, f (m + n) = f m + f n := fun m n => (hadd1 m n).symm
309 have hfcont : Continuous f := by
310 have hpath : Continuous fun m : ℝ => ((m, (0 : ℝ)) : LedgerState) :=
311 Continuous.prodMk continuous_id continuous_const
312 exact hcont.comp hpath
313 have hfform := continuous_additive_real f hfadd hfcont
314 have hform : ∀ z : LedgerState, p z = p (1, 0) * imbalance z := by
315 intro z
316 calc p z = p (imbalance z, 0) := hread z
317 _ = f (imbalance z) := rfl
318 _ = imbalance z * f 1 := hfform (imbalance z)
319 _ = p (1, 0) * imbalance z := by simp [f]; ring
320 have hadd : ∀ z w : LedgerState, p (z + w) = p z + p w := by
321 intro z w
322 rw [hform (z + w), hform z, hform w, imbalance_add]
323 ring
324 have hbal := balance_vanishing_of_net_imbalance_reading hread hadd1
325 exact ⟨hadd, hbal,
326 energyEqualsCost_of_additive_continuous_balanced_unit p hadd hcont hbal hunit⟩
327
328/-- The imbalance itself inhabits the sharper package, so the reduction is not
329vacuous. -/
330theorem imbalance_reads_net_and_additive_on_axis :
331 ReadsNetImbalance imbalance ∧ AdditiveOnDebitAxis imbalance ∧
332 Continuous imbalance ∧ imbalance ((1, 0) : LedgerState) ^ 2 = 1 :=
333 ⟨fun z => by simp [imbalance],
334 fun m n => by
335 have h := imbalance_add (m, (0 : ℝ)) (n, 0)
336 -- h : imbalance ((m,0)+(n,0)) = imbalance (m,0) + imbalance (n,0)
337 have heq : ((m, (0 : ℝ)) : LedgerState) + (n, 0) = (m + n, 0) := by
338 apply Prod.ext
339 · simp
340 · simp
341 rw [heq] at h
342 exact h.symm,
343 continuous_imbalance, imbalance_unit⟩
344
345/-! ## §7. Certificate -/
346
347/-- **The additivity-attack verdict, packaged.** (b): the ambient cost satisfies
348RCL, and two companion-matching packages on this carrier disagree on
349additivity; a swap-odd unit-normalized package also fails additivity. (c):
350net-imbalance reading + 1D Cauchy + continuity + unit discharges full
351additivity and `EnergyEqualsCost`. -/
352structure MomentumAdditivityCompositionVerdict : Prop where
353 ambient_cost_satisfies_rcl : SatisfiesCompositionLaw Cost.Jcost
354 composition_law_independence :
355 SatisfiesCompositionLaw Cost.Jcost ∧
356 (Continuous imbalance ∧
357 (∀ z : LedgerState, Balanced z → imbalance z = 0) ∧
358 imbalance ((1, 0) : LedgerState) ^ 2 = 1 ∧
359 (∀ z w : LedgerState, imbalance (z + w) = imbalance z + imbalance w) ∧
360 EnergyEqualsCost imbalance) ∧
361 (Continuous (fun z : LedgerState => |imbalance z|) ∧
362 (∀ z : LedgerState, Balanced z → |imbalance z| = 0) ∧
363 (fun z : LedgerState => |imbalance z|) (1, 0) ^ 2 = 1 ∧
364 ¬ (∀ z w : LedgerState,
365 |imbalance (z + w)| = |imbalance z| + |imbalance w|))
366 swap_odd_unit_still_not_additive :
367 Continuous nlPUnit ∧ SwapOdd nlPUnit ∧
368 (∀ z : LedgerState, Balanced z → nlPUnit z = 0) ∧
369 nlPUnit (1, 0) ^ 2 = 1 ∧
370 ¬ (∀ z w : LedgerState, nlPUnit (z + w) = nlPUnit z + nlPUnit w)
371 sufficient_net_imbalance_reading :
372 ∀ p : LedgerState → ℝ, ReadsNetImbalance p → AdditiveOnDebitAxis p →
373 Continuous p → p (1, 0) ^ 2 = 1 →
374 (∀ z w : LedgerState, p (z + w) = p z + p w) ∧
375 (∀ z : LedgerState, Balanced z → p z = 0) ∧
376 EnergyEqualsCost p
377 imbalance_inhabits_sharper_package :
378 ReadsNetImbalance imbalance ∧ AdditiveOnDebitAxis imbalance ∧
379 Continuous imbalance ∧ imbalance ((1, 0) : LedgerState) ^ 2 = 1
380
381theorem momentumAdditivityCompositionVerdict :
382 MomentumAdditivityCompositionVerdict where
383 ambient_cost_satisfies_rcl := chart_cost_satisfies_composition_law
384 composition_law_independence := momentum_additivity_independent_of_composition_law
385 swap_odd_unit_still_not_additive := nlPUnit_package
386 sufficient_net_imbalance_reading :=
387 energyEqualsCost_of_net_imbalance_reading_additive_unit
388 imbalance_inhabits_sharper_package := imbalance_reads_net_and_additive_on_axis
389
390/-! ## Axiom audit -/
391
392#print axioms chart_cost_satisfies_composition_law
393#print axioms composition_law_ignores_momentum
394#print axioms imbalance_unit
395#print axioms abs_imbalance_not_additive
396#print axioms imbalance_additive_package
397#print axioms abs_imbalance_package
398#print axioms momentum_additivity_independent_of_composition_law
399#print axioms nlPUnit_continuous
400#print axioms nlPUnit_swap_odd
401#print axioms nlPUnit_not_additive
402#print axioms nlPUnit_package
403#print axioms balance_vanishing_of_net_imbalance_reading
404#print axioms energyEqualsCost_of_net_imbalance_reading_additive_unit
405#print axioms imbalance_reads_net_and_additive_on_axis
406#print axioms momentumAdditivityCompositionVerdict
407
408end
409end MomentumAdditivityComposition
410end SevenGaps
411end Gravity
412end IndisputableMonolith
413