IndisputableMonolith.Gravity.SevenGaps.Gap5ChartFromLedgerMomentum

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.SymplecticAction
   4
   5/-!
   6# Is the half-imbalance chart derived, or stipulated? **VERDICT: STIPULATED.**
   7
   8## The verdict, stated first
   9
  10**The claim `C` below FAILED its own pre-registered criteria.** The chart is not
  11derived, and with the geometry route already closed, Pillar 1 has no surviving named
  12route by which a recognition primitive derives classical gravity.
  13
  14The four parts are all true and are all still here, kernel-clean. What failed is the
  15*attribution*, which is the fifth time in this programme that a correct theorem
  16carried a wrong attribution. Three independent defects, each verified against the
  17frozen criteria below rather than argued about:
  18
  191. **The smuggled premise, decisive.** Part 2 selects the imbalance among *linear*
  20   observables. Drop linearity and the tolerated family is infinite-dimensional:
  21   `m + m ^ 3` is a strictly monotone coordinate vanishing exactly on the balance
  22   locus, its coordinate change with `s / (1 + 3 m ^ 2)` is area-preserving so it is
  23   genuinely canonical, and the cost is not quadratic in it
  24   (`chart_not_forced_without_linearity`). Nothing in the substrate forces the
  25   momentum observable to be linear: recognition *events* are linear maps, but linear
  26   dynamics does not imply linear canonical coordinates. The frozen fail criterion
  27   "the tolerated chart family is positive-dimensional" is therefore met, and it was
  28   written down before the answer was known.
  292. **A state/event splice.** `Cost.SymplecticAction` assigns cost to an *event*:
  30   `traceCost (diagSL x) = Jcost x`. Part 4 applies the cost to a *state's* ratio.
  31   The event carrying the balanced state to `orbitPoint k t` is
  32   `diagSL (exp (t / 2))`, whose substrate cost is `Jlog (t / 2)`, not the `Jlog t`
  33   part 4 uses (`event_cost_differs_from_state_cost`). So part 1's symplectic
  34   provenance does not license part 4, and the two halves are about different
  35   objects.
  363. **No net reduction in what is assumed.** The theorems mention neither the ADM
  37   momentum `p` nor `lam`. The equation the physics still needs is
  38   `lam * p = m / (2 * sqrt k)`, which on a fixed orbit is *logically equivalent* to
  39   the chart it was supposed to derive. The gain is presentational: a transcendental
  40   stipulation becomes a linear one. Presentational gain restated as derivation is
  41   exactly what went wrong four times before, so it is recorded as a gain in
  42   exposition and not in provenance.
  43
  44Two further hits worth keeping. Part 1 is a renaming: `ConservesSigma` is *defined*
  45as `det M = 1`, so "sigma-conservation is symplectic" is a definitional unfolding.
  46And sigma-conservation does not preserve the imbalance at all, since `diagSL 2`
  47conserves it while carrying `(1,1)` to `(2, 1/2)`, so the imbalance is not the
  48sigma-privileged observable and no write-up may say it is.
  49
  50**What survives, at its honest strength.** `Jlog t = imbalance ^ 2 / (2 * casimir)`
  51is exact and true, and it is a one-line rearrangement of `J`'s definition,
  52`J (d / c) = (d - c) ^ 2 / (2 d c)`. It is a clean reformulation of the recognition
  53cost, not a derivation of anything. Anyone quoting it must say that.
  54
  55Verdict reached after a hostile cross-family read, with all three decisive
  56computations reverified independently before conceding. Frozen criteria committed at
  57`81620cd46d`, first verdict at `afb610fa84`, refutation formalized below.
  58
  59## The frozen record, unedited
  60
  61Everything from here to the end of this docstring was committed at `81620cd46d`
  62before any theorem in the file was written, so that the git history is the audit
  63trail and a reader need not trust the author
  64(`L-qg-freeze-the-candidate-before-you-price-it`). It is preserved verbatim,
  65including the parts the verdict above overturns. That is the point of freezing.
  66
  67## The question
  68
  69`HKTKineticFromRecognitionCost.exactCostKineticProfile` posts the exact
  70recognition cost of the momentum channel read in the chart
  71
  72  `t = 2 * Real.arsinh (lam * p)`,
  73
  74and in that chart the cost is exactly quadratic (`Jlog_two_arsinh`), which is the
  75premise Hojman-Kuchar-Teitelboim rigidity needs. A cross-family panel then showed
  76the clause is empty as a test of recognition, for two reasons proved in
  77`Gap5ReparamAttackOnConstraintSector`: the chart is `J`'s own inverse, so *any*
  78function quadratic in it is a multiple of `J` (`chart_alone_forces_the_cost`); and
  79the chart is **typed in as a literal**, with nothing deriving it.
  80
  81Section 4 of `HKTKineticFromRecognitionCost` proves that the rival identification
  82`t = kappa * p`, momentum linear in the log-imbalance, is *excluded*: it makes the
  83momentum response `sinh` and the algebra demands linear
  84(`no_exact_cost_kinetic_canonicalMom`). So the whole constraint-sector claim turns
  85on which of two coordinates on the same ledger is the momentum, and the repo
  86currently supplies no reason to prefer either.
  87
  88## The frozen claim under test
  89
  90`C`: **the substrate's own symplectic structure selects the half-imbalance chart,
  91because `lam * p` is the ledger's canonical momentum.**
  92
  93Concretely, the claim to be proved or refuted has four parts, in order.
  94
  951. The recognition ledger's phase space is the debit-credit plane, and
  96   sigma-conservation makes it symplectic. Already a theorem:
  97   `Cost.SymplecticAction.conservesSigma_iff_preservesArea`.
  982. On the debit-credit plane there is, up to scale, exactly **one** linear
  99   functional vanishing at the balanced ground state `(1,1)`, namely the net
 100   imbalance `m = d - c`. This selection mentions the cost nowhere.
 1013. `m` is a canonical momentum: it is symplectically conjugate to the ledger
 102   total `s = d + c`, up to a constant.
 1034. On a split-torus orbit of Casimir `d * c = k > 0` the recognition cost of the
 104   ledger ratio is **exactly** half the squared imbalance over the Casimir,
 105   `Jlog t = m ^ 2 / (2 * k)`, with no truncation. Hence
 106   `lam * p = m / (2 * sqrt k)` reproduces `exactCostKineticProfile` and the
 107   chart's free constant `lam` is the ledger scale rather than a fitted number.
 108
 109## Pass criteria, fixed in advance
 110
 111`C` passes only if all four hold, and additionally:
 112
 113- **Grep test.** A recognition primitive appears in the statement, not the
 114  motivation. Here: `Cost.Jlog` / `Cost.Jcost` and `ConservesSigma`.
 115- **Deletion test.** Removing the primitive breaks the result. Here: part 4 must
 116  fail for a cost that is not `J`.
 117- **Chart test** (`L-never-test-a-primitive-in-a-chart-built-from-it`, the test
 118  this file exists to satisfy). The coordinate must be derived independently of
 119  the primitive under test. Part 2 is the whole load: `m` is selected by linear
 120  algebra and the ground state alone, with `J` absent from the statement. If part
 121  2 needed `J`, `C` fails however pretty parts 3 and 4 are.
 122- **Reparametrization attack, run by the author before any write-up.** Exhibit
 123  the family of charts the argument still tolerates and show it is a point, not a
 124  family. Concretely: if `chi` is any increasing function fixing `0`, is
 125  `chi(m)` also selected? Part 2's linearity is what must exclude it, and the
 126  exclusion must be a theorem in this file, not a remark.
 127
 128## Fail criteria, equally fixed in advance
 129
 130`C` fails if part 2 requires the cost to select `m`; or if part 4 holds only to
 131second order rather than exactly; or if the tolerated chart family is
 132positive-dimensional. A failure closes the last named Pillar 1 provenance route
 133and is written up at equal effort, per the binding plan
 134`plans/QG_Pillar1_Provenance_Verdict_Master_Plan_20260726.html`.
 135
 136## What `C` does not decide, stated before the result is known
 137
 138Even a full pass leaves one bridge: that the ledger's canonical momentum **is**
 139the ADM momentum conjugate to the spatial metric. `C` replaces an unexplained
 140`arsinh` literal with a named identification of two momenta. That is strictly
 141better and it is not the same as closed, and no write-up of this file may say
 142otherwise. `C` also does not fix the magnitude: the Casimir `k` is free, so
 143`cKin = 2 * lam ^ 2` stays a positivity statement, exactly as the
 144`HKTKineticFromRecognitionCost` header already records.
 145-/
 146
 147namespace IndisputableMonolith
 148namespace Gravity
 149namespace SevenGaps
 150namespace ChartFromLedgerMomentum
 151
 152noncomputable section
 153
 154open Cost
 155
 156/-! ## The objects under test, defined before anything is claimed about them -/
 157
 158/-- A ledger state: a debit-credit pair. This is the phase space of
 159`Cost.SymplecticAction`, whose area form sigma-conservation preserves. -/
 160abbrev LedgerState := ℝ × ℝ
 161
 162/-- The balanced ground state: equal debit and credit, the sigma = 0 state at
 163which the recognition cost vanishes. -/
 164def balanced : LedgerState := (1, 1)
 165
 166/-- The net imbalance of a ledger state. Candidate for the ledger's canonical
 167momentum. Defined by subtraction; no cost appears. -/
 168def imbalance (z : LedgerState) : ℝ := z.1 - z.2
 169
 170/-- The ledger total. Candidate for the coordinate conjugate to the imbalance. -/
 171def total (z : LedgerState) : ℝ := z.1 + z.2
 172
 173/-- The Casimir of the split-torus action `(d, c) ↦ (x d, c / x)`: the one
 174combination every sigma-conserving diagonal event fixes. -/
 175def casimir (z : LedgerState) : ℝ := z.1 * z.2
 176
 177/-- The split-torus orbit point at log-ratio `t` and Casimir `k`: the ledger state
 178with `d / c = exp t` and `d * c = k`. The description holds only for `0 ≤ k`, since
 179`Real.sqrt` of a negative is `0` and the point degenerates to the origin; every
 180theorem below therefore carries a positivity hypothesis. -/
 181def orbitPoint (k t : ℝ) : LedgerState :=
 182  (Real.sqrt k * Real.exp (t / 2), Real.sqrt k * Real.exp (-t / 2))
 183
 184/-- A linear functional on the debit-credit plane, written by its coefficients so
 185that "linear" is a property of the data rather than a promise in a comment. -/
 186def linFunctional (a b : ℝ) (z : LedgerState) : ℝ := a * z.1 + b * z.2
 187
 188/-- The predicate part 2 is about: a linear functional vanishing at balance. The
 189recognition cost is absent from this definition, which is the point. -/
 190def VanishesAtBalanced (a b : ℝ) : Prop := linFunctional a b balanced = 0
 191
 192/-- A ledger state is balanced when its debit equals its credit. This is the
 193defining constraint of double-entry bookkeeping and it is prior to any cost: it
 194mentions no functional, no primitive, and no normalization. It is used below to
 195strengthen part 2 so that the selection of the momentum coordinate does not depend
 196on where the *cost* vanishes. -/
 197def Balanced (z : LedgerState) : Prop := z.1 = z.2
 198
 199/-! ## Part 2. The imbalance is the unique linear observable vanishing at balance
 200
 201This is the load-bearing part, and it is the one the chart test asks about
 202(`L-never-test-a-primitive-in-a-chart-built-from-it`). Nothing below mentions
 203`Jcost`, `Jlog`, or any recognition primitive: the selection is linear algebra
 204together with the location of the ground state. That is what distinguishes this
 205from the profile clause, whose coordinate was chosen so that the cost would look
 206quadratic in it. -/
 207
 208/-- A linear functional on the ledger plane vanishes at the balanced state exactly
 209when its coefficients are opposite. -/
 210theorem vanishesAtBalanced_iff (a b : ℝ) : VanishesAtBalanced a b ↔ b = -a := by
 211  unfold VanishesAtBalanced linFunctional balanced
 212  constructor
 213  · intro h; simp at h; linarith
 214  · intro h; simp [h]
 215
 216/-- **The imbalance is forced, up to scale.** Every linear observable on the
 217debit-credit plane that vanishes at the balanced ground state is a scalar multiple
 218of the net imbalance. The recognition cost appears nowhere in the hypothesis, so
 219this selection cannot be an artefact of the cost's shape. -/
 220theorem imbalance_is_the_unique_linear_selection (a b : ℝ)
 221    (h : VanishesAtBalanced a b) :
 222    ∀ z : LedgerState, linFunctional a b z = a * imbalance z := by
 223  rw [vanishesAtBalanced_iff] at h
 224  intro z
 225  simp [linFunctional, imbalance, h]
 226  ring
 227
 228/-- The imbalance is itself such an observable, so the previous theorem is not
 229vacuous. -/
 230theorem imbalance_vanishesAtBalanced : VanishesAtBalanced 1 (-1) := by
 231  simp [vanishesAtBalanced_iff]
 232
 233theorem linFunctional_one_neg_one (z : LedgerState) :
 234    linFunctional 1 (-1) z = imbalance z := by
 235  simp [linFunctional, imbalance]; ring
 236
 237/-! ### Part 2, strengthened so the ground state is not the cost's
 238
 239The version above selects the imbalance from vanishing at the single normalized
 240state `(1,1)`, which invites the objection that `(1,1)` was located by asking where
 241the recognition cost vanishes. The objection is answered by using the whole
 242double-entry balance locus `{d = c}` instead, which is the bookkeeping constraint
 243itself. The conclusion is unchanged, so nothing here depends on the normalization,
 244and the selection of the momentum coordinate is now downstream of double-entry
 245alone. -/
 246
 247/-- A linear observable vanishes on the entire balanced locus exactly when its
 248coefficients are opposite. The forward direction needs only one balanced state, but
 249the hypothesis no longer privileges any particular one. -/
 250theorem vanishesOnBalancedLocus_iff (a b : ℝ) :
 251    (∀ z : LedgerState, Balanced z → linFunctional a b z = 0) ↔ b = -a := by
 252  constructor
 253  · intro h
 254    have h1 := h (1, 1) rfl
 255    simp [linFunctional] at h1
 256    linarith
 257  · intro h z hz
 258    simp only [Balanced] at hz
 259    simp [linFunctional, h, hz]
 260
 261/-- **The imbalance is forced by double-entry alone.** Every linear observable on
 262the ledger plane that vanishes on the balanced locus is a scalar multiple of the net
 263imbalance. No cost, no primitive, and no normalization appears in the hypothesis, so
 264this is the version that satisfies the chart test without argument. -/
 265theorem imbalance_forced_by_balance_locus (a b : ℝ)
 266    (h : ∀ z : LedgerState, Balanced z → linFunctional a b z = 0) :
 267    ∀ z : LedgerState, linFunctional a b z = a * imbalance z := by
 268  rw [vanishesOnBalancedLocus_iff] at h
 269  intro z
 270  simp [linFunctional, imbalance, h]
 271  ring
 272
 273/-- **The tolerated family is one-dimensional, and its parameter is scale.** The
 274reparametrization attack, run against this file's own claim: the set of coordinates
 275part 2 admits is exactly `{a • imbalance}`, so it is a single ray rather than a
 276positive-dimensional family of charts. Compare O5, where the level-set argument
 277tolerated every increasing reparametrization fixing the rungs and therefore
 278identified nothing. The surviving scale is not a loophole that was overlooked; it
 279is the ledger scale, and it is the same freedom already recorded as unfixed in the
 280`HKTKineticFromRecognitionCost` header. -/
 281theorem tolerated_family_is_a_scale_ray :
 282    {f : LedgerState → ℝ | ∃ a b : ℝ, VanishesAtBalanced a b ∧ f = linFunctional a b}
 283      = {f : LedgerState → ℝ | ∃ a : ℝ, f = fun z => a * imbalance z} := by
 284  ext f
 285  constructor
 286  · rintro ⟨a, b, hab, rfl⟩
 287    exact ⟨a, funext (imbalance_is_the_unique_linear_selection a b hab)⟩
 288  · rintro ⟨a, rfl⟩
 289    refine ⟨a, -a, by simp [vanishesAtBalanced_iff], funext fun z => ?_⟩
 290    simp [linFunctional, imbalance]; ring
 291
 292/-! ## Part 3. The imbalance is a canonical momentum
 293
 294`Cost.SymplecticAction` proves that sigma-conservation is preservation of the
 295ledger area form. Here the imbalance-total coordinate change is shown to rescale
 296that form by a constant, which is what makes `(imbalance, total)` a canonical pair
 297up to normalization, so calling the imbalance a momentum is a statement about the
 298substrate's symplectic structure and not a naming convention. -/
 299
 300/-- The ledger state as a vector, so the area form of `Cost.SymplecticAction`
 301applies to it. -/
 302def toVec (z : LedgerState) : Fin 2 → ℝ := ![z.1, z.2]
 303
 304/-- The change of coordinates from debit-credit to imbalance-total. -/
 305def imbalanceTotalMap : Matrix (Fin 2) (Fin 2) ℝ := !![1, -1; 1, 1]
 306
 307theorem imbalanceTotalMap_apply (z : LedgerState) :
 308    imbalanceTotalMap.mulVec (toVec z) = ![imbalance z, total z] := by
 309  funext i
 310  fin_cases i <;>
 311    simp [imbalanceTotalMap, toVec, imbalance, total, Matrix.mulVec, dotProduct,
 312      Fin.sum_univ_two] <;> ring
 313
 314theorem imbalanceTotalMap_det : imbalanceTotalMap.det = 2 := by
 315  simp [imbalanceTotalMap, Matrix.det_fin_two_of]; ring
 316
 317/-- **The imbalance and the total are canonically conjugate up to a constant.**
 318The coordinate change rescales the ledger area form by exactly `2`, so it is
 319symplectic after normalization. Hence the imbalance is a momentum in the
 320substrate's own symplectic structure, the one sigma-conservation forces. -/
 321theorem imbalance_total_is_a_canonical_pair (v w : Fin 2 → ℝ) :
 322    Cost.SymplecticAction.areaForm (imbalanceTotalMap.mulVec v)
 323        (imbalanceTotalMap.mulVec w)
 324      = 2 * Cost.SymplecticAction.areaForm v w := by
 325  rw [Cost.SymplecticAction.areaForm_mulVec, imbalanceTotalMap_det]
 326
 327/-! ## Part 4. The recognition cost is exactly the squared imbalance
 328
 329No truncation, no jet, no fitted coefficient: an identity on every split-torus
 330orbit, with the Casimir supplying the normalization. -/
 331
 332/-- The recognition cost in the log-imbalance chart is twice the squared
 333half-imbalance. This is `Jlog t = cosh t - 1 = 2 sinh (t/2) ^ 2` written so that
 334the right-hand side is the object part 4 is about. -/
 335theorem Jlog_eq_two_sinh_half_sq (t : ℝ) :
 336    Cost.Jlog t = 2 * Real.sinh (t / 2) ^ 2 := by
 337  have hc : Real.cosh t = 2 * Real.sinh (t / 2) ^ 2 + 1 := by
 338    rw [show t = 2 * (t / 2) from by ring, Real.cosh_two_mul, Real.cosh_sq]
 339    ring
 340  rw [Cost.Jlog_as_cosh, hc]
 341  ring
 342
 343theorem orbitPoint_casimir (k t : ℝ) (hk : 0 ≤ k) :
 344    casimir (orbitPoint k t) = k := by
 345  have hsq : Real.sqrt k * Real.sqrt k = k := Real.mul_self_sqrt hk
 346  have hexp : Real.exp (t / 2) * Real.exp (-t / 2) = 1 := by
 347    rw [← Real.exp_add, show t / 2 + -t / 2 = (0 : ℝ) from by ring, Real.exp_zero]
 348  simp only [casimir, orbitPoint]
 349  calc Real.sqrt k * Real.exp (t / 2) * (Real.sqrt k * Real.exp (-t / 2))
 350      = (Real.sqrt k * Real.sqrt k) * (Real.exp (t / 2) * Real.exp (-t / 2)) := by ring
 351    _ = k := by rw [hsq, hexp, mul_one]
 352
 353/-- The imbalance of the orbit point is the half-imbalance sine, scaled by the
 354square root of the Casimir. -/
 355theorem orbitPoint_imbalance (k t : ℝ) :
 356    imbalance (orbitPoint k t) = Real.sqrt k * (2 * Real.sinh (t / 2)) := by
 357  simp only [imbalance, orbitPoint, Real.sinh_eq]
 358  rw [show (-t / 2 : ℝ) = -(t / 2) by ring]
 359  ring
 360
 361/-- **The recognition cost is exactly half the squared ledger imbalance.** On the
 362split-torus orbit of Casimir `k > 0`, the cost of the ledger ratio equals
 363`m ^ 2 / (2 k)` where `m` is the net imbalance of the ledger state. Exact, not a
 364second-order jet: this is the identity that the profile clause was reaching for,
 365now with its coordinate supplied by part 2 instead of typed in. -/
 366theorem Jlog_eq_imbalance_sq_div_two_casimir (k t : ℝ) (hk : 0 < k) :
 367    Cost.Jlog t = imbalance (orbitPoint k t) ^ 2 / (2 * k) := by
 368  have hsq : Real.sqrt k * Real.sqrt k = k := Real.mul_self_sqrt hk.le
 369  rw [orbitPoint_imbalance, Jlog_eq_two_sinh_half_sq]
 370  field_simp
 371  nlinarith [hsq]
 372
 373/-- The chart variable of `exactCostKineticProfile`, identified. The literal
 374`lam * p` in that profile is the ledger's net imbalance in units of twice the
 375square root of the Casimir, so the chart's free constant is the ledger scale. -/
 376theorem chart_variable_is_the_normalized_imbalance (k t : ℝ) (hk : 0 < k) :
 377    Real.sinh (t / 2) = imbalance (orbitPoint k t) / (2 * Real.sqrt k) := by
 378  have hne : Real.sqrt k ≠ 0 := by
 379    simpa using Real.sqrt_ne_zero'.mpr hk
 380  rw [orbitPoint_imbalance]
 381  field_simp
 382
 383/-- **The chart, derived.** The half-imbalance chart `t = 2 arsinh (lam * p)` is
 384exactly the statement that the momentum is the ledger's net imbalance at scale
 385`lam = 1 / (2 sqrt k)`. The `arsinh` is not a coordinate choice; it is the inverse
 386of the map from log-ratio to imbalance. -/
 387theorem chart_is_the_imbalance_coordinate (k t : ℝ) (hk : 0 < k) :
 388    t = 2 * Real.arsinh (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) := by
 389  rw [← chart_variable_is_the_normalized_imbalance k t hk, Real.arsinh_sinh]
 390  ring
 391
 392/-! ## The deletion test
 393
 394Part 2 selects the coordinate without the cost, so the chart test is satisfied by
 395construction. The deletion test is the other direction: the exactness in part 4 is
 396a property of the recognition cost and fails for a neighbouring cost. -/
 397
 398theorem sinh_two_arsinh (u : ℝ) :
 399    Real.sinh (2 * Real.arsinh u) = 2 * u * Real.sqrt (1 + u ^ 2) := by
 400  rw [Real.sinh_two_mul, Real.sinh_arsinh, Real.cosh_arsinh]
 401
 402/-- The second power cost, `x ↦ J (x ^ 2)`, in the log chart, and the nearest
 403neighbour of the recognition cost inside the power family. Correction after a hostile
 404read: this cost *does* satisfy the composition law
 405(`Gap5ReparamAttackOnConstraintSector.powCost_satisfiesCompositionLaw`) and what
 406excludes it is calibration (`isCalibrated_powCost_iff`), so an earlier version of this
 407docstring was simply wrong about which property fails. -/
 408def powTwoJlog (t : ℝ) : ℝ := Real.cosh (2 * t) - 1
 409
 410/-- **Deleting the recognition cost breaks part 4.** The second power cost is not a
 411quadratic function of the ledger imbalance: in the imbalance coordinate it is
 412quartic. So "the cost is exactly the squared imbalance" is a fact about `J` and not
 413about the coordinate, which is precisely what the profile clause could not say
 414about itself. -/
 415theorem powTwoJlog_not_quadratic_in_imbalance :
 416    ¬ ∃ C : ℝ, ∀ u : ℝ, powTwoJlog (2 * Real.arsinh u) = C * u ^ 2 := by
 417  rintro ⟨C, hC⟩
 418  have key : ∀ u : ℝ, powTwoJlog (2 * Real.arsinh u) = 8 * u ^ 2 * (1 + u ^ 2) := by
 419    intro u
 420    have hs : Real.sqrt (1 + u ^ 2) * Real.sqrt (1 + u ^ 2) = 1 + u ^ 2 :=
 421      Real.mul_self_sqrt (by positivity)
 422    have hpt : powTwoJlog (2 * Real.arsinh u) = Cost.Jlog (4 * Real.arsinh u) := by
 423      simp only [powTwoJlog, Cost.Jlog_as_cosh,
 424        show 2 * (2 * Real.arsinh u) = 4 * Real.arsinh u from by ring]
 425    rw [hpt, Jlog_eq_two_sinh_half_sq,
 426      show 4 * Real.arsinh u / 2 = 2 * Real.arsinh u from by ring, sinh_two_arsinh]
 427    nlinarith [hs]
 428  have h1 := hC 1
 429  have h2 := hC 2
 430  rw [key 1] at h1
 431  rw [key 2] at h2
 432  norm_num at h1 h2
 433  linarith
 434
 435/-! ## The refutation
 436
 437Formalized alongside the result it refutes, which is this programme's standing
 438practice for a killed attribution (the O5 counterexample is kept the same way). Two
 439defects are made into theorems here so that no future reader can restore the claim
 440by reading only the parts that worked.
 441
 442### Defect 1, decisive: linearity is doing all the work
 443
 444The referee's coordinate. `nlP` is strictly monotone and vanishes exactly on the
 445balance locus, so it is a legitimate coordinate by every criterion part 2 imposed
 446except linearity. Paired with `nlQ` the coordinate change is area-preserving, so it
 447is canonical too, and the cost is not quadratic in it. Hence part 2's selection of
 448the imbalance is an artefact of restricting to linear observables. -/
 449
 450/-- The nonlinear momentum coordinate that defeats part 2. -/
 451def nlP (m : ℝ) : ℝ := m + m ^ 3
 452
 453/-- Its area-preserving partner, so the pair is canonical and not merely a
 454relabelling of one axis. -/
 455def nlQ (m s : ℝ) : ℝ := s / (1 + 3 * m ^ 2)
 456
 457theorem nlP_factor (m : ℝ) : nlP m = m * (1 + m ^ 2) := by
 458  simp [nlP]; ring
 459
 460/-- `nlP` vanishes exactly where the imbalance does, so it respects the double-entry
 461balance locus just as the imbalance does. -/
 462theorem nlP_eq_zero_iff (m : ℝ) : nlP m = 0 ↔ m = 0 := by
 463  rw [nlP_factor, mul_eq_zero]
 464  constructor
 465  · rintro (h | h)
 466    · exact h
 467    · nlinarith [sq_nonneg m]
 468  · intro h; exact Or.inl h
 469
 470/-- `nlP` is a strictly monotone reparametrization, hence a genuine coordinate. -/
 471theorem nlP_strictMono : StrictMono nlP := by
 472  intro a b hab
 473  simp only [nlP]
 474  nlinarith [sq_nonneg (a + b), sq_nonneg (a - b), sq_nonneg a, sq_nonneg b]
 475
 476theorem nlP_hasDerivAt (m : ℝ) : HasDerivAt nlP (1 + 3 * m ^ 2) m := by
 477  have h : HasDerivAt (fun x : ℝ => x + x ^ 3) (1 + 3 * m ^ 2) m := by
 478    simpa using (hasDerivAt_id m).add ((hasDerivAt_id m).pow 3)
 479  exact h
 480
 481/-- `nlP` does not depend on the conjugate coordinate, which is why the Jacobian
 482determinant below is `1` whatever the remaining partial derivative is. -/
 483theorem nlP_hasDerivAt_snd (m s : ℝ) :
 484    HasDerivAt (fun _ : ℝ => nlP m) 0 s := hasDerivAt_const s (nlP m)
 485
 486theorem nlQ_hasDerivAt_snd (m s : ℝ) :
 487    HasDerivAt (fun y : ℝ => nlQ m y) (1 / (1 + 3 * m ^ 2)) s := by
 488  have hne : (1 : ℝ) + 3 * m ^ 2 ≠ 0 := by positivity
 489  simpa [nlQ, div_eq_mul_inv, one_div] using
 490    (hasDerivAt_id s).mul_const ((1 + 3 * m ^ 2)⁻¹)
 491
 492/-- **The nonlinear coordinate change is area-preserving.** Its Jacobian determinant
 493is `1`, with the diagonal entries supplied by `nlP_hasDerivAt` and
 494`nlQ_hasDerivAt_snd` and the upper-right entry by `nlP_hasDerivAt_snd`. The
 495determinant is `1` for *every* value of the remaining partial derivative `q`, which
 496is why that derivative never has to be computed. So `(nlP, nlQ)` is a canonical pair,
 497and the counterexample survives demanding that the momentum coordinate be
 498canonical. -/
 499theorem nl_jacobian_det_eq_one (m q : ℝ) :
 500    Matrix.det !![1 + 3 * m ^ 2, 0; q, 1 / (1 + 3 * m ^ 2)] = 1 := by
 501  have hne : (1 : ℝ) + 3 * m ^ 2 ≠ 0 := by positivity
 502  simp [Matrix.det_fin_two_of]
 503  field_simp
 504
 505/-- **The cost is not quadratic in the nonlinear coordinate.** At unit Casimir the
 506cost is `m ^ 2 / 2`, and no single constant makes that a multiple of `nlP m ^ 2`:
 507the coefficient would have to be `1 / 8` at `m = 1` and `1 / 50` at `m = 2`. -/
 508theorem cost_not_quadratic_in_nlP :
 509    ¬ ∃ C : ℝ, ∀ m : ℝ, m ^ 2 / 2 = C * nlP m ^ 2 := by
 510  rintro ⟨C, hC⟩
 511  have h1 := hC 1
 512  have h2 := hC 2
 513  simp only [nlP] at h1 h2
 514  norm_num at h1 h2
 515  linarith
 516
 517/-- **Defect 1, assembled: the chart is not forced once linearity is dropped.**
 518There is a strictly monotone coordinate, vanishing exactly on the balance locus and
 519belonging to an area-preserving pair, in which the recognition cost is not quadratic.
 520So part 2 selects the imbalance by fiat, and the frozen fail criterion "the tolerated
 521chart family is positive-dimensional" is met. This is the same failure shape as O5,
 522where the argument tolerated every increasing reparametrization fixing the rungs. -/
 523theorem chart_not_forced_without_linearity :
 524    ∃ g : ℝ → ℝ, StrictMono g ∧ (∀ m : ℝ, g m = 0 ↔ m = 0)
 525      ∧ (∀ m q : ℝ, Matrix.det !![1 + 3 * m ^ 2, 0; q, 1 / (1 + 3 * m ^ 2)] = 1)
 526      ∧ ¬ ∃ C : ℝ, ∀ m : ℝ, m ^ 2 / 2 = C * g m ^ 2 :=
 527  ⟨nlP, nlP_strictMono, nlP_eq_zero_iff, nl_jacobian_det_eq_one,
 528    cost_not_quadratic_in_nlP⟩
 529
 530/-! ### Defect 2: part 4 costs a state, part 1 costs an event
 531
 532`Cost.SymplecticAction.traceCost_diagSL` gives the cost of an *event*. The event
 533carrying the balanced state to `orbitPoint k t` is `diagSL (exp (t / 2))`, so the
 534substrate's cost of that event is `Jlog (t / 2)`. Part 4 uses `Jlog t`. They differ,
 535so the symplectic provenance imported in part 1 does not license part 4. -/
 536
 537/-- The two readings disagree, so the splice is real and not a matter of convention.
 538Witnessed at `t = 2`: the event cost is `Jlog 1` and part 4's cost is `Jlog 2`. -/
 539theorem event_cost_differs_from_state_cost : Cost.Jlog 1 ≠ Cost.Jlog 2 := by
 540  rw [Jlog_eq_two_sinh_half_sq, Jlog_eq_two_sinh_half_sq]
 541  have h0 : 0 < Real.sinh (1 / 2 : ℝ) := by
 542    have h := Real.sinh_lt_sinh.mpr (show (0 : ℝ) < 1 / 2 by norm_num)
 543    simpa using h
 544  have hlt : Real.sinh (1 / 2 : ℝ) < Real.sinh (2 / 2 : ℝ) := by
 545    apply Real.sinh_lt_sinh.mpr; norm_num
 546  intro h
 547  nlinarith [h0, hlt]
 548
 549/-- The event that carries the balanced state of Casimir `k` to `orbitPoint k t` has
 550eigenvalue `exp (t / 2)`, which is the fact that produces the mismatch above. -/
 551theorem orbitPoint_is_reached_by_event (k t : ℝ) :
 552    orbitPoint k t
 553      = (Real.exp (t / 2) * Real.sqrt k, (Real.exp (t / 2))⁻¹ * Real.sqrt k) := by
 554  simp only [orbitPoint, Prod.mk.injEq]
 555  rw [show (-t / 2 : ℝ) = -(t / 2) by ring, Real.exp_neg]
 556  exact ⟨by ring, by ring⟩
 557
 558/-! ## The successor, reduced
 559
 560The refutation above leaves exactly one repair: force linearity from the substrate. This
 561section does the cheap half of that repair honestly, by showing that **linearity is not
 562the premise actually needed**. A strictly weaker and far more physical premise suffices:
 563that the momentum observable is *additive under ledger consolidation*.
 564
 565Consolidating two double-entry ledgers is componentwise addition of debits and credits,
 566which is what aggregating accounts means, and it is the addition `LedgerState` already
 567carries. An observable that is additive under it, and continuous, is linear by Cauchy's
 568functional equation, and then part 2 forces it to be the imbalance. So the open problem
 569shrinks from "why linear", which is a regularity class and therefore the wrong kind of
 570question, to "why additive under consolidation", which is extensivity and is the kind of
 571thing a substrate can answer.
 572
 573**This is a reduction and not a closure, and the distinction is the whole lesson of this
 574module.** Additivity is a *premise* of the theorem below, not a consequence of anything
 575proved anywhere in this repository. `Foundation.JHessianGolden.additivePosting` is not
 576it: that result says the total *cost* is the sum of per-coordinate costs,
 577`Phi(x) = sum J(x i)`, which is a statement about the cost and not about any observable.
 578Reading it as the additivity below would repeat defect 2 exactly, a splice between two
 579objects that are both written as sums. Anyone continuing this line must discharge
 580additivity from the substrate, and must run the admissible-class test on whatever they
 581use to do it. -/
 582
 583/-- **The reduction: additive plus continuous plus vanishing on balance forces the
 584imbalance.** Linearity never has to be assumed. Consolidation additivity and continuity
 585give `ℝ`-linearity, and then the double-entry balance locus pins the observable to a
 586multiple of the net imbalance.
 587
 588Read the premises literally. `hadd` is additivity under the componentwise addition of
 589ledgers, which is consolidation. `hcont` is continuity. `hbal` is the double-entry
 590balance condition and mentions no cost. Nothing here is a recognition primitive, which
 591is the point: this theorem is the *conditional*, and the open problem is its
 592hypothesis. -/
 593theorem additive_continuous_balanced_is_imbalance
 594    (f : LedgerState → ℝ)
 595    (hadd : ∀ z w : LedgerState, f (z + w) = f z + f w)
 596    (hcont : Continuous f)
 597    (hbal : ∀ z : LedgerState, Balanced z → f z = 0) :
 598    ∃ a : ℝ, ∀ z : LedgerState, f z = a * imbalance z := by
 599  have hzero : f 0 = 0 := by
 600    have h := hadd 0 0
 601    simp only [add_zero] at h
 602    linarith
 603  let F : LedgerState →+ ℝ :=
 604    { toFun := f, map_zero' := hzero, map_add' := hadd }
 605  let L : LedgerState →ₗ[ℝ] ℝ := F.toRealLinearMap hcont
 606  have hLf : ∀ z : LedgerState, L z = f z := fun _ => rfl
 607  have hone : f ((1, 1) : LedgerState) = 0 := hbal (1, 1) rfl
 608  have hneg : f ((0, 1) : LedgerState) = -f ((1, 0) : LedgerState) := by
 609    have h := hadd (1, 0) (0, 1)
 610    have he : ((1, 0) : LedgerState) + ((0, 1) : LedgerState) = (1, 1) := by
 611      apply Prod.ext <;> simp
 612    rw [he, hone] at h
 613    linarith
 614  refine ⟨f (1, 0), fun z => ?_⟩
 615  have hsplit : z = z.1 • ((1, 0) : LedgerState) + z.2 • ((0, 1) : LedgerState) := by
 616    apply Prod.ext <;> simp
 617  have hL : f z = z.1 * f (1, 0) + z.2 * f (0, 1) := by
 618    rw [← hLf z]
 619    conv_lhs => rw [hsplit]
 620    rw [map_add, map_smul, map_smul, smul_eq_mul, smul_eq_mul, hLf, hLf]
 621  rw [hL, hneg, imbalance]
 622  ring
 623
 624/-- The imbalance itself satisfies all three hypotheses, so the reduction is not
 625vacuous and the conditional has at least one inhabitant. -/
 626theorem imbalance_is_additive_continuous_balanced :
 627    (∀ z w : LedgerState, imbalance (z + w) = imbalance z + imbalance w)
 628      ∧ Continuous imbalance
 629      ∧ (∀ z : LedgerState, Balanced z → imbalance z = 0) := by
 630  refine ⟨fun z w => by simp [imbalance]; ring, ?_, fun z hz => ?_⟩
 631  · exact (continuous_fst.sub continuous_snd)
 632  · simp only [Balanced] at hz
 633    simp [imbalance, hz]
 634
 635/-! ## The verdict certificate
 636
 637Every field below is a theorem of this file, and the certificate is deliberately
 638*not* named for the claim, because the claim failed. The first six fields are the
 639four frozen parts and their two tests, all true. The last two fields are the defects
 640that make the parts insufficient. A reader who wants the parts must take the defects
 641with them, which is the entire purpose of packaging them in one structure. -/
 642
 643/-- **The chart is stipulated, not derived: parts and defects together.** The four
 644frozen parts hold, and two independent defects make them insufficient for the
 645attribution. See the verdict at the top of this module for the third defect, that the
 646remaining ADM identification is logically equivalent to the chart it was to derive
 647and so is not formalizable as a gain. -/
 648structure ChartStipulatedVerdict : Prop where
 649  /-- Part 1, imported: sigma-conservation is preservation of the ledger area form. -/
 650  sigma_is_symplectic :
 651    ∀ M : Matrix (Fin 2) (Fin 2) ℝ,
 652      Cost.SymplecticAction.ConservesSigma M ↔
 653        ∀ v w : Fin 2 → ℝ,
 654          Cost.SymplecticAction.areaForm (M.mulVec v) (M.mulVec w)
 655            = Cost.SymplecticAction.areaForm v w
 656  /-- Part 2, the load-bearing one: the coordinate is selected by linear algebra
 657  and the double-entry balance locus, with no recognition primitive and no chosen
 658  normalization in the hypothesis. -/
 659  imbalance_forced :
 660    ∀ a b : ℝ, (∀ z : LedgerState, Balanced z → linFunctional a b z = 0) →
 661      ∀ z : LedgerState, linFunctional a b z = a * imbalance z
 662  /-- Part 2's reparametrization attack *within the linear class*: the tolerated
 663  family is the line of scalar multiples, including the zero functional. Note this is
 664  a line and not a ray, and it is the tolerated family only after linearity has
 665  already been assumed, which is what defect 1 below attacks. -/
 666  tolerated_linear_family_is_a_line :
 667    {f : LedgerState → ℝ | ∃ a b : ℝ, VanishesAtBalanced a b ∧ f = linFunctional a b}
 668      = {f : LedgerState → ℝ | ∃ a : ℝ, f = fun z => a * imbalance z}
 669  /-- Part 3: the imbalance is a canonical momentum. -/
 670  imbalance_is_a_momentum :
 671    ∀ v w : Fin 2 → ℝ,
 672      Cost.SymplecticAction.areaForm (imbalanceTotalMap.mulVec v)
 673          (imbalanceTotalMap.mulVec w)
 674        = 2 * Cost.SymplecticAction.areaForm v w
 675  /-- Part 4: the cost is exactly the squared imbalance over twice the Casimir. -/
 676  cost_is_squared_imbalance :
 677    ∀ k t : ℝ, 0 < k → Cost.Jlog t = imbalance (orbitPoint k t) ^ 2 / (2 * k)
 678  /-- Part 4's corollary: the stipulated chart is that coordinate. -/
 679  chart_is_derived :
 680    ∀ k t : ℝ, 0 < k →
 681      t = 2 * Real.arsinh (imbalance (orbitPoint k t) / (2 * Real.sqrt k))
 682  /-- The deletion test: a neighbouring cost fails part 4. Passing this is necessary
 683  and, as the earlier panel showed for `oscCost_not_quadratic_in_log_chart`, far from
 684  sufficient, since the chart forces the cost anyway. -/
 685  deletion_test :
 686    ¬ ∃ C : ℝ, ∀ u : ℝ, powTwoJlog (2 * Real.arsinh u) = C * u ^ 2
 687  /-- **Defect 1, decisive.** Drop linearity and the tolerated coordinate family is
 688  infinite-dimensional: there is a strictly monotone coordinate vanishing exactly on
 689  the balance locus, belonging to an area-preserving pair, in which the cost is not
 690  quadratic. -/
 691  linearity_is_load_bearing :
 692    ∃ g : ℝ → ℝ, StrictMono g ∧ (∀ m : ℝ, g m = 0 ↔ m = 0)
 693      ∧ (∀ m q : ℝ, Matrix.det !![1 + 3 * m ^ 2, 0; q, 1 / (1 + 3 * m ^ 2)] = 1)
 694      ∧ ¬ ∃ C : ℝ, ∀ m : ℝ, m ^ 2 / 2 = C * g m ^ 2
 695  /-- **Defect 2.** The symplectic module costs an event, part 4 costs a state, and
 696  the two disagree, so part 1 does not license part 4. -/
 697  state_event_splice : Cost.Jlog 1 ≠ Cost.Jlog 2
 698  /-- **The successor, as a conditional.** Linearity never needs to be assumed:
 699  additivity under ledger consolidation plus continuity plus vanishing on the balance
 700  locus already forces the imbalance. The open problem is the additivity hypothesis,
 701  which nothing in this repository currently supplies. -/
 702  reduction_to_additivity :
 703    ∀ f : LedgerState → ℝ,
 704      (∀ z w : LedgerState, f (z + w) = f z + f w) → Continuous f →
 705        (∀ z : LedgerState, Balanced z → f z = 0) →
 706          ∃ a : ℝ, ∀ z : LedgerState, f z = a * imbalance z
 707
 708theorem chartStipulatedVerdict : ChartStipulatedVerdict where
 709  sigma_is_symplectic := Cost.SymplecticAction.conservesSigma_iff_preservesArea
 710  imbalance_forced := imbalance_forced_by_balance_locus
 711  tolerated_linear_family_is_a_line := tolerated_family_is_a_scale_ray
 712  imbalance_is_a_momentum := imbalance_total_is_a_canonical_pair
 713  cost_is_squared_imbalance := Jlog_eq_imbalance_sq_div_two_casimir
 714  chart_is_derived := chart_is_the_imbalance_coordinate
 715  deletion_test := powTwoJlog_not_quadratic_in_imbalance
 716  linearity_is_load_bearing := chart_not_forced_without_linearity
 717  state_event_splice := event_cost_differs_from_state_cost
 718  reduction_to_additivity := additive_continuous_balanced_is_imbalance
 719
 720/-! ## Axiom audit -/
 721
 722#print axioms vanishesAtBalanced_iff
 723#print axioms imbalance_is_the_unique_linear_selection
 724#print axioms vanishesOnBalancedLocus_iff
 725#print axioms imbalance_forced_by_balance_locus
 726#print axioms tolerated_family_is_a_scale_ray
 727#print axioms imbalanceTotalMap_det
 728#print axioms imbalance_total_is_a_canonical_pair
 729#print axioms Jlog_eq_two_sinh_half_sq
 730#print axioms orbitPoint_casimir
 731#print axioms orbitPoint_imbalance
 732#print axioms Jlog_eq_imbalance_sq_div_two_casimir
 733#print axioms chart_variable_is_the_normalized_imbalance
 734#print axioms chart_is_the_imbalance_coordinate
 735#print axioms sinh_two_arsinh
 736#print axioms powTwoJlog_not_quadratic_in_imbalance
 737#print axioms nlP_eq_zero_iff
 738#print axioms nlP_strictMono
 739#print axioms nlP_hasDerivAt
 740#print axioms nlQ_hasDerivAt_snd
 741#print axioms nl_jacobian_det_eq_one
 742#print axioms cost_not_quadratic_in_nlP
 743#print axioms chart_not_forced_without_linearity
 744#print axioms event_cost_differs_from_state_cost
 745#print axioms orbitPoint_is_reached_by_event
 746#print axioms additive_continuous_balanced_is_imbalance
 747#print axioms imbalance_is_additive_continuous_balanced
 748#print axioms chartStipulatedVerdict
 749
 750end
 751
 752end ChartFromLedgerMomentum
 753end SevenGaps
 754end Gravity
 755end IndisputableMonolith
 756