IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity

   1import IndisputableMonolith.Gravity.SevenGaps.Gap5ChartFromLedgerMomentum
   2
   3/-!
   4# Track B, step B1: momentum additivity under ledger consolidation, a conditional closure
   5
   6**Verdict, stated first.** On the chart carrier `LedgerState := ℝ × ℝ` of
   7`Gap5ChartFromLedgerMomentum`, additivity of the momentum observable under ledger
   8consolidation is **proved from three named properties**, each shown load-bearing by
   9an exhibited countermodel in this module.  A hostile referee (2026-07-29) confirmed
  10the kernel mathematics and ruled on the framing: the first premise, the kinetic
  11condition, is pointwise `|p| = |imbalance|`, which is the magnitude half of the
  12chart conclusion itself.  So what is derived here is the *parity equivalence* —
  13additivity is swap-oddness inside the kinetic class — and what remains named is the
  14*magnitude bridge*.  This module is a conditional closure of B1, not a derivation
  15of the chart.  The three premises:
  16
  171. **the kinetic condition** `p z ^ 2 = imbalance z ^ 2`: the momentum's square is
  18   the squared net imbalance. On a split-torus orbit this follows from the
  19   exactness theorem `Jlog_eq_imbalance_sq_div_two_casimir` *composed with the
  20   energy-equals-cost identification* `p z ^ 2 = 2 * k * Jlog t` (energy is the
  21   recognition cost): the theorem gives `Jlog t = imbalance ^ 2 / (2 k)`, and the
  22   identification turns it into the kinetic condition on the orbit. That
  23   identification is declared as a hypothesis, not derived; as a global state
  24   identity the kinetic condition is a named modeling premise and the certificate
  25   says so;
  262. **continuity** of `p` (a named regularity premise);
  273. **swap-oddness** `p (z.2, z.1) = - p z`: the momentum is *odd under the
  28   substrate's own debit-credit exchange*. This is a symmetry property of the
  29   observable, and it is the premise the whole arc pivots on.
  30
  31## What is new, mathematically
  32
  33The chart module's open problem was: "why additive under consolidation", with
  34linearity banned as a premise (`chart_not_forced_without_linearity`). This module's
  35central theorem is that **within the kinetic + continuous class, additivity under
  36consolidation is *equivalent* to swap-oddness**
  37(`kinetic_root_additive_iff_swap_odd`). Extensivity of the momentum is therefore a
  38*parity under a substrate involution*, not a regularity class and not a functional
  39equation: the question "why is momentum extensive" gets the answer a substrate can
  40give, "because it is a signed charge under debit-credit exchange, not a magnitude".
  41
  42The classification behind it (`kinetic_root_classification`, with formal
  43exhaustiveness proved as `kinetic_root_mem_four`) shows a continuous kinetic
  44observable is one of exactly four functions: `± imbalance` (the signed branch,
  45additive) and `± |imbalance|` (the unsigned branch, not additive). The unsigned
  46branch is the countermodel showing swap-oddness is load-bearing; the `nlP`
  47reparametrization `m + m ^ 3` (continuous, swap-odd, balance-vanishing, not
  48kinetic, not additive) is the countermodel showing the kinetic condition is
  49load-bearing.  Stated plainly: the `nlP` family, which is the witness family of
  50`chart_not_forced_without_linearity`, is excluded here by the kinetic condition,
  51not by substrate-derived extensivity, and the kinetic condition is the magnitude
  52half of the chart conclusion.  The linearity trap is therefore not discharged by
  53this module; it is relocated.  The residual premise of the whole B1 arc is the
  54momentum-magnitude bridge `|p| = |imbalance|`, and the C2 constant-cluster attack
  55died on the same object (the chart theorem fixes the product `lam * p`, not
  56`lam`), so B1's residue and flag 12's blocker are one named target.
  57
  58## What is NOT claimed
  59
  60- A hostile referee (2026-07-29) confirmed the kernel and ruled the kinetic
  61  premise is the conclusion's magnitude half: the module stands as a conditional
  62  closure. The derived content is the parity equivalence; the magnitude bridge is
  63  the named residue, and it is shared with the cMom constant cluster (flag 12),
  64  whose Casimir route to `lam` died on the same missing bridge.
  65- The three premises are **named, not derived**. The on-orbit kinetic content is a
  66  theorem (`kinetic_on_orbit`, from the existing exactness theorem); the global
  67  kinetic condition and swap-oddness of the physical momentum are modeling
  68  premises, stated as such in the certificate. Whether "provenance derived" may
  69  rest on this named package is the flag-6 (B3) judgment, gated on hostile review.
  70- The state/event splice defect of the chart verdict is not touched: nothing here
  71  applies the event cost to a state. The kinetic condition is a property of the
  72  *observable*, stated on states, and the certificate derives it on an orbit only
  73  from the state-side exactness identity.
  74- This does not flip `gap1_provenance_derived`. It converts B1's "assume
  75  additivity" into "prove additivity from a kinetic magnitude premise, a continuity
  76  premise, and a debit-credit parity premise", with each premise shown to do work.
  77
  78## Scope
  79
  80Chart carrier only (`LedgerState`, the debit-credit plane). Nothing here is about
  81`Recognition.Ledger`, `DualEntryStrainState`, or the HKT momentum sector; the recon
  82brief (`QG/attack_full_theory_20260729/O15_attack_brief_20260729.html`) catalogs
  83why those are different carriers, and the `flux_unit` obstruction to consolidation
  84on the dual-entry type stands untouched.
  85-/
  86
  87namespace IndisputableMonolith
  88namespace Gravity
  89namespace SevenGaps
  90namespace MomentumAdditivity
  91
  92open ChartFromLedgerMomentum
  93
  94/-! ## §1. The two named properties, and imbalance arithmetic -/
  95
  96/-- **The kinetic condition.** The momentum observable's square is the squared net
  97ledger imbalance. On an orbit this is forced by the exactness of the recognition
  98cost (`kinetic_on_orbit`); as a global identity it is a named premise. -/
  99def KineticCondition (p : LedgerState → ℝ) : Prop :=
 100  ∀ z : LedgerState, p z ^ 2 = imbalance z ^ 2
 101
 102/-- **Swap-oddness.** The observable is odd under the debit-credit exchange, the
 103substrate's own involution of the ledger plane. A signed net-recognition charge has
 104this parity; an unsigned magnitude does not. -/
 105def SwapOdd (p : LedgerState → ℝ) : Prop :=
 106  ∀ z : LedgerState, p (z.2, z.1) = - p z
 107
 108theorem imbalance_swap (z : LedgerState) :
 109    imbalance (z.2, z.1) = - imbalance z := by
 110  show z.2 - z.1 = -(z.1 - z.2)
 111  ring
 112
 113theorem imbalance_add (z w : LedgerState) :
 114    imbalance (z + w) = imbalance z + imbalance w := by
 115  show z.1 + w.1 - (z.2 + w.2) = z.1 - z.2 + (w.1 - w.2)
 116  ring
 117
 118theorem imbalance_smul (t : ℝ) (z : LedgerState) :
 119    imbalance (t • z) = t * imbalance z := by
 120  show t * z.1 - t * z.2 = t * (z.1 - z.2)
 121  ring
 122
 123/-- The imbalance of a segment in the positive half-plane stays positive:
 124the half-plane is convex because `imbalance` is linear. -/
 125theorem imbalance_seg_pos {z₀ z : LedgerState} (h0 : 0 < imbalance z₀)
 126    (hz : 0 < imbalance z) {t : ℝ} (ht : t ∈ Set.Icc 0 1) :
 127    0 < imbalance ((1 - t) • z₀ + t • z) := by
 128  rw [imbalance_add, imbalance_smul, imbalance_smul]
 129  rcases Set.mem_Icc.mp ht with ⟨ht0, ht1⟩
 130  have hm : 0 < min (imbalance z₀) (imbalance z) := lt_min h0 hz
 131  have hge : min (imbalance z₀) (imbalance z)
 132      ≤ (1 - t) * imbalance z₀ + t * imbalance z := by
 133    have e1 : (1 - t) * min (imbalance z₀) (imbalance z) ≤ (1 - t) * imbalance z₀ :=
 134      mul_le_mul_of_nonneg_left (min_le_left _ _) (by linarith)
 135    have e2 : t * min (imbalance z₀) (imbalance z) ≤ t * imbalance z :=
 136      mul_le_mul_of_nonneg_left (min_le_right _ _) ht0
 137    have hsum := add_le_add e1 e2
 138    rwa [show (1 - t) * min (imbalance z₀) (imbalance z)
 139          + t * min (imbalance z₀) (imbalance z)
 140        = min (imbalance z₀) (imbalance z) from by ring] at hsum
 141  linarith
 142
 143/-- The imbalance of a segment in the negative half-plane stays negative. -/
 144theorem imbalance_seg_neg {z₀ z : LedgerState} (h0 : imbalance z₀ < 0)
 145    (hz : imbalance z < 0) {t : ℝ} (ht : t ∈ Set.Icc 0 1) :
 146    imbalance ((1 - t) • z₀ + t • z) < 0 := by
 147  rw [imbalance_add, imbalance_smul, imbalance_smul]
 148  rcases Set.mem_Icc.mp ht with ⟨ht0, ht1⟩
 149  have hm : max (imbalance z₀) (imbalance z) < 0 := max_lt h0 hz
 150  have hle : (1 - t) * imbalance z₀ + t * imbalance z
 151      ≤ max (imbalance z₀) (imbalance z) := by
 152    have e1 : (1 - t) * imbalance z₀ ≤ (1 - t) * max (imbalance z₀) (imbalance z) :=
 153      mul_le_mul_of_nonneg_left (le_max_left _ _) (by linarith)
 154    have e2 : t * imbalance z ≤ t * max (imbalance z₀) (imbalance z) :=
 155      mul_le_mul_of_nonneg_left (le_max_right _ _) ht0
 156    have hsum := add_le_add e1 e2
 157    rwa [show (1 - t) * max (imbalance z₀) (imbalance z)
 158          + t * max (imbalance z₀) (imbalance z)
 159        = max (imbalance z₀) (imbalance z) from by ring] at hsum
 160  linarith
 161
 162/-- **No sign change without a zero.** A continuous function on `[0, 1]` that is
 163never zero there cannot take opposite signs at the endpoints (the intermediate
 164value theorem, both orderings). -/
 165theorem no_sign_change_on_unit_interval {f : ℝ → ℝ}
 166    (hf : ContinuousOn f (Set.Icc 0 1))
 167    (hne : ∀ t ∈ Set.Icc (0 : ℝ) 1, f t ≠ 0) (h01 : f 0 * f 1 < 0) : False := by
 168  rcases mul_neg_iff.mp h01 with ⟨hpos, hneg⟩ | ⟨hneg, hpos⟩
 169  · have hg : ContinuousOn (fun t : ℝ => f (1 - t)) (Set.Icc 0 1) := by
 170      apply hf.comp (by fun_prop)
 171      intro t ht
 172      rcases Set.mem_Icc.mp ht with ⟨ht0, ht1⟩
 173      exact Set.mem_Icc.mpr ⟨by linarith, by linarith⟩
 174    have hmem : (0 : ℝ) ∈ Set.Icc ((fun t : ℝ => f (1 - t)) 0)
 175        ((fun t : ℝ => f (1 - t)) 1) := by
 176      simp only [sub_zero, sub_self]
 177      exact ⟨hneg.le, hpos.le⟩
 178    obtain ⟨s, hsm, hs⟩ := intermediate_value_Icc zero_le_one hg hmem
 179    have hs' : f (1 - s) = 0 := hs
 180    have hmem' : (1 - s) ∈ Set.Icc (0 : ℝ) 1 := by
 181      rcases Set.mem_Icc.mp hsm with ⟨hs0, hs1⟩
 182      exact Set.mem_Icc.mpr ⟨by linarith, by linarith⟩
 183    exact hne (1 - s) hmem' hs'
 184  · have hmem : (0 : ℝ) ∈ Set.Icc (f 0) (f 1) := ⟨hneg.le, hpos.le⟩
 185    obtain ⟨s, hsm, hs⟩ := intermediate_value_Icc zero_le_one hf hmem
 186    exact hne s hsm hs
 187
 188/-! ## §2. Sign constancy on the half-planes -/
 189
 190/-- On the positive-imbalance half-plane, a continuous kinetic `p` equals a single
 191sign times `imbalance`, the sign being `p (1, 0)`. Proof: the half-plane is convex,
 192so any deviation from the basepoint sign would, by the intermediate value theorem,
 193force `p` through zero at a point where `imbalance ≠ 0`, contradicting the kinetic
 194condition. -/
 195theorem sign_const_pos {p : LedgerState → ℝ} (hcont : Continuous p)
 196    (hkin : KineticCondition p) {z : LedgerState} (hz : 0 < imbalance z) :
 197    p z = p (1, 0) * imbalance z := by
 198  have hε : p (1, 0) ^ 2 = 1 := by
 199    have h := hkin (1, 0)
 200    have hi : imbalance (1, 0) = 1 := by simp [imbalance]
 201    rw [hi] at h
 202    simpa using h
 203  have hbase : 0 < imbalance (1, 0) := by simp [imbalance]
 204  have hγ : Continuous fun t : ℝ => (1 - t) • (1, 0) + t • z := by fun_prop
 205  have hf : ContinuousOn (fun t : ℝ => p ((1 - t) • (1, 0) + t • z)) (Set.Icc 0 1) :=
 206    hcont.comp_continuousOn hγ.continuousOn
 207  have hne : ∀ t ∈ Set.Icc (0 : ℝ) 1,
 208      p ((1 - t) • (1, 0) + t • z) ≠ 0 := by
 209    intro t ht
 210    have hpos : 0 < imbalance ((1 - t) • (1, 0) + t • z) :=
 211      imbalance_seg_pos hbase hz ht
 212    have hsq' := hkin ((1 - t) • (1, 0) + t • z)
 213    intro h0
 214    rw [h0, show ((0:ℝ)) ^ 2 = 0 from zero_pow two_ne_zero] at hsq'
 215    have hsp : (0:ℝ) < imbalance ((1 - t) • (1, 0) + t • z) ^ 2 :=
 216      sq_pos_of_ne_zero (ne_of_gt hpos)
 217    linarith
 218  have h0eq : p ((1 - (0:ℝ)) • (1, 0) + (0:ℝ) • z) = p (1, 0) := by
 219    simp
 220  have h1eq : p ((1 - (1:ℝ)) • (1, 0) + (1:ℝ) • z) = p z := by
 221    simp
 222  rcases sq_eq_sq_iff_eq_or_eq_neg.mp (hkin z) with h | h <;>
 223    rcases sq_eq_one_iff.mp hε with h1 | h1
 224  · rw [h1, one_mul]
 225    exact h
 226  · exfalso
 227    refine no_sign_change_on_unit_interval hf hne ?_
 228    rw [h0eq, h1eq, h1, h]
 229    nlinarith [hz]
 230  · exfalso
 231    refine no_sign_change_on_unit_interval hf hne ?_
 232    rw [h0eq, h1eq, h1, h]
 233    nlinarith [hz]
 234  · rw [h1, h]
 235    ring
 236
 237/-- On the negative-imbalance half-plane, a continuous kinetic `p` equals
 238`- p (0, 1)` times `imbalance`, by the same convexity argument from the basepoint
 239`(0, 1)`. -/
 240theorem sign_const_neg {p : LedgerState → ℝ} (hcont : Continuous p)
 241    (hkin : KineticCondition p) {z : LedgerState} (hz : imbalance z < 0) :
 242    p z = - p (0, 1) * imbalance z := by
 243  have hε : p (0, 1) ^ 2 = 1 := by
 244    have h := hkin (0, 1)
 245    have hi : imbalance (0, 1) = -1 := by simp [imbalance]
 246    rw [hi] at h
 247    simpa using h
 248  have hbase : imbalance (0, 1) < 0 := by simp [imbalance]
 249  have hγ : Continuous fun t : ℝ => (1 - t) • (0, 1) + t • z := by fun_prop
 250  have hf : ContinuousOn (fun t : ℝ => p ((1 - t) • (0, 1) + t • z)) (Set.Icc 0 1) :=
 251    hcont.comp_continuousOn hγ.continuousOn
 252  have hne : ∀ t ∈ Set.Icc (0 : ℝ) 1,
 253      p ((1 - t) • (0, 1) + t • z) ≠ 0 := by
 254    intro t ht
 255    have hneg : imbalance ((1 - t) • (0, 1) + t • z) < 0 :=
 256      imbalance_seg_neg hbase hz ht
 257    have hsq' := hkin ((1 - t) • (0, 1) + t • z)
 258    intro h0
 259    rw [h0, show ((0:ℝ)) ^ 2 = 0 from zero_pow two_ne_zero] at hsq'
 260    have hsp : (0:ℝ) < imbalance ((1 - t) • (0, 1) + t • z) ^ 2 :=
 261      sq_pos_of_ne_zero (ne_of_lt hneg)
 262    linarith
 263  have h0eq : p ((1 - (0:ℝ)) • (0, 1) + (0:ℝ) • z) = p (0, 1) := by
 264    simp
 265  have h1eq : p ((1 - (1:ℝ)) • (0, 1) + (1:ℝ) • z) = p z := by
 266    simp
 267  have hbase_eval : p z = - p (0, 1) * imbalance z ∨
 268      False := by
 269    rcases sq_eq_sq_iff_eq_or_eq_neg.mp (hkin z) with h | h <;>
 270      rcases sq_eq_one_iff.mp hε with h1 | h1
 271    · -- p z = imbalance z with p (0,1) = 1: sign change, excluded
 272      refine Or.inr ?_
 273      refine no_sign_change_on_unit_interval hf hne ?_
 274      rw [h0eq, h1eq, h1, h]
 275      nlinarith [hz]
 276    · -- p z = imbalance z = -(-1) * imbalance z, the claim with p (0,1) = -1
 277      exact Or.inl (by rw [h1, h]; ring)
 278    · -- p z = -imbalance z = -(1) * imbalance z, the claim with p (0,1) = 1
 279      exact Or.inl (by rw [h1, h]; ring)
 280    · -- p z = -imbalance z with p (0,1) = -1: sign change, excluded
 281      refine Or.inr ?_
 282      refine no_sign_change_on_unit_interval hf hne ?_
 283      rw [h0eq, h1eq, h1, h]
 284      nlinarith [hz]
 285  rcases hbase_eval with hres | hfal
 286  · exact hres
 287  · exact hfal.elim
 288
 289/-- **Balance-vanishing is derived, not assumed.** The kinetic condition alone
 290forces the observable to vanish on the balance locus, no continuity needed. -/
 291theorem balance_vanishing_of_kinetic {p : LedgerState → ℝ} (hkin : KineticCondition p)
 292    (z : LedgerState) (hb : Balanced z) : p z = 0 := by
 293  have hi : imbalance z = 0 := sub_eq_zero.mpr hb
 294  have hsq := hkin z
 295  rw [hi] at hsq
 296  have hz2 : p z ^ 2 = 0 := by simpa using hsq
 297  exact sq_eq_zero_iff.mp hz2
 298
 299/-! ## §3. The four-member classification -/
 300
 301/-- **Classification.** A continuous kinetic observable is pinned to a sign times
 302`imbalance` on each half-plane and vanishes on the balance locus, so it is one of
 303exactly four functions: `± imbalance` (signed branch) or `± |imbalance|` (unsigned
 304branch), the four sign patterns of the two half-plane signs. -/
 305theorem kinetic_root_classification {p : LedgerState → ℝ} (hcont : Continuous p)
 306    (hkin : KineticCondition p) :
 307    p (1, 0) ^ 2 = 1 ∧ p (0, 1) ^ 2 = 1 ∧
 308    (∀ z : LedgerState, 0 < imbalance z → p z = p (1, 0) * imbalance z) ∧
 309    (∀ z : LedgerState, imbalance z < 0 → p z = - p (0, 1) * imbalance z) ∧
 310    (∀ z : LedgerState, Balanced z → p z = 0) := by
 311  have hε1 : p (1, 0) ^ 2 = 1 := by
 312    have h := hkin (1, 0)
 313    have hi : imbalance (1, 0) = 1 := by simp [imbalance]
 314    rw [hi] at h
 315    simpa using h
 316  have hε2 : p (0, 1) ^ 2 = 1 := by
 317    have h := hkin (0, 1)
 318    have hi : imbalance (0, 1) = -1 := by simp [imbalance]
 319    rw [hi] at h
 320    simpa using h
 321  refine ⟨hε1, hε2, fun z hz => sign_const_pos hcont hkin hz,
 322    fun z hz => sign_const_neg hcont hkin hz, fun z hb =>
 323    balance_vanishing_of_kinetic hkin z hb⟩
 324
 325/-- **THEOREM (exactly four continuous kinetic observables).**  The classification
 326pins the two half-plane signs to unit real numbers, and each of the four sign
 327patterns is one named function, so the continuous kinetic class is exhausted by
 328`imbalance`, `- imbalance`, `|imbalance|`, and `- |imbalance|`.  The two signed
 329functions are the additive branch (swap parity `p (0, 1) = - p (1, 0)`); the two
 330unsigned ones are the swap-even branch.  This is the formal exhaustiveness the
 331section heading advertises. -/
 332theorem kinetic_root_mem_four {p : LedgerState → ℝ} (hcont : Continuous p)
 333    (hkin : KineticCondition p) :
 334    p = imbalance ∨ p = (fun z => - imbalance z) ∨
 335      p = (fun z => |imbalance z|) ∨ p = (fun z => - |imbalance z|) := by
 336  obtain ⟨hε1, hε2, hpos, hneg, hbal⟩ := kinetic_root_classification hcont hkin
 337  have ha : p (1, 0) = 1 ∨ p (1, 0) = -1 := sq_eq_one_iff.mp hε1
 338  have hb : p (0, 1) = 1 ∨ p (0, 1) = -1 := sq_eq_one_iff.mp hε2
 339  have key : ∀ z : LedgerState,
 340      p z = if 0 ≤ imbalance z then p (1, 0) * imbalance z
 341        else - p (0, 1) * imbalance z := by
 342    intro z
 343    rcases lt_trichotomy (imbalance z) 0 with hzn | hz0 | hzp
 344    · rw [if_neg (not_le_of_gt hzn)]
 345      exact hneg z hzn
 346    · rw [if_pos (le_of_eq hz0.symm)]
 347      have hzb : Balanced z := sub_eq_zero.mp (by simpa [imbalance] using hz0)
 348      rw [hbal z hzb, hz0]
 349      simp
 350    · rw [if_pos (le_of_lt hzp)]
 351      exact hpos z hzp
 352  rcases ha with ha1 | ha1 <;> rcases hb with hb1 | hb1
 353  · refine Or.inr (Or.inr (Or.inl ?_))
 354    funext z
 355    rw [key z, ha1, hb1]
 356    by_cases hz : 0 ≤ imbalance z
 357    · rw [if_pos hz, abs_of_nonneg hz]
 358      ring
 359    · rw [if_neg hz, abs_of_neg (lt_of_not_ge hz)]
 360      ring
 361  · left
 362    funext z
 363    rw [key z, ha1, hb1]
 364    by_cases hz : 0 ≤ imbalance z
 365    · rw [if_pos hz]
 366      ring
 367    · rw [if_neg hz]
 368      ring
 369  · refine Or.inr (Or.inl ?_)
 370    funext z
 371    rw [key z, ha1, hb1]
 372    by_cases hz : 0 ≤ imbalance z
 373    · rw [if_pos hz]
 374      ring
 375    · rw [if_neg hz]
 376      ring
 377  · refine Or.inr (Or.inr (Or.inr ?_))
 378    funext z
 379    rw [key z, ha1, hb1]
 380    by_cases hz : 0 ≤ imbalance z
 381    · rw [if_pos hz, abs_of_nonneg hz]
 382      ring
 383    · rw [if_neg hz, abs_of_neg (lt_of_not_ge hz)]
 384      ring
 385
 386/-! ## §4. Extensivity is the swap parity -/
 387
 388/-- **Additivity from the signed branch.** If the two half-plane signs agree
 389through the swap (`p (0, 1) = - p (1, 0)`), then `p = p (1, 0) • imbalance`
 390globally, hence `p` is additive under consolidation. If they disagree, the
 391balanced state `(1, 1)` already refutes additivity. So within the kinetic +
 392continuous class, additivity is exactly the swap parity. -/
 393theorem kinetic_root_additive_iff {p : LedgerState → ℝ} (hcont : Continuous p)
 394    (hkin : KineticCondition p) :
 395    (∀ z w : LedgerState, p (z + w) = p z + p w) ↔ p (0, 1) = - p (1, 0) := by
 396  obtain ⟨hε1, hε2, hpos, hneg, hbal⟩ := kinetic_root_classification hcont hkin
 397  constructor
 398  · intro h
 399    have hsum := h (1, 0) (0, 1)
 400    have heq : ((1, 0) : LedgerState) + (0, 1) = (1, 1) := by
 401      apply Prod.ext <;> simp
 402    rw [heq] at hsum
 403    have h11 : p (1, 1) = 0 := hbal (1, 1) rfl
 404    rw [h11] at hsum
 405    linarith
 406  · intro h12 z w
 407    have hform : ∀ u : LedgerState, p u = p (1, 0) * imbalance u := by
 408      intro u
 409      rcases lt_trichotomy (imbalance u) 0 with hun | hue | hup
 410      · rw [hneg u hun, h12]
 411        ring
 412      · have hub : Balanced u := by
 413          have : u.1 - u.2 = 0 := by
 414            have : imbalance u = 0 := hue
 415            simpa [imbalance] using this
 416          exact sub_eq_zero.mp this
 417        rw [hbal u hub]
 418        have : imbalance u = 0 := hue
 419        simp [this]
 420      · exact hpos u hup
 421    rw [hform (z + w), hform z, hform w, imbalance_add]
 422    ring
 423
 424/-- **The headline equivalence.** Within the kinetic + continuous class, additivity
 425under ledger consolidation and oddness under the debit-credit swap are the *same
 426property*. Extensivity of the momentum is a parity under a substrate involution. -/
 427theorem kinetic_root_additive_iff_swap_odd {p : LedgerState → ℝ}
 428    (hcont : Continuous p) (hkin : KineticCondition p) :
 429    (∀ z w : LedgerState, p (z + w) = p z + p w) ↔ SwapOdd p := by
 430  rw [kinetic_root_additive_iff hcont hkin]
 431  obtain ⟨hε1, hε2, hpos, hneg, hbal⟩ := kinetic_root_classification hcont hkin
 432  constructor
 433  · intro h12 z
 434    rcases lt_trichotomy (imbalance z) 0 with hzneg | hz0 | hzpos
 435    · have hswappos : 0 < imbalance (z.2, z.1) := by
 436        rw [imbalance_swap]; linarith
 437      rw [hpos (z.2, z.1) hswappos, hneg z hzneg, imbalance_swap, h12]
 438      ring
 439    · have hzb : Balanced z := sub_eq_zero.mp (by simpa [imbalance] using hz0)
 440      have hswb : Balanced (z.2, z.1) := hzb.symm
 441      rw [hbal z hzb, hbal (z.2, z.1) hswb]
 442      ring
 443    · have hswapneg : imbalance (z.2, z.1) < 0 := by
 444        rw [imbalance_swap]; linarith
 445      rw [hneg (z.2, z.1) hswapneg, hpos z hzpos, imbalance_swap, h12]
 446      ring
 447  · intro hswap
 448    have := hswap (1, 0)
 449    exact this
 450
 451/-! ## §5. B1, derived from the named kinetic package -/
 452
 453/-- **B1, derived from the named kinetic package.** A momentum observable whose
 454square is the squared ledger imbalance (the kinetic condition, which is the
 455magnitude half of the chart conclusion and is named, not substrate-derived), that
 456is continuous, and that is odd under the substrate's debit-credit swap, is
 457**additive under ledger consolidation**, vanishes on the balance locus (derived,
 458not assumed), and is a unit sign times the imbalance coordinate (the composition
 459with the existing reduction `additive_continuous_balanced_is_imbalance`, here
 460recovered directly with the sign pinned by the classification). -/
 461theorem momentum_additivity_from_swap {p : LedgerState → ℝ}
 462    (hkin : KineticCondition p) (hcont : Continuous p) (hswap : SwapOdd p) :
 463    (∀ z w : LedgerState, p (z + w) = p z + p w) ∧
 464    (∀ z : LedgerState, Balanced z → p z = 0) ∧
 465    (∃ a : ℝ, a ^ 2 = 1 ∧ ∀ z : LedgerState, p z = a * imbalance z) := by
 466  have hadd : ∀ z w : LedgerState, p (z + w) = p z + p w :=
 467    (kinetic_root_additive_iff_swap_odd hcont hkin).2 hswap
 468  obtain ⟨hε1, hε2, hpos, hneg, hbal⟩ := kinetic_root_classification hcont hkin
 469  have h12 : p (0, 1) = - p (1, 0) := hswap (1, 0)
 470  refine ⟨hadd, hbal, p (1, 0), hε1, fun z => ?_⟩
 471  rcases lt_trichotomy (imbalance z) 0 with hzneg | hz0 | hzpos
 472  · rw [hneg z hzneg, h12]
 473    ring
 474  · have hzb : Balanced z := sub_eq_zero.mp (by simpa [imbalance] using hz0)
 475    rw [hbal z hzb]
 476    have : imbalance z = 0 := hz0
 477    simp [this]
 478  · exact hpos z hzpos
 479
 480/-- **Where the kinetic condition comes from, on an orbit.** The recognition cost
 481is exactly the squared imbalance over twice the Casimir
 482(`Jlog_eq_imbalance_sq_div_two_casimir`, existing), so a momentum whose kinetic
 483energy `p ^ 2 / (2 k)` equals the cost has the imbalance's magnitude on that orbit.
 484The global kinetic condition off-orbit is a named modeling premise; this theorem is
 485the on-orbit, derived part of it. -/
 486theorem kinetic_on_orbit (k t : ℝ) (hk : 0 < k) {p : LedgerState → ℝ}
 487    (hkinetic_energy : p (orbitPoint k t) ^ 2 = 2 * k * Cost.Jlog t) :
 488    p (orbitPoint k t) ^ 2 = imbalance (orbitPoint k t) ^ 2 := by
 489  rw [hkinetic_energy, Jlog_eq_imbalance_sq_div_two_casimir k t hk]
 490  have hk2 : (2 : ℝ) * k ≠ 0 := mul_ne_zero two_ne_zero hk.ne'
 491  field_simp
 492
 493/-! ## §6. Each premise is load-bearing -/
 494
 495/-- **The kinetic condition is load-bearing.** The `nlP` reparametrization
 496`m ↦ m + m ^ 3` (the witness family of `chart_not_forced_without_linearity`) is
 497continuous, swap-odd, and balance-vanishing, but fails the kinetic condition and is
 498not additive. Dropping the kinetic condition reopens the linearity trap; keeping it
 499is what excludes the reparametrization family. -/
 500theorem nlP_countermodel :
 501    Continuous (fun z : LedgerState => nlP (imbalance z)) ∧
 502    SwapOdd (fun z : LedgerState => nlP (imbalance z)) ∧
 503    (∀ z : LedgerState, Balanced z → nlP (imbalance z) = 0) ∧
 504    ¬ KineticCondition (fun z : LedgerState => nlP (imbalance z)) ∧
 505    ¬ (∀ z w : LedgerState,
 506        nlP (imbalance (z + w)) = nlP (imbalance z) + nlP (imbalance w)) := by
 507  have hcont : Continuous fun z : LedgerState => nlP (imbalance z) := by
 508    have hb : Continuous fun z : LedgerState => imbalance z :=
 509      continuous_fst.sub continuous_snd
 510    exact (hb.add (hb.pow 3)).congr (fun z => by simp [nlP])
 511  refine ⟨hcont, fun z => ?_, fun z hb => ?_, ?_, ?_⟩
 512  · show nlP (imbalance (z.2, z.1)) = - nlP (imbalance z)
 513    rw [imbalance_swap]
 514    simp [nlP]
 515    ring
 516  · have : imbalance z = 0 := sub_eq_zero.mpr hb
 517    simp [nlP, this]
 518  · intro h
 519    have h1 := h (1, 0)
 520    norm_num [nlP, imbalance] at h1
 521  · intro h
 522    have h1 := h (1, 0) (1, 0)
 523    have h2 : ((1, 0) : LedgerState) + (1, 0) = (2, 0) := by
 524      apply Prod.ext <;> simp <;> norm_num
 525    rw [h2] at h1
 526    norm_num [nlP, imbalance] at h1
 527
 528/-- **Swap-oddness is load-bearing.** The absolute imbalance `z ↦ |imbalance z|` is
 529continuous, kinetic, and balance-vanishing, but it is swap-*even*, hence not
 530additive: consolidating `(1, 0)` with `(0, 1)` gives the balanced state, whose
 531absolute imbalance is `0 ≠ 1 + 1`. The unsigned branch is the countermodel that
 532pins the whole arc on the swap parity. -/
 533theorem abs_countermodel :
 534    Continuous (fun z : LedgerState => |imbalance z|) ∧
 535    KineticCondition (fun z : LedgerState => |imbalance z|) ∧
 536    (∀ z : LedgerState, Balanced z → |imbalance z| = 0) ∧
 537    ¬ SwapOdd (fun z : LedgerState => |imbalance z|) ∧
 538    ¬ (∀ z w : LedgerState,
 539        |imbalance (z + w)| = |imbalance z| + |imbalance w|) := by
 540  refine ⟨(continuous_fst.sub continuous_snd).abs, fun z => sq_abs (imbalance z),
 541    fun z hb => ?_, ?_, ?_⟩
 542  · have : imbalance z = 0 := sub_eq_zero.mpr hb
 543    simp [this]
 544  · intro h
 545    have h1 := h (1, 0)
 546    norm_num [imbalance] at h1
 547  · intro h
 548    have h1 := h (1, 0) (0, 1)
 549    have heq : ((1, 0) : LedgerState) + (0, 1) = (1, 1) := by
 550      apply Prod.ext <;> simp
 551    rw [heq] at h1
 552    norm_num [imbalance] at h1
 553
 554/-! ## §7. The certificate -/
 555
 556/-- **The B1 verdict, packaged: a conditional closure.**  Additivity is proved
 557*from the named kinetic premise*, continuity, and swap parity; each premise is
 558shown load-bearing by an exhibited countermodel.  The kinetic premise is the
 559magnitude half of the chart conclusion (`|p| = |imbalance|` pointwise), so the
 560certificate's derived content is the parity equivalence and the formal
 561exhaustiveness of the four-member class; the residual named premise is the
 562momentum-magnitude bridge, shared with the cMom constant cluster. -/
 563structure MomentumAdditivityVerdict : Prop where
 564  /-- Additivity, derived FROM the kinetic premise: kinetic + continuous +
 565  swap-odd forces additivity under ledger consolidation.  The kinetic premise is
 566  named, not substrate-derived; it is the magnitude half of the chart. -/
 567  additivity_from_kinetic_swap : ∀ p : LedgerState → ℝ, KineticCondition p →
 568    Continuous p → SwapOdd p → ∀ z w : LedgerState, p (z + w) = p z + p w
 569  /-- The composition: such a momentum is a unit sign times the imbalance
 570  coordinate. -/
 571  momentum_is_imbalance_coordinate : ∀ p : LedgerState → ℝ, KineticCondition p →
 572    Continuous p → SwapOdd p →
 573    ∃ a : ℝ, a ^ 2 = 1 ∧ ∀ z : LedgerState, p z = a * imbalance z
 574  /-- Balance-vanishing is derived from the kinetic condition, not assumed. -/
 575  balance_vanishing_derived : ∀ p : LedgerState → ℝ, KineticCondition p →
 576    ∀ z : LedgerState, Balanced z → p z = 0
 577  /-- Within the kinetic + continuous class, additivity and swap-oddness are the
 578  same property: extensivity is a parity, not a regularity class. -/
 579  additivity_iff_swap_odd : ∀ p : LedgerState → ℝ, Continuous p →
 580    KineticCondition p → ((∀ z w : LedgerState, p (z + w) = p z + p w) ↔ SwapOdd p)
 581  /-- The kinetic condition does work: the `nlP` family passes the other two
 582  premises and fails additivity. -/
 583  kinetic_is_load_bearing : Continuous (fun z : LedgerState => nlP (imbalance z)) ∧
 584    SwapOdd (fun z : LedgerState => nlP (imbalance z)) ∧
 585    (∀ z : LedgerState, Balanced z → nlP (imbalance z) = 0) ∧
 586    ¬ KineticCondition (fun z : LedgerState => nlP (imbalance z)) ∧
 587    ¬ (∀ z w : LedgerState,
 588        nlP (imbalance (z + w)) = nlP (imbalance z) + nlP (imbalance w))
 589  /-- The swap parity does work: the unsigned branch passes the other two premises
 590  and fails additivity. -/
 591  swap_is_load_bearing : Continuous (fun z : LedgerState => |imbalance z|) ∧
 592    KineticCondition (fun z : LedgerState => |imbalance z|) ∧
 593    (∀ z : LedgerState, Balanced z → |imbalance z| = 0) ∧
 594    ¬ SwapOdd (fun z : LedgerState => |imbalance z|) ∧
 595    ¬ (∀ z w : LedgerState,
 596        |imbalance (z + w)| = |imbalance z| + |imbalance w|)
 597  /-- The on-orbit kinetic content is the existing exactness theorem composed
 598  with the energy-equals-cost identification `p ^ 2 = 2 * k * Jlog`; the
 599  identification is declared in the hypothesis, not derived. -/
 600  kinetic_on_orbit_derived : ∀ (k t : ℝ), 0 < k → ∀ {p : LedgerState → ℝ},
 601    p (orbitPoint k t) ^ 2 = 2 * k * Cost.Jlog t →
 602    p (orbitPoint k t) ^ 2 = imbalance (orbitPoint k t) ^ 2
 603
 604theorem momentumAdditivityVerdict : MomentumAdditivityVerdict where
 605  additivity_from_kinetic_swap := fun p hkin hcont hswap =>
 606    (momentum_additivity_from_swap hkin hcont hswap).1
 607  momentum_is_imbalance_coordinate := fun p hkin hcont hswap =>
 608    (momentum_additivity_from_swap hkin hcont hswap).2.2
 609  balance_vanishing_derived := fun p hkin => balance_vanishing_of_kinetic hkin
 610  additivity_iff_swap_odd := fun p hcont hkin =>
 611    kinetic_root_additive_iff_swap_odd hcont hkin
 612  kinetic_is_load_bearing := nlP_countermodel
 613  swap_is_load_bearing := abs_countermodel
 614  kinetic_on_orbit_derived := fun k t hk p hke => kinetic_on_orbit k t hk hke
 615
 616/-! ## Axiom audit -/
 617
 618#print axioms imbalance_seg_pos
 619#print axioms imbalance_seg_neg
 620#print axioms no_sign_change_on_unit_interval
 621#print axioms balance_vanishing_of_kinetic
 622#print axioms sign_const_pos
 623#print axioms sign_const_neg
 624#print axioms kinetic_root_classification
 625#print axioms kinetic_root_mem_four
 626#print axioms kinetic_root_additive_iff
 627#print axioms kinetic_root_additive_iff_swap_odd
 628#print axioms momentum_additivity_from_swap
 629#print axioms kinetic_on_orbit
 630#print axioms nlP_countermodel
 631#print axioms abs_countermodel
 632#print axioms momentumAdditivityVerdict
 633
 634end MomentumAdditivity
 635end SevenGaps
 636end Gravity
 637end IndisputableMonolith
 638