IndisputableMonolith.Gravity.SevenGaps.Gap5EnergyEqualsCostDerivation

   1import IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumMagnitudeBridge
   2
   3/-!
   4# EnergyEqualsCost: the Hamiltonian lead is closed negatively (polarization
   5independence), and the premise discharges from exactly one extra input
   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
  11## (b) The no-go: `EnergyEqualsCost` is independent of the Hamiltonian data
  12
  13The orbit family `orbitPoint k t` is, on the stated carrier `LedgerState` with
  14the σ = 0 area form of `Cost.SymplecticAction`, exactly the Hamiltonian flow of
  15the Casimir Hamiltonian `orbitHamiltonian z = casimir z / 2`
  16(`orbitPoint_is_hamiltonian_flow`, `orbitHamiltonian_constant_on_orbit`; both
  17MODEL-tagged definitions are stated in §0 and disclosed). That Hamiltonian
  18system admits two canonical momentum observables which agree on every substrate
  19selection that is not already equivalent to the premise:
  20
  21* `imbalance`, canonically conjugate to the ledger total with bracket
  22  `{imbalance, total} = 2`, which is exactly the determinant of the chart's
  23  canonical frame (`poisson_imbalance_total_eq_frame_det`), satisfies
  24  `EnergyEqualsCost` (`energy_equals_cost_of_imbalance`, existing);
  25* the reparametrized momentum `nlP ∘ imbalance`, canonically conjugate to
  26  `nlQ` with Jacobian determinant `1` (`nl_jacobian_det_eq_one`, existing, so
  27  it is canonical with the same normalization), fails `EnergyEqualsCost`
  28  (`not_energyEqualsCost_nlP`, new).
  29
  30Both are continuous, swap-odd under the debit-credit exchange, and vanishing on
  31the balance locus (the nlP package is `nlP_countermodel`, existing). Hence
  32`EnergyEqualsCost` is **independent of the Hamiltonian data**: the symplectic
  33form, the Hamiltonian, and the orbit flow do not determine whether "the
  34momentum" satisfies the premise, because two canonical momenta of the same
  35system, passing every substrate selection short of the premise, land on
  36opposite sides of it (`energyEqualsCost_independent_of_hamiltonian_data`).
  37This closes the general Hamiltonian lead that `Gap5MomentumMagnitudeBridge`
  38left OPEN, and closes it at class level: the exhibited pair defeats any
  39argument whose only inputs are Hamiltonian structure, not any named candidate.
  40What survives the no-go, disclosed as its scope: a derivation that imports
  41*non-symplectic* structure of the ledger. §3 names the exact extra input.
  42
  43(Remark, prose only: the nlP momentum also generates a balance-locus-preserving
  44flow, since any function of the imbalance does; linearity is the only property
  45on which the two packages provably differ.)
  46
  47## (c) The sharper reduction: the premise is the linear momentum, normalized
  48
  49Three kernel-checked pieces.
  50
  511. **Pointwise cost form.** `EnergyEqualsCost p` is equivalent, on the open
  52   positive quadrant, to the pointwise identity
  53   `p z ^ 2 = 2 * casimir z * Cost.Jcost (z.1 / z.2)`
  54   (`energyEqualsCost_iff_pointwise_ratio_cost`): the momentum's square is
  55   twice the Casimir times the recognition cost of the state's own ledger
  56   ratio. Via `imbalance_sq_eq_two_casimir_jcost` this is the known
  57   equivalence with the kinetic condition, now with the cost explicit per
  58   state.
  592. **The exact discharge condition.** Additivity under ledger consolidation,
  60   continuity, balance-vanishing, and the unit normalization `p (1,0) ^ 2 = 1`
  61   together imply `EnergyEqualsCost p`
  62   (`energyEqualsCost_of_additive_continuous_balanced_unit`): the chart
  63   reduction forces `p = a • imbalance`, the normalization pins `a ^ 2 = 1`,
  64   and the existing `energy_equals_cost_of_imbalance` closes. Deriving THAT
  65   requires exactly one thing the library does not yet have: additivity of the
  66   physical momentum under consolidation (the chart successor, OPEN), since
  67   the unit normalization is the ledger-scale choice already recorded as
  68   unfixed in the HKT kinetic header. The premise's real home is the
  69   additivity lane; the Hamiltonian lane is closed by (b).
  703. **The quadrant question, answered.** The orbit route is confined to the
  71   open positive quadrant for a kernel-checked reason: `orbitPoint k t` has
  72   positive coordinates for `0 < k` (`orbitPoint_pos`, existing) and
  73   degenerates to the origin for `k ≤ 0` (`orbitPoint_eq_zero_of_nonpos`,
  74   new, since `Real.sqrt` of a nonpositive is `0`). The route extends to Q3 by
  75   the signed parameterization: every state with both coordinates negative
  76   lies on the negated orbit of its (positive) Casimir
  77   (`neg_orbit_coverage`), and there the ratio is positive and the cost
  78   reading is intact. The algebraic identity underlying everything,
  79   `imbalance z ^ 2 = 2 * casimir z * Cost.Jcost (z.1 / z.2)`, holds at every
  80   off-axis state in every quadrant (`imbalance_sq_eq_two_casimir_jcost`), so
  81   the kinetic condition itself is quadrant-free; what is confined to
  82   Q1 ∪ Q3 is the *energy-cost reading*, since on Q2/Q4 the ratio is negative
  83   and the recognition cost of the ratio is negative (`quadrant_signs`).
  84   Extending the premise to Q2/Q4 in its cost form would therefore require a
  85   premise about a negative-cost quantity, which is a different physical
  86   statement, not an orbit-coverage gap.
  87
  88## What is NOT claimed
  89
  90* No flag flip. Flags 6 and 12 still rest on `EnergyEqualsCost`; the premise
  91  is not discharged, because the one surviving input (momentum additivity) is
  92  itself open.
  93* The no-go kills derivations from Hamiltonian/symplectic data alone. It does
  94  not touch the additivity route; it redirects to it.
  95* `orbitHamiltonian` and `hamiltonianVectorField` are MODEL-tagged stated
  96  definitions (the stated Hamiltonian of the split-torus posting dynamics on
  97  the chart carrier, identity carrier map), per the charge's disclosure rule.
  98  The no-go does not depend on them being canonical choices: the exhibited
  99  counter-pair lives on the same carrier with the same area form.
 100-/
 101
 102namespace IndisputableMonolith
 103namespace Gravity
 104namespace SevenGaps
 105namespace EnergyEqualsCostDerivation
 106
 107open ChartFromLedgerMomentum MomentumAdditivity MomentumMagnitudeBridge
 108
 109noncomputable section
 110
 111/-! ## §0. The stated Hamiltonian on the stated carrier -/
 112
 113/-- **The Casimir Hamiltonian (MODEL, stated and disclosed).** On the chart
 114carrier `LedgerState` with the σ = 0 area form of `Cost.SymplecticAction`, the
 115split-torus recognition dynamics (`diagSL`) is the Hamiltonian flow of
 116`H z = casimir z / 2`. The carrier map is the identity on the chart carrier. -/
 117def orbitHamiltonian (z : LedgerState) : ℝ := casimir z / 2
 118
 119/-- **The Hamiltonian vector field of `orbitHamiltonian` (MODEL, stated).**
 120With `ω = dd ∧ dc` (the `areaForm`), `X_H = (∂H/∂c) ∂_d − (∂H/∂d) ∂_c`, which
 121for `H = d·c/2` is `(d/2, −c/2)`. -/
 122def hamiltonianVectorField (z : LedgerState) : LedgerState := (z.1 / 2, - z.2 / 2)
 123
 124/-- Poisson bracket of two coefficient-listed linear observables under the
 125ledger area form: for `f = a₁ d + b₁ c` and `g = a₂ d + b₂ c`,
 126`{f, g} = a₁ b₂ − b₁ a₂`. -/
 127def poissonLin (a₁ b₁ a₂ b₂ : ℝ) : ℝ := a₁ * b₂ - b₁ * a₂
 128
 129/-! ## §1. The orbit flow is Hamiltonian -/
 130
 131private theorem hasDerivAt_exp_half (t : ℝ) :
 132    HasDerivAt (fun s : ℝ => Real.exp (s / 2)) (Real.exp (t / 2) / 2) t := by
 133  have h : HasDerivAt (fun s : ℝ => Real.exp (s / 2)) (Real.exp (t / 2) * (1 / 2)) t :=
 134    ((hasDerivAt_id' t).div_const (2 : ℝ)).exp
 135  convert h using 1
 136  ring
 137
 138private theorem hasDerivAt_exp_neg_half (t : ℝ) :
 139    HasDerivAt (fun s : ℝ => Real.exp (-s / 2)) (- Real.exp (-t / 2) / 2) t := by
 140  have h : HasDerivAt (fun s : ℝ => Real.exp (-s / 2)) (Real.exp (-t / 2) * (-1 / 2)) t :=
 141    (((hasDerivAt_id' t).neg).div_const (2 : ℝ)).exp
 142  convert h using 1
 143  ring
 144
 145/-- **The orbit is the Hamiltonian flow of the Casimir Hamiltonian.** The time
 146derivative of `orbitPoint k t` at `t` is the Hamiltonian vector field evaluated
 147at the orbit point. -/
 148theorem orbitPoint_is_hamiltonian_flow (k t : ℝ) :
 149    HasDerivAt (fun s : ℝ => orbitPoint k s)
 150      (hamiltonianVectorField (orbitPoint k t)) t := by
 151  have h1 : HasDerivAt (fun s : ℝ => Real.sqrt k * Real.exp (s / 2))
 152      (Real.sqrt k * (Real.exp (t / 2) / 2)) t :=
 153    (hasDerivAt_exp_half t).const_mul (Real.sqrt k)
 154  have h2 : HasDerivAt (fun s : ℝ => Real.sqrt k * Real.exp (-s / 2))
 155      (Real.sqrt k * (- Real.exp (-t / 2) / 2)) t :=
 156    (hasDerivAt_exp_neg_half t).const_mul (Real.sqrt k)
 157  have hp := h1.prodMk h2
 158  have e1 : (fun s : ℝ => orbitPoint k s)
 159      = fun s => (Real.sqrt k * Real.exp (s / 2), Real.sqrt k * Real.exp (-s / 2)) :=
 160    funext fun s => rfl
 161  have c1 : (orbitPoint k t).1 / 2 = Real.sqrt k * (Real.exp (t / 2) / 2) := by
 162    show Real.sqrt k * Real.exp (t / 2) / 2 = Real.sqrt k * (Real.exp (t / 2) / 2)
 163    ring
 164  have c2 : -(orbitPoint k t).2 / 2 = Real.sqrt k * (- Real.exp (-t / 2) / 2) := by
 165    show -(Real.sqrt k * Real.exp (-t / 2)) / 2 = Real.sqrt k * (- Real.exp (-t / 2) / 2)
 166    ring
 167  have e2 : hamiltonianVectorField (orbitPoint k t)
 168      = (Real.sqrt k * (Real.exp (t / 2) / 2),
 169          Real.sqrt k * (- Real.exp (-t / 2) / 2)) := by
 170    rw [show hamiltonianVectorField (orbitPoint k t)
 171        = ((orbitPoint k t).1 / 2, -(orbitPoint k t).2 / 2) from rfl]
 172    rw [c1, c2]
 173  rw [e1, e2]
 174  exact hp
 175
 176/-- The Casimir Hamiltonian is conserved along its own flow: its value on the
 177orbit of Casimir `k` is constantly `k / 2`. -/
 178theorem orbitHamiltonian_constant_on_orbit (k t : ℝ) (hk : 0 ≤ k) :
 179    orbitHamiltonian (orbitPoint k t) = k / 2 := by
 180  rw [orbitHamiltonian, orbitPoint_casimir k t hk]
 181
 182/-! ## §2. The two canonical momenta, and the no-go -/
 183
 184/-- `{imbalance, total} = 2`: the imbalance is canonically conjugate to the
 185ledger total with normalization 2. -/
 186theorem poisson_imbalance_total : poissonLin 1 (-1) 1 1 = 2 := by
 187  norm_num [poissonLin]
 188
 189/-- The bracket normalization is exactly the canonical-frame determinant of the
 190chart module: `{imbalance, total} = det imbalanceTotalMap = 2`. -/
 191theorem poisson_imbalance_total_eq_frame_det :
 192    poissonLin 1 (-1) 1 1 = imbalanceTotalMap.det := by
 193  rw [poisson_imbalance_total, imbalanceTotalMap_det]
 194
 195/-- **The reparametrized momentum fails the premise.** Witness: the unit-Casimir
 196orbit point at `t = 2 arsinh (1/2)`, where the imbalance is `1` but
 197`nlP 1 = 2`, so the squared value `4` differs from the required `1`. -/
 198theorem not_energyEqualsCost_nlP :
 199    ¬ EnergyEqualsCost (fun z : LedgerState => nlP (imbalance z)) := by
 200  intro hE
 201  have hkin := (open_positive_kinetic_iff_energy_equals_cost).mpr hE
 202  set t₀ : ℝ := 2 * Real.arsinh (1 / 2) with ht₀
 203  have hpos := orbitPoint_pos 1 t₀ one_pos
 204  have h1 := hkin (orbitPoint 1 t₀) hpos.1 hpos.2
 205  have himb : imbalance (orbitPoint 1 t₀) = 1 := by
 206    rw [orbitPoint_imbalance, Real.sqrt_one, ht₀]
 207    rw [show (2 * Real.arsinh (1 / 2 : ℝ)) / 2 = Real.arsinh (1 / 2) from by ring,
 208      Real.sinh_arsinh]
 209    ring
 210  have hnl : nlP (1 : ℝ) = 2 := by norm_num [nlP]
 211  change nlP (imbalance (orbitPoint 1 t₀)) ^ 2 = imbalance (orbitPoint 1 t₀) ^ 2 at h1
 212  rw [himb, hnl] at h1
 213  norm_num at h1
 214
 215/-- **The imbalance package:** the canonical momentum that satisfies the
 216premise, with every substrate selection it passes. -/
 217theorem imbalance_momentum_package :
 218    Continuous imbalance ∧ SwapOdd imbalance ∧
 219      (∀ z : LedgerState, Balanced z → imbalance z = 0) ∧
 220      EnergyEqualsCost imbalance ∧ poissonLin 1 (-1) 1 1 = 2 :=
 221  ⟨continuous_imbalance, fun z => imbalance_swap z,
 222    fun z hz => show imbalance z = 0 from sub_eq_zero.mpr hz, energy_equals_cost_of_imbalance,
 223    poisson_imbalance_total⟩
 224
 225/-- **The nlP package:** the canonical momentum that fails the premise, passing
 226the same selections: continuity, swap parity, balance-vanishing, and canonical
 227status with the same normalization (Jacobian 1 on the `(imbalance, total)`
 228frame, whose own determinant is 2). -/
 229theorem nlP_momentum_package :
 230    Continuous (fun z : LedgerState => nlP (imbalance z)) ∧
 231      SwapOdd (fun z : LedgerState => nlP (imbalance z)) ∧
 232      (∀ z : LedgerState, Balanced z → nlP (imbalance z) = 0) ∧
 233      (∀ m q : ℝ, Matrix.det !![1 + 3 * m ^ 2, 0; q, 1 / (1 + 3 * m ^ 2)] = 1) ∧
 234      imbalanceTotalMap.det = 2 ∧
 235      ¬ EnergyEqualsCost (fun z : LedgerState => nlP (imbalance z)) :=
 236  ⟨nlP_countermodel.1, nlP_countermodel.2.1, nlP_countermodel.2.2.1,
 237    nl_jacobian_det_eq_one, imbalanceTotalMap_det, not_energyEqualsCost_nlP⟩
 238
 239/-- **NO-GO (polarization independence).** The ledger Hamiltonian system (the
 240σ = 0 area form, the Casimir Hamiltonian, its orbit flow) admits two canonical
 241momentum observables that agree on continuity, swap parity, balance-vanishing,
 242and canonical-momentum normalization, and disagree on `EnergyEqualsCost`. The
 243premise is therefore independent of the Hamiltonian data: no derivation whose
 244inputs are the symplectic form, the Hamiltonian, and the orbit flow alone can
 245conclude it. This knocks down the class of Hamiltonian-only derivations, not
 246any named candidate; the surviving route (non-symplectic, the ledger's linear
 247structure) is §3. -/
 248theorem energyEqualsCost_independent_of_hamiltonian_data :
 249    (Continuous imbalance ∧ SwapOdd imbalance ∧
 250      (∀ z : LedgerState, Balanced z → imbalance z = 0) ∧
 251      EnergyEqualsCost imbalance ∧ poissonLin 1 (-1) 1 1 = 2) ∧
 252    (Continuous (fun z : LedgerState => nlP (imbalance z)) ∧
 253      SwapOdd (fun z : LedgerState => nlP (imbalance z)) ∧
 254      (∀ z : LedgerState, Balanced z → nlP (imbalance z) = 0) ∧
 255      (∀ m q : ℝ, Matrix.det !![1 + 3 * m ^ 2, 0; q, 1 / (1 + 3 * m ^ 2)] = 1) ∧
 256      imbalanceTotalMap.det = 2 ∧
 257      ¬ EnergyEqualsCost (fun z : LedgerState => nlP (imbalance z))) :=
 258  ⟨imbalance_momentum_package, nlP_momentum_package⟩
 259
 260/-! ## §3. The exact discharge condition -/
 261
 262/-- **The discharge condition.** If the momentum is additive under ledger
 263consolidation, continuous, balance-vanishing, and unit-normalized
 264(`p (1,0) ^ 2 = 1`, the ledger scale), then it is a unit sign times the
 265imbalance and `EnergyEqualsCost` holds. The only open input is additivity
 266(the chart successor); the normalization is the scale choice already recorded
 267as unfixed in the HKT kinetic header. -/
 268theorem energyEqualsCost_of_additive_continuous_balanced_unit
 269    (p : LedgerState → ℝ)
 270    (hadd : ∀ z w : LedgerState, p (z + w) = p z + p w)
 271    (hcont : Continuous p)
 272    (hbal : ∀ z : LedgerState, Balanced z → p z = 0)
 273    (hunit : p (1, 0) ^ 2 = 1) :
 274    EnergyEqualsCost p := by
 275  obtain ⟨a, ha⟩ := additive_continuous_balanced_is_imbalance p hadd hcont hbal
 276  have hpa : p (1, 0) = a := by
 277    have h := ha ((1, 0) : LedgerState)
 278    rw [h]
 279    simp [imbalance]
 280  have ha2 : a ^ 2 = 1 := by
 281    rw [hpa] at hunit
 282    exact hunit
 283  intro k t hk
 284  have hE := energy_equals_cost_of_imbalance k t hk
 285  calc p (orbitPoint k t) ^ 2
 286      = (a * imbalance (orbitPoint k t)) ^ 2 := by rw [ha]
 287    _ = a ^ 2 * imbalance (orbitPoint k t) ^ 2 := by ring
 288    _ = imbalance (orbitPoint k t) ^ 2 := by rw [ha2, one_mul]
 289    _ = 2 * k * Cost.Jlog t := hE
 290
 291/-- **The pointwise cost form of the premise.** On the open positive quadrant,
 292`EnergyEqualsCost p` says state by state: the momentum's square is twice the
 293Casimir times the recognition cost of the state's own ledger ratio. -/
 294theorem energyEqualsCost_iff_pointwise_ratio_cost {p : LedgerState → ℝ} :
 295    EnergyEqualsCost p ↔
 296      ∀ z : LedgerState, 0 < z.1 → 0 < z.2 →
 297        p z ^ 2 = 2 * casimir z * Cost.Jcost (z.1 / z.2) := by
 298  constructor
 299  · intro hE z hd hc
 300    have hz := orbit_coverage z hd hc
 301    have hk : 0 < casimir z := mul_pos hd hc
 302    have h1 := hE (casimir z) (Real.log (z.1 / z.2)) hk
 303    have hJ : Cost.Jlog (Real.log (z.1 / z.2)) = Cost.Jcost (z.1 / z.2) := by
 304      show Cost.Jcost (Real.exp (Real.log (z.1 / z.2))) = Cost.Jcost (z.1 / z.2)
 305      rw [Real.exp_log (div_pos hd hc)]
 306    rw [← hz, hJ] at h1
 307    exact h1
 308  · intro hpt k t hk
 309    have hpos := orbitPoint_pos k t hk
 310    have h1 := hpt (orbitPoint k t) hpos.1 hpos.2
 311    have hratio : (orbitPoint k t).1 / (orbitPoint k t).2 = Real.exp t := by
 312      have hsk : Real.sqrt k ≠ 0 := (Real.sqrt_ne_zero').mpr hk
 313      show (Real.sqrt k * Real.exp (t / 2)) / (Real.sqrt k * Real.exp (-t / 2)) =
 314        Real.exp t
 315      rw [mul_div_mul_comm, div_self hsk, one_mul, ← Real.exp_sub]
 316      congr 1
 317      ring
 318    rw [orbitPoint_casimir k t hk.le, hratio] at h1
 319    simpa only [Cost.Jlog] using h1
 320
 321/-! ## §4. The quadrant question -/
 322
 323/-- **Why the orbit route cannot leave the positive quadrant.** For nonpositive
 324Casimir the orbit degenerates to the origin, since `Real.sqrt` of a
 325nonpositive is `0`. With `orbitPoint_pos` (positive Casimir gives positive
 326coordinates) this confines the route to the open positive quadrant. -/
 327theorem orbitPoint_eq_zero_of_nonpos {k : ℝ} (hk : k ≤ 0) (t : ℝ) :
 328    orbitPoint k t = (0, 0) := by
 329  have hsk : Real.sqrt k = 0 := (Real.sqrt_eq_zero').mpr hk
 330  simp [orbitPoint, hsk]
 331
 332/-- **Q3 is reachable by the signed orbit.** Every state with both coordinates
 333negative lies on the negated orbit of its (positive) Casimir, at the same log
 334ratio. The cost reading is intact there: the ratio is positive. -/
 335theorem neg_orbit_coverage (z : LedgerState) (hd : z.1 < 0) (hc : z.2 < 0) :
 336    z = - orbitPoint (casimir z) (Real.log (z.1 / z.2)) := by
 337  have hw := orbit_coverage (-z.1, -z.2) (neg_pos.mpr hd) (neg_pos.mpr hc)
 338  have hcas : casimir (-z.1, -z.2) = casimir z := by
 339    simp only [casimir, neg_mul_neg]
 340  have hrat : ((-z.1, -z.2) : LedgerState).1 / ((-z.1, -z.2) : LedgerState).2 =
 341      z.1 / z.2 := neg_div_neg_eq _ _
 342  rw [hcas, hrat] at hw
 343  rw [← hw]
 344  apply Prod.ext
 345  · show z.1 = - -z.1
 346    simp
 347  · show z.2 = - -z.2
 348    simp
 349
 350/-- **The master identity is quadrant-free.** At every off-axis state, the
 351squared imbalance is twice the Casimir times the recognition cost of the ledger
 352ratio. The kinetic condition has no quadrant boundary; only the energy-cost
 353reading does. -/
 354theorem imbalance_sq_eq_two_casimir_jcost (z : LedgerState)
 355    (h1 : z.1 ≠ 0) (h2 : z.2 ≠ 0) :
 356    imbalance z ^ 2 = 2 * casimir z * Cost.Jcost (z.1 / z.2) := by
 357  simp only [imbalance, casimir, Cost.Jcost]
 358  field_simp [h1, h2]
 359  ring
 360
 361/-- **Quadrant signs.** Ratio and Casimir share a sign on Q1 and Q3 (where the
 362recognition cost of the ratio is nonnegative, so the energy-cost reading is
 363natural) and are both negative-signed appropriately on Q2/Q4: there the ratio
 364is negative and the Casimir is negative, so the energy-cost reading is a
 365statement about a negative-cost quantity. -/
 366theorem quadrant_signs (z : LedgerState) :
 367    (0 < z.1 → 0 < z.2 → 0 < casimir z ∧ 0 < z.1 / z.2) ∧
 368    (z.1 < 0 → z.2 < 0 → 0 < casimir z ∧ 0 < z.1 / z.2) ∧
 369    (z.1 < 0 → 0 < z.2 → casimir z < 0 ∧ z.1 / z.2 < 0) ∧
 370    (0 < z.1 → z.2 < 0 → casimir z < 0 ∧ z.1 / z.2 < 0) :=
 371  ⟨fun h1 h2 => ⟨mul_pos h1 h2, div_pos h1 h2⟩,
 372    fun h1 h2 => ⟨mul_pos_of_neg_of_neg h1 h2, div_pos_of_neg_of_neg h1 h2⟩,
 373    fun h1 h2 => ⟨mul_neg_of_neg_of_pos h1 h2, div_neg_of_neg_of_pos h1 h2⟩,
 374    fun h1 h2 => ⟨mul_neg_of_pos_of_neg h1 h2, div_neg_of_pos_of_neg h1 h2⟩⟩
 375
 376/-! ## §5. The verdict certificate -/
 377
 378/-- **The derivation verdict, packaged.** (b): the orbit flow is the Casimir
 379Hamiltonian's flow, and the premise is independent of the Hamiltonian data by
 380the exhibited canonical counter-pair. (c): the pointwise cost form, the exact
 381discharge condition (additivity + continuity + balance + unit normalization),
 382and the quadrant answer (orbit confinement for a kernel reason, Q3 signed
 383coverage, the quadrant-free master identity, the quadrant signs). -/
 384structure EnergyEqualsCostDerivationVerdict : Prop where
 385  orbit_is_hamiltonian_flow :
 386    ∀ k t : ℝ, HasDerivAt (fun s : ℝ => orbitPoint k s)
 387      (hamiltonianVectorField (orbitPoint k t)) t
 388  hamiltonian_conserved_on_orbit :
 389    ∀ k t : ℝ, 0 ≤ k → orbitHamiltonian (orbitPoint k t) = k / 2
 390  hamiltonian_data_independence :
 391    (Continuous imbalance ∧ SwapOdd imbalance ∧
 392      (∀ z : LedgerState, Balanced z → imbalance z = 0) ∧
 393      EnergyEqualsCost imbalance ∧ poissonLin 1 (-1) 1 1 = 2) ∧
 394    (Continuous (fun z : LedgerState => nlP (imbalance z)) ∧
 395      SwapOdd (fun z : LedgerState => nlP (imbalance z)) ∧
 396      (∀ z : LedgerState, Balanced z → nlP (imbalance z) = 0) ∧
 397      (∀ m q : ℝ, Matrix.det !![1 + 3 * m ^ 2, 0; q, 1 / (1 + 3 * m ^ 2)] = 1) ∧
 398      imbalanceTotalMap.det = 2 ∧
 399      ¬ EnergyEqualsCost (fun z : LedgerState => nlP (imbalance z)))
 400  sufficient_additive_unit :
 401    ∀ p : LedgerState → ℝ,
 402      (∀ z w : LedgerState, p (z + w) = p z + p w) → Continuous p →
 403      (∀ z : LedgerState, Balanced z → p z = 0) → p (1, 0) ^ 2 = 1 →
 404      EnergyEqualsCost p
 405  premise_pointwise_cost_form :
 406    ∀ p : LedgerState → ℝ, EnergyEqualsCost p ↔
 407      ∀ z : LedgerState, 0 < z.1 → 0 < z.2 →
 408        p z ^ 2 = 2 * casimir z * Cost.Jcost (z.1 / z.2)
 409  orbit_degenerate_of_nonpos :
 410    ∀ k t : ℝ, k ≤ 0 → orbitPoint k t = (0, 0)
 411  q3_signed_orbit_coverage :
 412    ∀ z : LedgerState, z.1 < 0 → z.2 < 0 →
 413      z = - orbitPoint (casimir z) (Real.log (z.1 / z.2))
 414  off_axis_cost_identity :
 415    ∀ z : LedgerState, z.1 ≠ 0 → z.2 ≠ 0 →
 416      imbalance z ^ 2 = 2 * casimir z * Cost.Jcost (z.1 / z.2)
 417  quadrant_signs_hold :
 418    ∀ z : LedgerState,
 419      (0 < z.1 → 0 < z.2 → 0 < casimir z ∧ 0 < z.1 / z.2) ∧
 420      (z.1 < 0 → z.2 < 0 → 0 < casimir z ∧ 0 < z.1 / z.2) ∧
 421      (z.1 < 0 → 0 < z.2 → casimir z < 0 ∧ z.1 / z.2 < 0) ∧
 422      (0 < z.1 → z.2 < 0 → casimir z < 0 ∧ z.1 / z.2 < 0)
 423
 424theorem energyEqualsCostDerivationVerdict : EnergyEqualsCostDerivationVerdict where
 425  orbit_is_hamiltonian_flow := orbitPoint_is_hamiltonian_flow
 426  hamiltonian_conserved_on_orbit := orbitHamiltonian_constant_on_orbit
 427  hamiltonian_data_independence := energyEqualsCost_independent_of_hamiltonian_data
 428  sufficient_additive_unit := energyEqualsCost_of_additive_continuous_balanced_unit
 429  premise_pointwise_cost_form := fun _ => energyEqualsCost_iff_pointwise_ratio_cost
 430  orbit_degenerate_of_nonpos := fun k t hk => orbitPoint_eq_zero_of_nonpos (k := k) hk t
 431  q3_signed_orbit_coverage := neg_orbit_coverage
 432  off_axis_cost_identity := imbalance_sq_eq_two_casimir_jcost
 433  quadrant_signs_hold := quadrant_signs
 434
 435/-! ## Axiom audit -/
 436
 437#print axioms orbitPoint_is_hamiltonian_flow
 438#print axioms orbitHamiltonian_constant_on_orbit
 439#print axioms poisson_imbalance_total
 440#print axioms poisson_imbalance_total_eq_frame_det
 441#print axioms not_energyEqualsCost_nlP
 442#print axioms imbalance_momentum_package
 443#print axioms nlP_momentum_package
 444#print axioms energyEqualsCost_independent_of_hamiltonian_data
 445#print axioms energyEqualsCost_of_additive_continuous_balanced_unit
 446#print axioms energyEqualsCost_iff_pointwise_ratio_cost
 447#print axioms orbitPoint_eq_zero_of_nonpos
 448#print axioms neg_orbit_coverage
 449#print axioms imbalance_sq_eq_two_casimir_jcost
 450#print axioms quadrant_signs
 451#print axioms energyEqualsCostDerivationVerdict
 452
 453end
 454end EnergyEqualsCostDerivation
 455end SevenGaps
 456end Gravity
 457end IndisputableMonolith
 458