IndisputableMonolith.Gravity.SevenGaps.Gap5NetImbalanceDerivation
IndisputableMonolith/Gravity/SevenGaps/Gap5NetImbalanceDerivation.lean · 343 lines · 25 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivityComposition
2
3/-!
4# Net-imbalance package from posting-level incidence
5
6**Verdict, stated first.** Of the three charged outcomes, **(c) LANDED** as the
7headline and **(b) LANDED** as the supporting no-go; **(a) is not derived**.
8
9The consumer package waiting upstream is
10`ReadsNetImbalance` (P1) and `AdditiveOnDebitAxis` (P2), which with continuity
11and unit force full consolidation additivity and `EnergyEqualsCost`. The prior
12composition-law attack showed those two properties are not forced by ambient
13RCL plus companions, and identified P2 as the selecting property among
14P1-satisfying observables (`|imbalance|` and `nlPUnit` pass P1, fail P2).
15
16This module imports the next layer of ledger posting structure beyond the
17composition law: **column posting incidence** (a state's momentum is the sum of
18its pure-debit and pure-credit contributions). That structure is named, not
19derived from σ = 0 or from RCL. Under incidence together with debit-credit
20parity (`SwapOdd`), P1 and P2 become equivalent, so the two-property frontier
21collapses to a single 1D Cauchy obligation on the debit axis. Sufficiency
22through the existing consumer is kernel-checked both ways.
23
24The same incidence layer does **not** by itself force that Cauchy obligation:
25the cube-difference observable `z ↦ z.1³ − z.2³` is continuous, swap-odd,
26balance-vanishing, unit-normalized, and column-incident, yet fails both P1 and
27P2. Scope (per `L-qg-witness-is-not-a-class-20260729`): that is a concrete
28package witness on the stated `LedgerState` carrier, not a class theorem.
29
30## What is NOT claimed
31
32* No flag flip. Flags 6 and 12 still rest on `EnergyEqualsCost`; the remaining
33 named input is 1D debit-axis additivity (equivalently P1) under posting
34 incidence and swap-oddness.
35* Column posting incidence is a named posting-level hypothesis, not a theorem
36 of the symplectic or RCL modules. Deriving it from deeper substrate structure
37 is OPEN and is the natural next attack if the 1D Cauchy side closes first.
38* B1's kinetic-conditional additivity is neither used nor strengthened.
39-/
40
41namespace IndisputableMonolith
42namespace Gravity
43namespace SevenGaps
44namespace NetImbalanceDerivation
45
46open ChartFromLedgerMomentum MomentumAdditivity MomentumAdditivityComposition
47open MomentumMagnitudeBridge EnergyEqualsCostDerivation
48
49noncomputable section
50
51/-! ## §0. Posting-level column incidence -/
52
53/-- **Column posting incidence.** The momentum of a mixed debit-credit state is
54the sum of the pure-debit contribution and the pure-credit contribution. This
55is the posting-level claim that the two columns contribute independently; it is
56strictly beyond the recognition composition law (which never mentions a
57momentum observable). -/
58def PostingIncidence (p : LedgerState → ℝ) : Prop :=
59 ∀ d c : ℝ, p (d, c) = p (d, 0) + p (0, c)
60
61/-- Under debit-credit swap-oddness, a pure credit is the negation of the
62matching pure debit. -/
63theorem axisOdd_of_swapOdd {p : LedgerState → ℝ} (hswap : SwapOdd p) :
64 ∀ n : ℝ, p (0, n) = - p (n, 0) := by
65 intro n
66 simpa using hswap (n, (0 : ℝ))
67
68/-- The ledger state decomposes as a pure-debit net charge plus a balanced
69offset: `z = (imbalance z, 0) + (z.2, z.2)`. -/
70theorem state_eq_netDebit_plus_balanced (z : LedgerState) :
71 z = ((imbalance z, (0 : ℝ)) : LedgerState) + (z.2, z.2) := by
72 apply Prod.ext
73 · change z.1 = (z.1 - z.2) + z.2
74 ring
75 · simp
76
77theorem balanced_snd_pair (z : LedgerState) :
78 ChartFromLedgerMomentum.Balanced ((z.2, z.2) : LedgerState) :=
79 rfl
80
81/-! ## §1. Under incidence + swap-odd, P1 ↔ P2 -/
82
83/-- From posting incidence and swap-oddness, the momentum is the difference of
84the two pure-column readings: `p (d, c) = p (d, 0) - p (c, 0)`. -/
85theorem posting_form_of_incidence_swap
86 {p : LedgerState → ℝ} (hinc : PostingIncidence p) (hswap : SwapOdd p)
87 (d c : ℝ) : p (d, c) = p (d, 0) - p (c, 0) := by
88 have haxis := axisOdd_of_swapOdd hswap
89 calc p (d, c) = p (d, 0) + p (0, c) := hinc d c
90 _ = p (d, 0) + (- p (c, 0)) := by rw [haxis c]
91 _ = p (d, 0) - p (c, 0) := by ring
92
93/-- **Equivalence of the two remaining inputs.** Under column posting incidence
94and debit-credit parity, net-imbalance reading is equivalent to 1D additivity on
95the debit axis. The two-property frontier therefore collapses to one. -/
96theorem readsNet_iff_additiveOnDebit_of_posting
97 {p : LedgerState → ℝ} (hinc : PostingIncidence p) (hswap : SwapOdd p) :
98 ReadsNetImbalance p ↔ AdditiveOnDebitAxis p := by
99 have hform := posting_form_of_incidence_swap hinc hswap
100 constructor
101 · intro hread m n
102 have himb : imbalance ((m + n, n) : LedgerState) = m := by
103 change (m + n) - n = m
104 ring
105 have h1 : p (m + n, n) = p (m, 0) := by
106 calc p (m + n, n) = p (imbalance (m + n, n), 0) := hread (m + n, n)
107 _ = p (m, 0) := by rw [himb]
108 have h2 : p (m + n, n) = p (m + n, 0) - p (n, 0) := hform (m + n) n
109 linarith
110 · intro hadd1 z
111 have hdiff : ∀ a b : ℝ, p (a, 0) - p (b, 0) = p (a - b, 0) := by
112 intro a b
113 have h := hadd1 (a - b) b
114 have hab : (a - b + b : ℝ) = a := by ring
115 rw [hab] at h
116 linarith
117 calc p z = p (z.1, z.2) := rfl
118 _ = p (z.1, 0) - p (z.2, 0) := hform z.1 z.2
119 _ = p (z.1 - z.2, 0) := hdiff z.1 z.2
120 _ = p (imbalance z, 0) := rfl
121
122/-! ## §2. Sufficiency: incidence + swap + one of P1/P2 discharges EEC -/
123
124/-- Under posting incidence and swap-oddness, debit-axis additivity, continuity,
125and unit normalization force full consolidation additivity, derived
126balance-vanishing, and `EnergyEqualsCost`. No kinetic hypothesis. -/
127theorem energyEqualsCost_of_posting_incidence_additive_unit
128 (p : LedgerState → ℝ)
129 (hinc : PostingIncidence p)
130 (hswap : SwapOdd p)
131 (hadd1 : AdditiveOnDebitAxis p)
132 (hcont : Continuous p)
133 (hunit : p (1, 0) ^ 2 = 1) :
134 (∀ z w : LedgerState, p (z + w) = p z + p w) ∧
135 (∀ z : LedgerState, ChartFromLedgerMomentum.Balanced z → p z = 0) ∧
136 MomentumMagnitudeBridge.EnergyEqualsCost p := by
137 have hread : ReadsNetImbalance p :=
138 (readsNet_iff_additiveOnDebit_of_posting hinc hswap).mpr hadd1
139 exact energyEqualsCost_of_net_imbalance_reading_additive_unit p hread hadd1 hcont hunit
140
141/-- Symmetric form: net-imbalance reading in place of debit-axis additivity. -/
142theorem energyEqualsCost_of_posting_incidence_readsNet_unit
143 (p : LedgerState → ℝ)
144 (hinc : PostingIncidence p)
145 (hswap : SwapOdd p)
146 (hread : ReadsNetImbalance p)
147 (hcont : Continuous p)
148 (hunit : p (1, 0) ^ 2 = 1) :
149 (∀ z w : LedgerState, p (z + w) = p z + p w) ∧
150 (∀ z : LedgerState, ChartFromLedgerMomentum.Balanced z → p z = 0) ∧
151 MomentumMagnitudeBridge.EnergyEqualsCost p := by
152 have hadd1 : AdditiveOnDebitAxis p :=
153 (readsNet_iff_additiveOnDebit_of_posting hinc hswap).mp hread
154 exact energyEqualsCost_of_net_imbalance_reading_additive_unit p hread hadd1 hcont hunit
155
156/-! ## §3. Inhabitation: imbalance sits in the posting package -/
157
158theorem imbalance_posting_incidence : PostingIncidence imbalance := by
159 intro d c
160 change d - c = (d - 0) + (0 - c)
161 ring
162
163theorem imbalance_swap_odd : SwapOdd imbalance := by
164 intro z
165 change z.2 - z.1 = -(z.1 - z.2)
166 ring
167
168theorem imbalance_inhabits_posting_package :
169 PostingIncidence imbalance ∧ SwapOdd imbalance ∧
170 ReadsNetImbalance imbalance ∧ AdditiveOnDebitAxis imbalance ∧
171 Continuous imbalance ∧ imbalance ((1, 0) : LedgerState) ^ 2 = 1 :=
172 ⟨imbalance_posting_incidence, imbalance_swap_odd,
173 imbalance_reads_net_and_additive_on_axis.1,
174 imbalance_reads_net_and_additive_on_axis.2.1,
175 imbalance_reads_net_and_additive_on_axis.2.2.1,
176 imbalance_reads_net_and_additive_on_axis.2.2.2⟩
177
178/-! ## §4. No-go: incidence + swap + companions do not force P1/P2 -/
179
180/-- Cube-difference observable: column-separable and swap-odd, but not a
181function of net imbalance alone. -/
182def cubeDiff (z : LedgerState) : ℝ := z.1 ^ 3 - z.2 ^ 3
183
184theorem cubeDiff_posting_incidence : PostingIncidence cubeDiff := by
185 intro d c
186 change d ^ 3 - c ^ 3 = (d ^ 3 - (0 : ℝ) ^ 3) + ((0 : ℝ) ^ 3 - c ^ 3)
187 ring
188
189theorem cubeDiff_swap_odd : SwapOdd cubeDiff := by
190 intro z
191 change z.2 ^ 3 - z.1 ^ 3 = -(z.1 ^ 3 - z.2 ^ 3)
192 ring
193
194theorem cubeDiff_continuous : Continuous cubeDiff :=
195 (continuous_fst.pow 3).sub (continuous_snd.pow 3)
196
197theorem cubeDiff_balance_vanishing :
198 ∀ z : LedgerState, ChartFromLedgerMomentum.Balanced z → cubeDiff z = 0 := by
199 intro z hz
200 change z.1 = z.2 at hz
201 simp [cubeDiff, hz]
202
203theorem cubeDiff_unit : cubeDiff (1, 0) ^ 2 = 1 := by
204 norm_num [cubeDiff]
205
206theorem cubeDiff_not_additiveOnDebitAxis :
207 ¬ AdditiveOnDebitAxis cubeDiff := by
208 intro h
209 have h1 := h (1 : ℝ) (1 : ℝ)
210 -- LHS: cubeDiff (1,0) + cubeDiff (1,0) = 1 + 1 = 2
211 -- RHS: cubeDiff (2,0) = 8
212 change (1 : ℝ) ^ 3 - (0 : ℝ) ^ 3 + ((1 : ℝ) ^ 3 - (0 : ℝ) ^ 3)
213 = (1 + 1 : ℝ) ^ 3 - (0 : ℝ) ^ 3 at h1
214 norm_num at h1
215
216theorem cubeDiff_not_readsNetImbalance :
217 ¬ ReadsNetImbalance cubeDiff := by
218 intro h
219 -- At z = (2, 1): cubeDiff = 7, imbalance = 1, cubeDiff (1,0) = 1
220 have h1 := h ((2, 1) : LedgerState)
221 change (2 : ℝ) ^ 3 - (1 : ℝ) ^ 3
222 = ((2 : ℝ) - (1 : ℝ)) ^ 3 - (0 : ℝ) ^ 3 at h1
223 norm_num at h1
224
225/-- **NO-GO (incidence does not select the Cauchy property).** On the stated
226`LedgerState` carrier there is a continuous, swap-odd, balance-vanishing,
227unit-normalized, column-incident momentum (`cubeDiff`) that fails both
228`ReadsNetImbalance` and `AdditiveOnDebitAxis`. Column posting incidence plus
229debit-credit parity plus the three consumer companions therefore cannot force
230the remaining 1D Cauchy input.
231
232Quantifier written first: ambient posting incidence of this concrete observable
233together with the concrete package. Not a ∀ over a class of posting systems. -/
234theorem posting_incidence_does_not_force_debit_axis_additivity :
235 PostingIncidence cubeDiff ∧ SwapOdd cubeDiff ∧
236 Continuous cubeDiff ∧
237 (∀ z : LedgerState, ChartFromLedgerMomentum.Balanced z → cubeDiff z = 0) ∧
238 cubeDiff (1, 0) ^ 2 = 1 ∧
239 ¬ AdditiveOnDebitAxis cubeDiff ∧
240 ¬ ReadsNetImbalance cubeDiff :=
241 ⟨cubeDiff_posting_incidence, cubeDiff_swap_odd, cubeDiff_continuous,
242 cubeDiff_balance_vanishing, cubeDiff_unit,
243 cubeDiff_not_additiveOnDebitAxis, cubeDiff_not_readsNetImbalance⟩
244
245/-! ## §5. Prior countermodels fail posting incidence (incidence is selecting) -/
246
247theorem abs_imbalance_not_posting_incidence :
248 ¬ PostingIncidence (fun z : LedgerState => |imbalance z|) := by
249 intro h
250 -- At (1,1): LHS = |0| = 0; RHS = |1| + |-1| = 2
251 have h1 := h (1 : ℝ) (1 : ℝ)
252 change |(1 : ℝ) - 1| = |(1 : ℝ) - 0| + |(0 : ℝ) - 1| at h1
253 norm_num at h1
254
255theorem nlPUnit_not_posting_incidence :
256 ¬ PostingIncidence nlPUnit := by
257 intro h
258 -- At (2,1): LHS = nlP(1)/2 = 1; RHS = nlP(2)/2 + nlP(-1)/2 = 5 + (-1) = 4
259 have h1 := h (2 : ℝ) (1 : ℝ)
260 simp only [nlPUnit, nlP, imbalance] at h1
261 norm_num at h1
262
263/-- Absolute imbalance and the unit-normalized nlP reparametrization both fail
264column posting incidence. Naming incidence therefore excludes the composition-
265law no-go witnesses; the remaining obstruction is the cube-difference family
266(and its continuous cousins), which fail the 1D Cauchy property. -/
267theorem prior_nogo_witnesses_fail_posting_incidence :
268 ¬ PostingIncidence (fun z : LedgerState => |imbalance z|) ∧
269 ¬ PostingIncidence nlPUnit :=
270 ⟨abs_imbalance_not_posting_incidence, nlPUnit_not_posting_incidence⟩
271
272/-! ## §6. Certificate -/
273
274/-- **The net-imbalance posting-incidence verdict.** (c): under column posting
275incidence and swap-oddness, P1 ↔ P2, and either plus continuity and unit
276discharges `EnergyEqualsCost` through the upstream consumer; imbalance inhabits
277the package. (b): incidence plus companions still admit a non-Cauchy witness
278(`cubeDiff`). (a): no derivation of P1/P2 from incidence alone. -/
279structure NetImbalanceDerivationVerdict : Prop where
280 posting_collapses_P1_P2 :
281 ∀ p : LedgerState → ℝ, PostingIncidence p → SwapOdd p →
282 (ReadsNetImbalance p ↔ AdditiveOnDebitAxis p)
283 sufficient_via_additive :
284 ∀ p : LedgerState → ℝ, PostingIncidence p → SwapOdd p →
285 AdditiveOnDebitAxis p → Continuous p → p (1, 0) ^ 2 = 1 →
286 (∀ z w : LedgerState, p (z + w) = p z + p w) ∧
287 (∀ z : LedgerState, ChartFromLedgerMomentum.Balanced z → p z = 0) ∧
288 MomentumMagnitudeBridge.EnergyEqualsCost p
289 sufficient_via_readsNet :
290 ∀ p : LedgerState → ℝ, PostingIncidence p → SwapOdd p →
291 ReadsNetImbalance p → Continuous p → p (1, 0) ^ 2 = 1 →
292 (∀ z w : LedgerState, p (z + w) = p z + p w) ∧
293 (∀ z : LedgerState, ChartFromLedgerMomentum.Balanced z → p z = 0) ∧
294 MomentumMagnitudeBridge.EnergyEqualsCost p
295 imbalance_inhabits :
296 PostingIncidence imbalance ∧ SwapOdd imbalance ∧
297 ReadsNetImbalance imbalance ∧ AdditiveOnDebitAxis imbalance ∧
298 Continuous imbalance ∧ imbalance ((1, 0) : LedgerState) ^ 2 = 1
299 incidence_does_not_force_cauchy :
300 PostingIncidence cubeDiff ∧ SwapOdd cubeDiff ∧
301 Continuous cubeDiff ∧
302 (∀ z : LedgerState, ChartFromLedgerMomentum.Balanced z → cubeDiff z = 0) ∧
303 cubeDiff (1, 0) ^ 2 = 1 ∧
304 ¬ AdditiveOnDebitAxis cubeDiff ∧
305 ¬ ReadsNetImbalance cubeDiff
306 prior_witnesses_fail_incidence :
307 ¬ PostingIncidence (fun z : LedgerState => |imbalance z|) ∧
308 ¬ PostingIncidence nlPUnit
309
310theorem netImbalanceDerivationVerdict : NetImbalanceDerivationVerdict where
311 posting_collapses_P1_P2 := fun _ hinc hswap =>
312 readsNet_iff_additiveOnDebit_of_posting hinc hswap
313 sufficient_via_additive :=
314 energyEqualsCost_of_posting_incidence_additive_unit
315 sufficient_via_readsNet :=
316 energyEqualsCost_of_posting_incidence_readsNet_unit
317 imbalance_inhabits := imbalance_inhabits_posting_package
318 incidence_does_not_force_cauchy :=
319 posting_incidence_does_not_force_debit_axis_additivity
320 prior_witnesses_fail_incidence := prior_nogo_witnesses_fail_posting_incidence
321
322/-! ## Axiom audit -/
323
324#print axioms axisOdd_of_swapOdd
325#print axioms posting_form_of_incidence_swap
326#print axioms readsNet_iff_additiveOnDebit_of_posting
327#print axioms energyEqualsCost_of_posting_incidence_additive_unit
328#print axioms energyEqualsCost_of_posting_incidence_readsNet_unit
329#print axioms imbalance_inhabits_posting_package
330#print axioms cubeDiff_not_additiveOnDebitAxis
331#print axioms cubeDiff_not_readsNetImbalance
332#print axioms posting_incidence_does_not_force_debit_axis_additivity
333#print axioms abs_imbalance_not_posting_incidence
334#print axioms nlPUnit_not_posting_incidence
335#print axioms prior_nogo_witnesses_fail_posting_incidence
336#print axioms netImbalanceDerivationVerdict
337
338end
339end NetImbalanceDerivation
340end SevenGaps
341end Gravity
342end IndisputableMonolith
343