IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost

   1import IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity
   2import IndisputableMonolith.Cost.Convexity
   3import IndisputableMonolith.Cost.FunctionalEquation
   4import IndisputableMonolith.Cost.SymplecticAction
   5
   6/-!
   7# Pillar 1 work item 1: halving the disclosed constraint premise
   8
   9`HKTKineticNormalizedRigidity.KineticNormalizedCanonicalMom` carries a disclosed
  10premise,
  11
  12    S.hp a b p = (2 * cKin) * p     with `cKin ≠ 0` constant,
  13
  14and four kill theorems in that module show the rigidity conclusion is false
  15without it, so the premise carries the whole load. This module reduces that load
  16and reports, in Lean, exactly how far the reduction goes and where it stops.
  17
  18## What is established
  19
  20**§2. Only half the premise was ever an assumption.** The premise says two
  21things: the momentum response is linear in the momentum, and its coefficient
  22does not look at the neighbouring field values. Assume only the second, together
  23with vanishing at zero momentum,
  24
  25    S.hp a b p = φ p,   φ 0 = 0,
  26
  27and the point-split functional equation carried by every `CanonicalMom` target
  28forces `φ` to be exactly linear, with an explicit nonzero coefficient
  29(`kinetic_normalization_of_universal_response`). No recognition input is used.
  30Under the ambient `CanonicalMom` axioms the two classes are therefore
  31*equivalent*, which is what `UniversalKineticCanonicalMom.toKineticNormalized`
  32and its converse say. The result is not a larger model class; it is that the
  33load-bearing surface of the disclosed premise is field-independence alone.
  34
  35**§3. Field-independence is equivalent to channel separation.** Writing the
  36density as a momentum-channel cost plus a link term, `h a b p = K p + U a b`
  37with `K` stationary at zero momentum, is equivalent to §2's hypothesis
  38(`universal_of_channelSeparated`, `channelSeparated_of_universal`). That is a
  39restatement, not a weakening, and it is recorded as one. Its only value is
  40provenance: `Foundation.JHessianGolden.additivePosting` already formalizes
  41recognition cost as posted additively coordinate by coordinate,
  42`Φ(x) = Σᵢ J(xᵢ)`, with Hessian `diag(J''(xᵢ))`. Channel separation is that
  43additivity applied to a two-channel split. Whether the momentum and the spatial
  44link are distinct ledger channels is **not proved here**; see the open items
  45below.
  46
  47**§4. The exact cost is excluded from the linear chart.** Identify the momentum
  48with the log-imbalance linearly, `t = κ p`; then `Jlog t = cosh t - 1` gives
  49momentum response `w κ sinh (κ p)`, derived rather than assumed
  50(`costKinetic_hp_eq_sinh`), which §2 forces linear, and `sinh` is not linear
  51(`no_exact_cost_kinetic_canonicalMom`). Read the scope literally: this excludes
  52that chart, not the cost. §8 exhibits a chart in which the exact cost is
  53quadratic and does inhabit the algebra.
  54
  55**§5. The balance jet fits, with a fitted coefficient.** The second-order jet
  56about balance is `JlogQuad t = (J''(1) / 2) * t ^ 2`
  57(`JlogQuad_matches_Jlog_to_second_order`). A target with that momentum sector
  58satisfies the disclosed premise with `cKin = w * κ ^ 2 * J''(1) / 2`
  59(`quadCost_hp_eq_linear`) and inherits full ADM rigidity
  60(`quadCost_ADM_rigidity`). Both `w` and `κ` are free, so that number is a fit.
  61
  62**§6. The load-bearing test.** The variable-kinetic inhabitant of the kill tower
  63is a field-dependent cost weight and is excluded from the universal class
  64(`vacuumKinetic_not_universalKinetic`), while the ADM anchor still inhabits it,
  65so §2 has not emptied the class.
  66
  67**§7 does not work, and says so.** Its route was to impose the calibration
  68condition `J''(1) = 1` on a per-site jet family. Three defects kill it: the
  69family is defined in this module, so the per-site condition is settled by an
  70unfold and is the between-site equality renamed; the free chart absorbs the
  71value, so only constancy does work and the recognition number does none; and the
  72family fails the Recognition Composition Law outright (`jetCost_not_rcl`). The
  73section is kept with that diagnosis because the general lesson transfers: a
  74pointwise recognition condition carries weight only in proportion to the depth of
  75the uniqueness theorem behind it, and none at all if the ambient free parameters
  76can absorb its value.
  77
  78**§8. The composition law carries the premise.** Two results. First the chart:
  79`J (exp t) = 2 sinh (t / 2) ^ 2`, so identifying the momentum with the
  80half-imbalance *sine*, `t = 2 arsinh (λ p)`, makes the exact recognition cost
  81`2 λ ^ 2 p ^ 2` with no truncation (`Jlog_two_arsinh`). The exact cost inhabits
  82the undeformed algebra, and §5's truncation was an artifact of §4's chart. Then
  83the derivation: let each site carry its own cost weight `W a b`, so
  84field-independence is absent from the hypothesis, and require each site's weight
  85to satisfy the Recognition Composition Law. Since `w * J` satisfies that law only
  86for `w` in `{0, 1}` (`compositionLaw_forces_unit_weight`), because a rescaled
  87recognition cost is not a recognition cost, every weight is forced to `1`, hence
  88`S.hp a b p = 4 λ ^ 2 p` and `cKin = 2 λ ^ 2 > 0`
  89(`rclKinetic_hp_eq_linear`, `rclKinetic_ADM_rigidity`). The ADM anchor inhabits
  90the class at `λ = 1/2` with its own coefficient `1/2` (`hamDynRCLKinetic`), and
  91deleting the clause readmits the kill inhabitant *exactly*, not by analogy: at
  92`λ = 1/2` with weights `2 / (1 + a ^ 2)` the profile is
  93`vacuumKineticLocalProfile` (`vacuumKineticLocalProfile_eq_exactCost`), which
  94`not_HKTRigidityModVacuumStatementN2` refutes. The exclusion is also proved
  95directly from the clause (`no_rcl_presentation_of_vacuumKinetic`).
  96
  97## What is and is not established
  98
  99Established: the substrate supplies two facts about the constraint sector that
 100the algebra does not. The momentum-channel cost weight cannot vary from site to
 101site, and it cannot be negative, so the kinetic coefficient is field-independent
 102and positive. Both come from one theorem about the composition law, applied to
 103the repo's own `Cost.Jcost`, and deleting that theorem's hypothesis makes the
 104rigidity conclusion false rather than weaker.
 105
 106Not established: the magnitude. `cKin = 2 λ ^ 2` with `λ` free, and `λ` is fixed
 107in the anchor only by matching ADM's coefficient, so it is fitted. Nor is the
 108channel identification discharged: the chart is assumed to be one global
 109constant, and a site-dependent chart `λ a b` reproduces the kill inhabitant at
 110unit weight. That is the honest boundary. Recognition now does logical work in
 111the constraint sector, and it does not yet predict a number there.
 112
 113## The open objects, named
 114
 1151. A ledger-axiom predicate on point-split targets that forces the chart to be
 116   global, which is what would discharge the channel identification. The test it
 117   must pass is sharper than before: it has to separate two countermodels, the
 118   variable-weight kill inhabitant *and* the unit-weight site-dependent chart
 119   `λ a b`. A predicate that only excludes the first is another guard that does
 120   not discriminate.
 1212. Any independent fixing of `λ`, that is, a quantization of the momentum-channel
 122   half-imbalance sine against a recognition constant rather than against ADM's
 123   `cKin`. This is the only thing that would turn `cKin = 2 λ ^ 2` from a
 124   positivity statement into a number.
 125
 126Provenance of the corrections: a cross-family hostile read (Grok 4.5, 2026-07-25)
 127forced the §1 to §6 language, and a four-family panel (Opus 5, Grok 4.5,
 128GPT-5.6 Sol, Kimi K3, 2026-07-25) killed §7 and supplied both the composition-law
 129route and the chart identity that §8 is built on.
 130
 131No `sorry`, no `admit`, no new axiom, no `native_decide`. No FullTheoryLedger
 132flag changes.
 133-/
 134
 135namespace IndisputableMonolith
 136namespace Gravity
 137namespace SevenGaps
 138namespace HKTKineticFromRecognitionCost
 139
 140open HypersurfaceDeformation DynamicStructureBracket DynamicStructureFunctionBlocker
 141open HKTPointSplitTarget HKTPointSplitStrong HKTLocalFunctionalEquation
 142open HKTCanonicalMomTarget HKTCanonicalMomRigidity
 143open HKTKineticNormalizedRigidity
 144open FullTheoryLedger
 145
 146noncomputable section
 147
 148/-! ## §1. The weakened premise -/
 149
 150/-- A `CanonicalMom` target whose momentum response is *ultralocal-universal*:
 151it depends on the momentum alone, not on the neighbouring field values, and it
 152vanishes at zero momentum.
 153
 154As a hypothesis this is weaker than `KineticNormalizedCanonicalMom`, which also
 155demands linearity. As a class it is not larger: §2 proves the two coincide under
 156the ambient `CanonicalMom` axioms. -/
 157structure UniversalKineticCanonicalMom where
 158  target : HKTPointSplitTargetDynCanonicalMom
 159  universal_response :
 160    ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (φ : ℝ → ℝ),
 161      ContDiff ℝ 2 (profileMap h) ∧
 162        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 163          target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
 164          (∀ a b p : ℝ, S.hp a b p = φ p) ∧ φ 0 = 0
 165
 166/-! ## §2. The functional equation forces linearity -/
 167
 168/-- The structure function of a `CanonicalMom` target takes a nonzero value
 169somewhere: a structure function vanishing identically would be phase-space
 170constant, which `structure_nonconstant` forbids. -/
 171theorem exists_structure_value_ne_zero
 172    (T : HKTPointSplitTargetDynCanonicalMom) (g : ℝ → ℝ)
 173    (hG : ∀ (x : PhaseSpace 2) (j : ZMod 2), T.structureFunction x j = g (x.1 j)) :
 174    ∃ a : ℝ, g a ≠ 0 := by
 175  by_contra hall
 176  push_neg at hall
 177  refine T.structure_nonconstant ?_
 178  intro x y j
 179  rw [hG x j, hG y j, hall (x.1 j), hall (y.1 j)]
 180
 181/-- **Half the premise, derived.** A field-independent momentum response
 182vanishing at zero momentum is automatically linear on any `CanonicalMom`
 183point-split target, with the coefficient read off the momentum coupling, the
 184structure function, and the gradient response at one point.
 185
 186Nothing about recognition enters. What enters is that the point-split functional
 187equation is separately linear in each momentum slot, so a response that cannot
 188hide field dependence cannot hide nonlinearity either. The choice of the point
 189`(a₀, a₀ + 1)` is free: the denominator cannot vanish, since a vanishing one
 190would make the equation read `0 = cMom * g a₀ * r`, false at `r = 1`. -/
 191theorem kinetic_normalization_of_universal_response
 192    (T : HKTPointSplitTargetDynCanonicalMom)
 193    (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom : ℝ) (φ : ℝ → ℝ)
 194    (hHam : ∀ (x : PhaseSpace 2) (j : ZMod 2),
 195      T.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j))
 196    (hG : ∀ (x : PhaseSpace 2) (j : ZMod 2), T.structureFunction x j = g (x.1 j))
 197    (hcMom : cMom ≠ 0)
 198    (hMom : ∀ (x : PhaseSpace 2) (j : ZMod 2),
 199      T.momDensity x j = cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j))
 200    (hUniv : ∀ a b p : ℝ, S.hp a b p = φ p) (hφ0 : φ 0 = 0) :
 201    ∃ cKin : ℝ, cKin ≠ 0 ∧ ∀ a b p : ℝ, S.hp a b p = (2 * cKin) * p := by
 202  obtain ⟨a₀, hga₀⟩ := exists_structure_value_ne_zero T g hG
 203  have hFE := alternating_FE_of_profile T h S g cMom hHam hG hMom
 204  -- Evaluate the functional equation at `(a, b, p, r) = (a₀, a₀ + 1, 0, r)`.
 205  have key : ∀ r : ℝ, S.hb a₀ (a₀ + 1) 0 * φ r = cMom * g a₀ * r := by
 206    intro r
 207    have hr := hFE a₀ (a₀ + 1) 0 r
 208    rw [hUniv (a₀ + 1) a₀ r, hUniv a₀ (a₀ + 1) 0, hφ0] at hr
 209    have hsub : a₀ + 1 - a₀ = (1 : ℝ) := by ring
 210    rw [hsub] at hr
 211    linarith [hr]
 212  have hprod : cMom * g a₀ ≠ 0 := mul_ne_zero hcMom hga₀
 213  have hbne : S.hb a₀ (a₀ + 1) 0 ≠ 0 := by
 214    intro h0
 215    have h1 := key 1
 216    rw [h0, zero_mul, mul_one] at h1
 217    exact hprod h1.symm
 218  refine ⟨cMom * g a₀ / (2 * S.hb a₀ (a₀ + 1) 0), ?_, ?_⟩
 219  · exact div_ne_zero hprod (mul_ne_zero two_ne_zero hbne)
 220  · intro a b p
 221    rw [hUniv a b p]
 222    refine mul_left_cancel₀ hbne ?_
 223    rw [key p]
 224    field_simp
 225
 226/-- The derived coefficient does not depend on which point was used to read it
 227off: any two constants presenting the same response agree. -/
 228theorem kinetic_coefficient_unique {h : LocalHamProfile} (S : LocalHamSmooth h)
 229    (c₁ c₂ : ℝ)
 230    (h₁ : ∀ a b p : ℝ, S.hp a b p = (2 * c₁) * p)
 231    (h₂ : ∀ a b p : ℝ, S.hp a b p = (2 * c₂) * p) : c₁ = c₂ := by
 232  have hEq := (h₁ 0 0 1).symm.trans (h₂ 0 0 1)
 233  linarith [hEq]
 234
 235/-- Every universal-response target is kinetic-normalized. -/
 236def UniversalKineticCanonicalMom.toKineticNormalized
 237    (T : UniversalKineticCanonicalMom) : KineticNormalizedCanonicalMom where
 238  target := T.target
 239  kinetic_normalized := by
 240    obtain ⟨h, S, φ, hcd, hHam, hUniv, hφ0⟩ := T.universal_response
 241    obtain ⟨g, hG⟩ := T.target.structure_profile
 242    obtain ⟨cMom, hcMom, hMom⟩ := T.target.canonical_mom
 243    obtain ⟨cKin, hcKin, hHp⟩ :=
 244      kinetic_normalization_of_universal_response T.target h S g cMom φ hHam hG
 245        hcMom hMom hUniv hφ0
 246    exact ⟨h, S, cKin, hcd, hcKin, hHam, hHp⟩
 247
 248/-- And conversely, so the two classes are the same class and §2 is an
 249equivalence rather than an enlargement. -/
 250def KineticNormalizedCanonicalMom.toUniversalKinetic
 251    (T : KineticNormalizedCanonicalMom) : UniversalKineticCanonicalMom where
 252  target := T.target
 253  universal_response := by
 254    obtain ⟨h, S, cKin, hcd, _hcKin, hHam, hHp⟩ := T.kinetic_normalized
 255    exact ⟨h, S, fun p => (2 * cKin) * p, hcd, hHam, hHp, by ring⟩
 256
 257/-- **Rigidity without the assumed normalization.** The ADM shape and the
 258canonical momentum form hold for every target whose momentum response is merely
 259field-independent and stationary at zero momentum. -/
 260theorem HKTRigidityUniversalKineticN2_holds (T : UniversalKineticCanonicalMom) :
 261    ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
 262      cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
 263        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 264          T.target.hamDensity x j =
 265            cKin * (x.2 j * x.2 j) +
 266              cGrad *
 267                (T.target.structureFunction x j *
 268                  ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
 269              V (x.1 j)) ∧
 270        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 271          T.target.momDensity x j =
 272            cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
 273  HKTRigidityKineticNormalizedN2_holds T.toKineticNormalized
 274
 275/-! ## §3. Channel separation, and where its provenance stops -/
 276
 277/-- The density splits into a momentum-channel cost and a link term, with the
 278momentum channel stationary at zero momentum.
 279
 280`Foundation.JHessianGolden.additivePosting` formalizes recognition cost as
 281posted additively coordinate by coordinate, `Φ(x) = Σᵢ J(xᵢ)`, with Hessian
 282`diag(J''(xᵢ))`; this is that additivity for a two-channel split, and the
 283stationarity clause is `J'(1) = 0` transported to the momentum chart. The two
 284theorems below show this is logically the same hypothesis as §2's, so the
 285recognition layer supplies provenance and not strength. -/
 286def ChannelSeparated (h : LocalHamProfile) : Prop :=
 287  ∃ (K : ℝ → ℝ) (U : ℝ → ℝ → ℝ),
 288    (∀ a b p : ℝ, h a b p = K p + U a b) ∧ HasDerivAt K 0 0
 289
 290theorem universal_of_channelSeparated
 291    (h : LocalHamProfile) (S : LocalHamSmooth h)
 292    (hcd : ContDiff ℝ 2 (profileMap h)) (hCS : ChannelSeparated h) :
 293    ∃ φ : ℝ → ℝ, (∀ a b p : ℝ, S.hp a b p = φ p) ∧ φ 0 = 0 := by
 294  obtain ⟨K, U, hEq, hK0⟩ := hCS
 295  have hKderiv : ∀ a b p : ℝ, HasDerivAt K (S.hp a b p) p := by
 296    intro a b p
 297    have hS := hasDerivAt_hp_of_normalized h S hcd a b p
 298    have hfun : (fun t => h a b t) = fun t => K t + U a b :=
 299      funext fun t => hEq a b t
 300    rw [hfun] at hS
 301    simpa using hS.add_const (-(U a b))
 302  refine ⟨fun p => S.hp 0 0 p, ?_, ?_⟩
 303  · intro a b p
 304    exact (hKderiv a b p).unique (hKderiv 0 0 p)
 305  · exact (hKderiv 0 0 0).unique hK0
 306
 307theorem channelSeparated_of_universal
 308    (h : LocalHamProfile) (S : LocalHamSmooth h)
 309    (hcd : ContDiff ℝ 2 (profileMap h)) (φ : ℝ → ℝ)
 310    (hUniv : ∀ a b p : ℝ, S.hp a b p = φ p) (hφ0 : φ 0 = 0) :
 311    ChannelSeparated h := by
 312  refine ⟨fun p => h 0 0 p - h 0 0 0, fun a b => h a b 0, ?_, ?_⟩
 313  · intro a b p
 314    have hF : ∀ t : ℝ, HasDerivAt (fun u => h a b u - h 0 0 u) 0 t := by
 315      intro t
 316      have h1 := hasDerivAt_hp_of_normalized h S hcd a b t
 317      have h2 := hasDerivAt_hp_of_normalized h S hcd 0 0 t
 318      have hsub := h1.sub h2
 319      rw [hUniv a b t, hUniv 0 0 t, sub_self] at hsub
 320      exact hsub
 321    have hdiff : Differentiable ℝ (fun u => h a b u - h 0 0 u) :=
 322      fun t => (hF t).differentiableAt
 323    have hconst :=
 324      is_const_of_deriv_eq_zero hdiff (fun t => (hF t).deriv) p 0
 325    simp only at hconst
 326    linarith [hconst]
 327  · have h1 := hasDerivAt_hp_of_normalized h S hcd 0 0 0
 328    rw [hUniv 0 0 0, hφ0] at h1
 329    exact h1.sub_const (h 0 0 0)
 330
 331/-! ## §4. The exact recognition cost is excluded -/
 332
 333/-- A local Hamiltonian density carrying its momentum dependence as the
 334recognition cost of a ledger imbalance, read in the log-imbalance chart: the
 335momentum `p` sits at ledger ratio `exp (κ * p)`, whose cost is `Jlog (κ * p)`,
 336with cost weight `w`. Both `w` and `κ` are free constants. -/
 337def costKineticProfile (w κ : ℝ) (U : ℝ → ℝ → ℝ) : LocalHamProfile :=
 338  fun a b p => w * Cost.Jlog (κ * p) + U a b
 339
 340/-- A `CanonicalMom` target whose momentum sector is the exact recognition cost. -/
 341structure CostKineticCanonicalMom where
 342  target : HKTPointSplitTargetDynCanonicalMom
 343  cost_kinetic :
 344    ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (w κ : ℝ) (U : ℝ → ℝ → ℝ),
 345      ContDiff ℝ 2 (profileMap h) ∧ w ≠ 0 ∧ κ ≠ 0 ∧
 346        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 347          target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
 348          (∀ a b p : ℝ, h a b p = w * Cost.Jlog (κ * p) + U a b)
 349
 350/-- The momentum response of a recognition-cost density is `w κ sinh (κ p)`,
 351derived from `Jlog = cosh - 1` rather than assumed. -/
 352theorem costKinetic_hp_eq_sinh
 353    (h : LocalHamProfile) (S : LocalHamSmooth h) (w κ : ℝ) (U : ℝ → ℝ → ℝ)
 354    (hcd : ContDiff ℝ 2 (profileMap h))
 355    (hProf : ∀ a b p : ℝ, h a b p = w * Cost.Jlog (κ * p) + U a b)
 356    (a b p : ℝ) :
 357    S.hp a b p = w * (Real.sinh (κ * p) * κ) := by
 358  have hS := hasDerivAt_hp_of_normalized h S hcd a b p
 359  have hfun : (fun t => h a b t) = fun t => w * Cost.Jlog (κ * t) + U a b :=
 360    funext fun t => hProf a b t
 361  rw [hfun] at hS
 362  have hinner : HasDerivAt (fun t : ℝ => κ * t) κ p := by
 363    simpa using (hasDerivAt_id p).const_mul κ
 364  have hJ : HasDerivAt (fun t : ℝ => Cost.Jlog (κ * t)) (Real.sinh (κ * p) * κ) p :=
 365    (Cost.hasDerivAt_Jlog (κ * p)).comp p hinner
 366  have hexp : HasDerivAt (fun t : ℝ => w * Cost.Jlog (κ * t) + U a b)
 367      (w * (Real.sinh (κ * p) * κ)) p := (hJ.const_mul w).add_const (U a b)
 368  exact hS.unique hexp
 369
 370/-- The cost form satisfies §2's two hypotheses: field-independence because the
 371cost reads the imbalance alone, vanishing at zero momentum because the cost is
 372stationary at the balanced ratio. -/
 373theorem costKinetic_universal
 374    (h : LocalHamProfile) (S : LocalHamSmooth h) (w κ : ℝ) (U : ℝ → ℝ → ℝ)
 375    (hcd : ContDiff ℝ 2 (profileMap h))
 376    (hProf : ∀ a b p : ℝ, h a b p = w * Cost.Jlog (κ * p) + U a b) :
 377    (∀ a b p : ℝ, S.hp a b p = w * (Real.sinh (κ * p) * κ)) ∧
 378      w * (Real.sinh (κ * 0) * κ) = 0 := by
 379  refine ⟨costKinetic_hp_eq_sinh h S w κ U hcd hProf, ?_⟩
 380  rw [mul_zero, Real.sinh_zero, zero_mul, mul_zero]
 381
 382private theorem one_lt_cosh_one : (1 : ℝ) < Real.cosh 1 := by
 383  rw [Real.cosh_eq]
 384  have h1 : (2.7182818283 : ℝ) < Real.exp 1 := Real.exp_one_gt_d9
 385  have h2 : (0 : ℝ) < Real.exp (-1) := Real.exp_pos _
 386  linarith
 387
 388private theorem sinh_one_pos : (0 : ℝ) < Real.sinh 1 := by
 389  rw [Real.sinh_eq]
 390  have h1 : (2.7182818283 : ℝ) < Real.exp 1 := Real.exp_one_gt_d9
 391  have h2 : Real.exp (-1) < Real.exp 0 := Real.exp_lt_exp.mpr (by norm_num)
 392  rw [Real.exp_zero] at h2
 393  linarith
 394
 395/-- `sinh` is not linear: no constant rescaling of the identity matches it. -/
 396theorem sinh_not_linear (c : ℝ) : ¬ ∀ t : ℝ, Real.sinh t = c * t := by
 397  intro hlin
 398  have h1 : Real.sinh 1 = c := by
 399    have := hlin 1
 400    linarith [this]
 401  have h2 : Real.sinh 2 = c * 2 := hlin 2
 402  have htwo : Real.sinh (2 * (1 : ℝ)) = 2 * Real.sinh 1 * Real.cosh 1 :=
 403    Real.sinh_two_mul 1
 404  rw [show (2 * (1 : ℝ)) = 2 by norm_num] at htwo
 405  rw [h2, h1] at htwo
 406  have hcpos : (0 : ℝ) < c := by rw [← h1]; exact sinh_one_pos
 407  nlinarith [one_lt_cosh_one, hcpos, htwo]
 408
 409/-- **The exclusion, in the linear chart only.** No nondegenerate `CanonicalMom`
 410point-split target carries the exact recognition cost in its momentum sector
 411*when the momentum is identified with the log-imbalance linearly*, `t = κ p`.
 412
 413§2 forces the momentum response linear; §4 makes it `w κ sinh (κ p)`; `sinh` is
 414not linear. Read the scope literally: `CostKineticCanonicalMom` hardcodes the
 415linear chart, so this excludes that chart and not the cost. §8 exhibits a chart in
 416which the same exact cost is quadratic and does inhabit the algebra, so this is a
 417no-go about a coordinate identification rather than about recognition. It is also
 418not a statement that the higher terms are a physical correction: in this chart
 419they leave the algebra rather than deform it. -/
 420theorem no_exact_cost_kinetic_canonicalMom : IsEmpty CostKineticCanonicalMom := by
 421  constructor
 422  intro T
 423  obtain ⟨h, S, w, κ, U, hcd, hw, hκ, hHam, hProf⟩ := T.cost_kinetic
 424  obtain ⟨g, hG⟩ := T.target.structure_profile
 425  obtain ⟨cMom, hcMom, hMom⟩ := T.target.canonical_mom
 426  obtain ⟨hHp, hφ0⟩ := costKinetic_universal h S w κ U hcd hProf
 427  obtain ⟨cKin, _hcKin, hLin⟩ :=
 428    kinetic_normalization_of_universal_response T.target h S g cMom
 429      (fun p => w * (Real.sinh (κ * p) * κ)) hHam hG hcMom hMom hHp hφ0
 430  have hall : ∀ p : ℝ, w * (Real.sinh (κ * p) * κ) = (2 * cKin) * p := by
 431    intro p
 432    rw [← hHp 0 0 p]
 433    exact hLin 0 0 p
 434  refine sinh_not_linear (2 * cKin / (w * κ * κ)) ?_
 435  intro t
 436  have ht := hall (t / κ)
 437  rw [mul_div_cancel₀ t hκ] at ht
 438  field_simp at ht ⊢
 439  nlinarith [ht]
 440
 441/-! ## §5. The surviving object: the balance jet -/
 442
 443/-- The recognition cost's curvature at the balanced ratio, `deriv (deriv Jcost) 1`,
 444proved equal to `1` in `Cost/Convexity.lean`. -/
 445def recogCurvature : ℝ := deriv (deriv Cost.Jcost) 1
 446
 447theorem recogCurvature_eq_one : recogCurvature = 1 := Cost.deriv2_Jcost_one
 448
 449/-- The second-order jet of the recognition cost about balance, written so that
 450its coefficient is literally the recognition primitive. -/
 451def JlogQuad (t : ℝ) : ℝ := (recogCurvature / 2) * t ^ 2
 452
 453theorem JlogQuad_eq_half_sq (t : ℝ) : JlogQuad t = t ^ 2 / 2 := by
 454  rw [JlogQuad, recogCurvature_eq_one]; ring
 455
 456theorem deriv_Jlog_eq_sinh : deriv Cost.Jlog = Real.sinh :=
 457  funext fun t => (Cost.hasDerivAt_Jlog t).deriv
 458
 459/-- The curvature of the recognition cost at balance, computed in the
 460log-imbalance chart, is `J''(1)`. -/
 461theorem deriv2_Jlog_zero_eq_recogCurvature :
 462    deriv (deriv Cost.Jlog) 0 = recogCurvature := by
 463  rw [deriv_Jlog_eq_sinh, Real.deriv_sinh, Real.cosh_zero, recogCurvature_eq_one]
 464
 465theorem hasDerivAt_JlogQuad (t : ℝ) :
 466    HasDerivAt JlogQuad (recogCurvature * t) t := by
 467  have hsq : HasDerivAt (fun u : ℝ => u ^ 2) (2 * t) t := by
 468    simpa using (hasDerivAt_id t).pow 2
 469  have hmul := hsq.const_mul (recogCurvature / 2)
 470  have hrw : recogCurvature / 2 * (2 * t) = recogCurvature * t := by ring
 471  rw [hrw] at hmul
 472  exact hmul
 473
 474private theorem deriv_JlogQuad_eq : deriv JlogQuad = fun t => recogCurvature * t :=
 475  funext fun t => (hasDerivAt_JlogQuad t).deriv
 476
 477/-- `JlogQuad` is the second-order jet: value, slope, and curvature at balance
 478all agree with the exact recognition cost. -/
 479theorem JlogQuad_matches_Jlog_to_second_order :
 480    JlogQuad 0 = Cost.Jlog 0 ∧
 481      deriv JlogQuad 0 = deriv Cost.Jlog 0 ∧
 482        deriv (deriv JlogQuad) 0 = deriv (deriv Cost.Jlog) 0 := by
 483  have hval : JlogQuad 0 = Cost.Jlog 0 := by
 484    rw [JlogQuad_eq_half_sq, Cost.Jlog_as_cosh, Real.cosh_zero]; norm_num
 485  have hslope : deriv JlogQuad 0 = deriv Cost.Jlog 0 := by
 486    rw [deriv_JlogQuad_eq, deriv_Jlog_eq_sinh]
 487    show recogCurvature * (0 : ℝ) = Real.sinh 0
 488    rw [mul_zero, Real.sinh_zero]
 489  have hcurv : deriv (deriv JlogQuad) 0 = deriv (deriv Cost.Jlog) 0 := by
 490    rw [deriv_JlogQuad_eq, deriv2_Jlog_zero_eq_recogCurvature]
 491    have hlin : HasDerivAt (fun t : ℝ => recogCurvature * t) recogCurvature 0 := by
 492      simpa using (hasDerivAt_id (0 : ℝ)).const_mul recogCurvature
 493    exact hlin.deriv
 494  exact ⟨hval, hslope, hcurv⟩
 495
 496/-- A local Hamiltonian density whose momentum sector is the recognition cost
 497truncated at its balance jet. -/
 498def quadCostKineticProfile (w κ : ℝ) (U : ℝ → ℝ → ℝ) : LocalHamProfile :=
 499  fun a b p => w * JlogQuad (κ * p) + U a b
 500
 501/-- A `CanonicalMom` target whose momentum sector is the balance jet. -/
 502structure QuadCostKineticCanonicalMom where
 503  target : HKTPointSplitTargetDynCanonicalMom
 504  quad_cost_kinetic :
 505    ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (w κ : ℝ) (U : ℝ → ℝ → ℝ),
 506      ContDiff ℝ 2 (profileMap h) ∧ w ≠ 0 ∧ κ ≠ 0 ∧
 507        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 508          target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
 509          (∀ a b p : ℝ, h a b p = w * JlogQuad (κ * p) + U a b)
 510
 511/-- The disclosed premise holds for a balance-jet density with
 512
 513    cKin = w * κ ^ 2 * J''(1) / 2.
 514
 515Field-independent because `J''` is evaluated at the balanced ratio, where it is
 516the universal number `1`; `J''` itself is `x ^ (-3)` and is not constant, so
 517field-independence is a property of balance and not an identity. `w` and `κ`
 518are free, so this expression fixes no number: it is a consistency statement, not
 519a prediction. -/
 520theorem quadCost_hp_eq_linear
 521    (h : LocalHamProfile) (S : LocalHamSmooth h) (w κ : ℝ) (U : ℝ → ℝ → ℝ)
 522    (hcd : ContDiff ℝ 2 (profileMap h))
 523    (hProf : ∀ a b p : ℝ, h a b p = w * JlogQuad (κ * p) + U a b)
 524    (a b p : ℝ) :
 525    S.hp a b p = (2 * (w * κ ^ 2 * recogCurvature / 2)) * p := by
 526  have hS := hasDerivAt_hp_of_normalized h S hcd a b p
 527  have hfun : (fun t => h a b t) = fun t => w * JlogQuad (κ * t) + U a b :=
 528    funext fun t => hProf a b t
 529  rw [hfun] at hS
 530  have hinner : HasDerivAt (fun t : ℝ => κ * t) κ p := by
 531    simpa using (hasDerivAt_id p).const_mul κ
 532  have hJ : HasDerivAt (fun t : ℝ => JlogQuad (κ * t))
 533      (recogCurvature * (κ * p) * κ) p :=
 534    (hasDerivAt_JlogQuad (κ * p)).comp p hinner
 535  have hexp : HasDerivAt (fun t : ℝ => w * JlogQuad (κ * t) + U a b)
 536      (w * (recogCurvature * (κ * p) * κ)) p := (hJ.const_mul w).add_const (U a b)
 537  rw [hS.unique hexp]
 538  ring
 539
 540theorem quadCost_cKin_ne_zero {w κ : ℝ} (hw : w ≠ 0) (hκ : κ ≠ 0) :
 541    w * κ ^ 2 * recogCurvature / 2 ≠ 0 := by
 542  have hnum : w * κ ^ 2 * recogCurvature ≠ 0 := by
 543    rw [recogCurvature_eq_one, mul_one]
 544    exact mul_ne_zero hw (pow_ne_zero 2 hκ)
 545  exact div_ne_zero hnum (by norm_num : (2 : ℝ) ≠ 0)
 546
 547/-- A balance-jet target inhabits the kinetic-normalized class with the derived
 548coefficient, so it consumes the derived form rather than an assumed field. -/
 549def QuadCostKineticCanonicalMom.toKineticNormalized
 550    (T : QuadCostKineticCanonicalMom) : KineticNormalizedCanonicalMom where
 551  target := T.target
 552  kinetic_normalized := by
 553    obtain ⟨h, S, w, κ, U, hcd, hw, hκ, hHam, hProf⟩ := T.quad_cost_kinetic
 554    exact ⟨h, S, w * κ ^ 2 * recogCurvature / 2, hcd,
 555      quadCost_cKin_ne_zero hw hκ, hHam,
 556      quadCost_hp_eq_linear h S w κ U hcd hProf⟩
 557
 558/-- Every balance-jet target is ADM in shape with canonical momentum form, and
 559no normalization is assumed in the hypothesis. -/
 560theorem quadCost_ADM_rigidity (T : QuadCostKineticCanonicalMom) :
 561    ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
 562      cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
 563        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 564          T.target.hamDensity x j =
 565            cKin * (x.2 j * x.2 j) +
 566              cGrad *
 567                (T.target.structureFunction x j *
 568                  ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
 569              V (x.1 j)) ∧
 570        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 571          T.target.momDensity x j =
 572            cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
 573  HKTRigidityKineticNormalizedN2_holds T.toKineticNormalized
 574
 575/-! ## §6. The load-bearing test -/
 576
 577/-- **Removing field-independence breaks the proof.** The variable-kinetic
 578inhabitant of the kill tower carries the field-dependent weight `1 / (1 + a ^ 2)`
 579on its momentum term, which is exactly a cost weight that looks at the field. It
 580is excluded from the universal class, and the kill theorems in
 581`HKTKineticNormalizedRigidity` show the rigidity statement is false once such an
 582inhabitant is admitted. So field-independence does not merely strengthen the
 583conclusion; dropping it falsifies it. -/
 584theorem vacuumKinetic_not_universalKinetic :
 585    ¬ ∃ T : UniversalKineticCanonicalMom,
 586      T.target = vacuumKineticCanonicalMomTarget := by
 587  rintro ⟨T, hEq⟩
 588  exact vacuumKinetic_not_kineticNormalized ⟨T.toKineticNormalized, hEq⟩
 589
 590/-- The ADM anchor still inhabits the weakened class, so §2 has not emptied it. -/
 591def hamDynUniversalKinetic : UniversalKineticCanonicalMom :=
 592  KineticNormalizedCanonicalMom.toUniversalKinetic hamDynKineticNormalized
 593
 594theorem hamDyn_satisfies_universalKinetic :
 595    ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
 596      cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
 597        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 598          hamDynUniversalKinetic.target.hamDensity x j =
 599            cKin * (x.2 j * x.2 j) +
 600              cGrad *
 601                (hamDynUniversalKinetic.target.structureFunction x j *
 602                  ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
 603              V (x.1 j)) ∧
 604        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 605          hamDynUniversalKinetic.target.momDensity x j =
 606            cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
 607  HKTRigidityUniversalKineticN2_holds hamDynUniversalKinetic
 608
 609/-! ## §7. Field-independence derived from a recognition primitive
 610
 611**This route does not work, and the section is kept because knowing why is worth
 612more than the theorems are.** It is superseded by §8. The construction: let every
 613pair of neighbouring field values carry its own momentum-sector cost jet in one
 614global chart, with its own log-curvature `c a b`, so that field-independence is
 615absent from the shape; then impose
 616`Cost.FunctionalEquation.IsCalibrated (jetCost (c a b))` at each site, which
 617forces every `c a b` to `1`, hence the disclosed premise with `cKin = κ ^ 2 / 2`.
 618Everything below that sentence is proved, the class is nonempty, and the kill
 619inhabitant is excluded. It still fails, for three reasons, all of them found by a
 620cross-family panel (Opus 5, Grok 4.5, GPT-5.6 Sol, Kimi K3, 2026-07-25) and none
 621of them repaired here.
 622
 623First, `jetCost` is a family this module defines, and
 624`IsCalibrated (jetCost c) ↔ c = 1` is settled by unfolding that definition. A
 625per-site condition whose unique solution is read off a definition is the
 626between-site equality renamed, so the defence that calibration looks at one site
 627while field-independence relates two sites is empty here. It has content only when
 628the uniqueness of the solution is a theorem, which is what §8 arranges.
 629
 630Second, the value is absorbed. `cKin = κ ^ 2 / 2` with `κ` free, so the class of
 631targets with all curvatures equal to `1` in chart `κ` is the class with all
 632curvatures equal to any positive constant `c₀` in chart `κ / sqrt c₀`. The
 633recognition *number* `J''(1) = 1` therefore does no work; only the constancy does.
 634
 635Third, `jetCost c` is not a recognition cost. It fails the Recognition
 636Composition Law for every nonzero `c` (`jetCost_not_rcl`, proved in §8). So this
 637section imposes a normalization on an object the substrate rejects.
 638
 639What survives is the negative result, worth stating because it is general: a
 640recognition condition imposed pointwise carries logical weight only in proportion
 641to the depth of the uniqueness theorem behind it, and a condition whose value the
 642ambient free parameters can absorb carries none at all.
 643-/
 644
 645/-- The multiplicative cost function whose balance jet has log-curvature `c`:
 646in the log-imbalance chart `x = exp t` it is `t ↦ (c / 2) * t ^ 2`. -/
 647def jetCost (c : ℝ) : ℝ → ℝ := fun x => (c / 2) * (Real.log x) ^ 2
 648
 649theorem G_jetCost (c : ℝ) :
 650    Cost.FunctionalEquation.G (jetCost c) = fun t => (c / 2) * t ^ 2 := by
 651  funext t
 652  simp [Cost.FunctionalEquation.G, jetCost, Real.log_exp]
 653
 654private theorem deriv_half_sq (c : ℝ) :
 655    deriv (fun t : ℝ => (c / 2) * t ^ 2) = fun t => c * t := by
 656  funext t
 657  have hsq : HasDerivAt (fun u : ℝ => u ^ 2) (2 * t) t := by
 658    simpa using (hasDerivAt_id t).pow 2
 659  have hmul := hsq.const_mul (c / 2)
 660  rw [show c / 2 * (2 * t) = c * t by ring] at hmul
 661  exact hmul.deriv
 662
 663private theorem deriv_linear_zero (c : ℝ) : deriv (fun t : ℝ => c * t) 0 = c := by
 664  simpa using ((hasDerivAt_id (0 : ℝ)).const_mul c).deriv
 665
 666/-- **Calibration reads off the jet coefficient.** A balance jet is calibrated
 667exactly when its log-curvature is `J''(1) = 1`.
 668
 669Do not read `jetCost c` as a recognition cost. It satisfies no composition law
 670for any nonzero `c` (`jetCost_not_rcl`), and calling it one here would
 671contradict that theorem. It is a one-parameter deformation of the recognition
 672cost's jet, which is a different object. -/
 673theorem isCalibrated_jetCost_iff (c : ℝ) :
 674    Cost.FunctionalEquation.IsCalibrated (jetCost c) ↔ c = 1 := by
 675  unfold Cost.FunctionalEquation.IsCalibrated
 676  rw [G_jetCost, deriv_half_sq, deriv_linear_zero]
 677
 678/-- `jetCost` is not an ad hoc family invented for this section. In the log chart
 679it is `t ↦ (c / 2) * t ^ 2`, and at the recognition curvature `c = J''(1)` that
 680is exactly `JlogQuad`, the balance jet of the actual recognition cost from §5. So
 681`jetCost` is the one-parameter deformation of the recognition cost's own jet, and
 682`isCalibrated_jetCost_iff` says the calibration axiom selects the undeformed
 683member. -/
 684theorem G_jetCost_recogCurvature :
 685    Cost.FunctionalEquation.G (jetCost recogCurvature) = JlogQuad := by
 686  rw [G_jetCost]
 687  funext t
 688  rw [JlogQuad]
 689
 690/-- A local Hamiltonian density whose momentum sector is, at each pair of
 691neighbouring field values, the balance jet of that pair's own cost function,
 692read in one global chart `κ`. The log-curvature `c a b` is free to look at the
 693field: this shape does not assume field-independence. -/
 694def perSiteJetProfile (c : ℝ → ℝ → ℝ) (κ : ℝ) (U : ℝ → ℝ → ℝ) : LocalHamProfile :=
 695  fun a b p => (c a b / 2) * (κ * p) ^ 2 + U a b
 696
 697/-- The calibration clause is a statement about the density, not about the
 698auxiliary family. Read the density in the log-imbalance chart `t = κ p`; the
 699clause holds at a site exactly when the density's curvature there, at balance, is
 700the recognition curvature `J''(1)`. Nothing is hidden in `jetCost`. -/
 701theorem isCalibrated_iff_density_curvature
 702    (c : ℝ → ℝ → ℝ) (κ : ℝ) (U : ℝ → ℝ → ℝ) (hκ : κ ≠ 0) (a b : ℝ) :
 703    Cost.FunctionalEquation.IsCalibrated (jetCost (c a b)) ↔
 704      deriv (deriv (fun t : ℝ => perSiteJetProfile c κ U a b (t / κ))) 0
 705        = recogCurvature := by
 706  have hchart : (fun t : ℝ => perSiteJetProfile c κ U a b (t / κ))
 707      = fun t : ℝ => (c a b / 2) * t ^ 2 + U a b := by
 708    funext t
 709    simp only [perSiteJetProfile]
 710    rw [mul_div_cancel₀ t hκ]
 711  have hshift : deriv (fun t : ℝ => (c a b / 2) * t ^ 2 + U a b)
 712      = deriv (fun t : ℝ => (c a b / 2) * t ^ 2) := by
 713    funext t
 714    exact deriv_add_const (f := fun u : ℝ => (c a b / 2) * u ^ 2) (x := t) (c := U a b)
 715  rw [isCalibrated_jetCost_iff, hchart, hshift, deriv_half_sq, deriv_linear_zero,
 716    recogCurvature_eq_one]
 717
 718/-- A `CanonicalMom` target whose momentum sector is a per-site cost jet in a
 719global chart, with every site's jet *calibrated*. The jets are not recognition
 720costs; see `jetCost_not_rcl` and the section header. -/
 721structure CalibratedJetCanonicalMom where
 722  target : HKTPointSplitTargetDynCanonicalMom
 723  calibrated_jet :
 724    ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (c : ℝ → ℝ → ℝ) (κ : ℝ)
 725      (U : ℝ → ℝ → ℝ),
 726      ContDiff ℝ 2 (profileMap h) ∧ κ ≠ 0 ∧
 727        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 728          target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
 729          (∀ a b p : ℝ, h a b p = perSiteJetProfile c κ U a b p) ∧
 730          (∀ a b : ℝ, Cost.FunctionalEquation.IsCalibrated (jetCost (c a b)))
 731
 732/-- **Field-independence, derived.** Calibration forces every site's
 733log-curvature to `1`, so the momentum response is `κ ^ 2 * p` at every pair of
 734field values, which is the disclosed premise with `cKin = κ ^ 2 / 2`. -/
 735theorem calibratedJet_hp_eq_linear
 736    (h : LocalHamProfile) (S : LocalHamSmooth h) (c : ℝ → ℝ → ℝ) (κ : ℝ)
 737    (U : ℝ → ℝ → ℝ)
 738    (hcd : ContDiff ℝ 2 (profileMap h))
 739    (hProf : ∀ a b p : ℝ, h a b p = perSiteJetProfile c κ U a b p)
 740    (hCal : ∀ a b : ℝ, Cost.FunctionalEquation.IsCalibrated (jetCost (c a b)))
 741    (a b p : ℝ) :
 742    S.hp a b p = (2 * (κ ^ 2 / 2)) * p := by
 743  have hc : c a b = 1 := (isCalibrated_jetCost_iff (c a b)).mp (hCal a b)
 744  have hS := hasDerivAt_hp_of_normalized h S hcd a b p
 745  have hfun : (fun t => h a b t) = fun t => (1 / 2 : ℝ) * (κ * t) ^ 2 + U a b := by
 746    funext t
 747    rw [hProf a b t]
 748    simp only [perSiteJetProfile, hc]
 749  rw [hfun] at hS
 750  have hinner : HasDerivAt (fun t : ℝ => κ * t) κ p := by
 751    simpa using (hasDerivAt_id p).const_mul κ
 752  have hsq : HasDerivAt (fun t : ℝ => (κ * t) ^ 2) (2 * (κ * p) * κ) p := by
 753    simpa using hinner.pow 2
 754  have hhalf := hsq.const_mul (1 / 2 : ℝ)
 755  rw [show (1 / 2 : ℝ) * (2 * (κ * p) * κ) = κ ^ 2 * p by ring] at hhalf
 756  rw [hS.unique (hhalf.add_const (U a b))]
 757  ring
 758
 759theorem calibratedJet_cKin_ne_zero {κ : ℝ} (hκ : κ ≠ 0) : κ ^ 2 / 2 ≠ 0 :=
 760  div_ne_zero (pow_ne_zero 2 hκ) (by norm_num)
 761
 762/-- A calibrated-jet target inhabits the kinetic-normalized class, with the
 763coefficient derived from the calibration axiom rather than assumed. -/
 764def CalibratedJetCanonicalMom.toKineticNormalized
 765    (T : CalibratedJetCanonicalMom) : KineticNormalizedCanonicalMom where
 766  target := T.target
 767  kinetic_normalized := by
 768    obtain ⟨h, S, c, κ, U, hcd, hκ, hHam, hProf, hCal⟩ := T.calibrated_jet
 769    exact ⟨h, S, κ ^ 2 / 2, hcd, calibratedJet_cKin_ne_zero hκ, hHam,
 770      calibratedJet_hp_eq_linear h S c κ U hcd hProf hCal⟩
 771
 772/-- Every calibrated-jet target is ADM in shape, with the canonical momentum
 773relation. No field-independence appears anywhere in the hypothesis. -/
 774theorem calibratedJet_ADM_rigidity (T : CalibratedJetCanonicalMom) :
 775    ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
 776      cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
 777        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 778          T.target.hamDensity x j =
 779            cKin * (x.2 j * x.2 j) +
 780              cGrad *
 781                (T.target.structureFunction x j *
 782                  ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
 783              V (x.1 j)) ∧
 784        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 785          T.target.momDensity x j =
 786            cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
 787  HKTRigidityKineticNormalizedN2_holds T.toKineticNormalized
 788
 789/-- **The class is nonempty, so the rigidity above is not vacuous.** The ADM
 790anchor's momentum sector is literally the calibrated recognition jet in the
 791chart `κ = 1`: `hamDynLocalProfile a b p = (1/2) * p ^ 2 + U a b`, which is
 792`perSiteJetProfile` with every log-curvature equal to the recognition primitive.
 793Nothing is fitted here; the anchor was written before this section existed. -/
 794def hamDynCalibratedJet : CalibratedJetCanonicalMom where
 795  target := hamDynPointSplitTargetCanonicalMom
 796  calibrated_jet := by
 797    refine ⟨hamDynLocalProfile, hamDynLocalSmooth, (fun _ _ => 1), 1,
 798      (fun a b => (1 / 2 : ℝ) * ((1 + a * a) * ((b - a) * (b - a)))),
 799      hamDynLocalProfile_contDiff2, one_ne_zero,
 800      hamDynDensity_eq_localProfile, ?_, ?_⟩
 801    · intro a b p
 802      simp only [hamDynLocalProfile, perSiteJetProfile]
 803      ring
 804    · intro _ _
 805      exact (isCalibrated_jetCost_iff 1).mpr rfl
 806
 807instance : Nonempty CalibratedJetCanonicalMom := ⟨hamDynCalibratedJet⟩
 808
 809theorem hamDyn_satisfies_calibratedJet :
 810    ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
 811      cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
 812        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 813          hamDynCalibratedJet.target.hamDensity x j =
 814            cKin * (x.2 j * x.2 j) +
 815              cGrad *
 816                (hamDynCalibratedJet.target.structureFunction x j *
 817                  ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
 818              V (x.1 j)) ∧
 819        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 820          hamDynCalibratedJet.target.momDensity x j =
 821            cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
 822  calibratedJet_ADM_rigidity hamDynCalibratedJet
 823
 824/-! ### The removal test
 825
 826The two theorems below are the discrimination. The first says the kill
 827inhabitant has exactly the per-site jet shape, so the shape assumption is not
 828secretly excluding it; the second says its jet at `a = 0` is uncalibrated, so
 829the recognition clause is what excludes it. -/
 830
 831/-- The variable-kinetic kill inhabitant *is* a per-site jet profile: chart
 832`κ = 1`, log-curvatures `c a b = 2 / (1 + a ^ 2)`. So the shape assumed in this
 833section admits it. -/
 834theorem vacuumKineticLocalProfile_eq_perSiteJet :
 835    vacuumKineticLocalProfile
 836      = perSiteJetProfile (fun a _ => 2 * vacuumKineticA a) 1 vacuumKineticW := by
 837  funext a b p
 838  simp only [vacuumKineticLocalProfile, perSiteJetProfile]
 839  ring
 840
 841/-- Its jet at `a = 0` has log-curvature `2`, not `1`, so it is not calibrated.
 842This is the clause that excludes it, and §7's header explains why excluding it
 843this way is worth less than it looks. -/
 844theorem vacuumKinetic_jet_not_calibrated :
 845    ¬ Cost.FunctionalEquation.IsCalibrated (jetCost (2 * vacuumKineticA 0)) := by
 846  rw [isCalibrated_jetCost_iff]
 847  simp only [vacuumKineticA]
 848  norm_num
 849
 850/-- **The kill inhabitant is excluded by the recognition clause.** Together with
 851`not_HKTRigidityModVacuumStatementN2`, which says the rigidity conclusion is
 852false once this inhabitant is admitted, and with
 853`vacuumKineticLocalProfile_eq_perSiteJet`, which says the shape assumption alone
 854does admit it: deleting the calibration clause does not weaken the theorem, it
 855falsifies it. -/
 856theorem vacuumKinetic_not_calibratedJet :
 857    ¬ ∃ T : CalibratedJetCanonicalMom,
 858      T.target = vacuumKineticCanonicalMomTarget := by
 859  rintro ⟨T, hEq⟩
 860  exact vacuumKinetic_not_kineticNormalized ⟨T.toKineticNormalized, hEq⟩
 861
 862/-! ### The same primitive at the exact level
 863
 864The jet argument above uses calibration. At the exact level the composition law
 865does the corresponding job on its own: it admits no free cost weight at all, so
 866a weight that looks at the field is not a recognition cost at any site where it
 867differs from one. This is why §4's exclusion cannot be dodged by rescaling. -/
 868
 869/-- **The recognition composition law admits no free weight.** If `w * J`
 870satisfies the RCL then `w` is `0` or `1`. A single instance, `x = y = 2`,
 871already forces it. -/
 872theorem compositionLaw_forces_unit_weight (w : ℝ)
 873    (hComp : Cost.FunctionalEquation.SatisfiesCompositionLaw
 874      (fun x => w * Cost.Jcost x)) :
 875    w = 0 ∨ w = 1 := by
 876  have h := hComp 2 2 (by norm_num) (by norm_num)
 877  have e4 : Cost.Jcost (2 * 2) = 9 / 8 := by norm_num [Cost.Jcost]
 878  have e1 : Cost.Jcost (2 / 2) = 0 := by norm_num [Cost.Jcost]
 879  have e2 : Cost.Jcost 2 = 1 / 4 := by norm_num [Cost.Jcost]
 880  simp only [e4, e1, e2] at h
 881  have hquad : w * (w - 1) = 0 := by nlinarith [h]
 882  rcases mul_eq_zero.mp hquad with h0 | h1
 883  · exact Or.inl h0
 884  · exact Or.inr (by linarith)
 885
 886/-- A field-dependent cost weight is not a family of recognition costs unless it
 887is constantly one. -/
 888theorem rcl_forces_field_independent_weight (W : ℝ → ℝ → ℝ)
 889    (hComp : ∀ a b : ℝ, Cost.FunctionalEquation.SatisfiesCompositionLaw
 890      (fun x => W a b * Cost.Jcost x))
 891    (hne : ∀ a b : ℝ, W a b ≠ 0) (a b : ℝ) : W a b = 1 :=
 892  (compositionLaw_forces_unit_weight (W a b) (hComp a b)).resolve_left (hne a b)
 893
 894/-! ## §8. The exact recognition cost, in the chart where it is quadratic
 895
 896§4 excluded the exact cost. That exclusion is real but narrower than its old
 897name: it excludes the *linear* chart `t = κ p`, in which the response is `sinh`
 898and cannot be linear. The chart is not forced, and there is one in which the
 899exact cost is quadratic on the nose. The recognition cost has the half-imbalance
 900form `J (exp t) = 2 * sinh (t / 2) ^ 2`, so identify the momentum with the
 901half-imbalance *sine* rather than with the imbalance itself,
 902`sinh (t / 2) = λ p`, equivalently `t = 2 * arsinh (λ p)`. Then
 903
 904    J (exp (2 * arsinh (λ p))) = 2 * λ ^ 2 * p ^ 2
 905
 906exactly, with no truncation and no jet (`Jlog_two_arsinh`). The exact recognition
 907cost inhabits the undeformed `CanonicalMom` algebra, §5's concession that only the
 908balance jet survives was an artifact of the linear chart, and open item 2 of this
 909module, the deformed algebra, is not needed for this purpose.
 910
 911That removes the truncation but not the field dependence, since the cost weight
 912`W a b` is still free. Here the load is carried by the Recognition Composition
 913Law, and carried as a theorem rather than as a definition: `w * J` satisfies the
 914law only for `w` in `{0, 1}` (`compositionLaw_forces_unit_weight`), because a
 915rescaled recognition cost is not a recognition cost. Imposing the law site by
 916site therefore forces unit weight at every site, which is field-independence, and
 917it forces the sign, so `cKin = 2 * λ ^ 2 > 0`.
 918
 919Why this is not §7 again. §7's clause was calibration of a family this module
 920itself defined; its unique solution is read off by unfolding a definition, its
 921value is absorbed by the free chart, and `jetCost_not_rcl` proves the family was
 922not a recognition cost at all. §8's clause is a nonlinear functional equation on
 923the repo's own `Cost.Jcost`, its unique solution is a theorem, and the
 924countermodel is exact rather than illustrative: delete the clause, take chart
 925`λ = 1/2` and weights `W a = 2 / (1 + a ^ 2)`, and the profile *is* the kill
 926inhabitant (`vacuumKineticLocalProfile_eq_exactCost`), which
 927`not_HKTRigidityModVacuumStatementN2` refutes. The exclusion is also proved
 928directly from the clause rather than routed through the older one
 929(`no_rcl_presentation_of_vacuumKinetic`).
 930
 931What remains assumed is the whole of what remains: the chart is one global
 932constant `λ`. A site-dependent `λ a b` reproduces the kill inhabitant at unit
 933weight, so the momentum-channel identification is not discharged, and `λ` is
 934unfixed, so `cKin = 2 λ ^ 2` is a positivity statement and not a number.
 935Recognition supplies two facts the algebra does not: the cost weight cannot vary
 936from site to site, and it cannot be negative. It does not supply the magnitude.
 937-/
 938
 939/-- **The recognition cost is exactly quadratic in the half-imbalance sine.**
 940`J (exp t) = 2 * sinh (t / 2) ^ 2`, so at `t = 2 * arsinh u` the cost is `2 u ^ 2`
 941with no truncation. This is the identity that repairs §4's chart. -/
 942theorem Jlog_two_arsinh (u : ℝ) : Cost.Jlog (2 * Real.arsinh u) = 2 * u ^ 2 := by
 943  have hbase := Real.cosh_sq_sub_sinh_sq (Real.arsinh u)
 944  rw [Real.sinh_arsinh] at hbase
 945  rw [Cost.Jlog_as_cosh, Real.cosh_two_mul, Real.sinh_arsinh]
 946  linarith
 947
 948/-- A density posting the *exact* recognition cost of the momentum channel, read
 949in the half-imbalance-sine chart, with a per-site cost weight `W a b` that is
 950free to look at the field. -/
 951def exactCostKineticProfile (W : ℝ → ℝ → ℝ) (lam : ℝ) (U : ℝ → ℝ → ℝ) :
 952    LocalHamProfile :=
 953  fun a b p => W a b * Cost.Jlog (2 * Real.arsinh (lam * p)) + U a b
 954
 955theorem exactCostKineticProfile_quadratic
 956    (W : ℝ → ℝ → ℝ) (lam : ℝ) (U : ℝ → ℝ → ℝ) (a b p : ℝ) :
 957    exactCostKineticProfile W lam U a b p
 958      = W a b * (2 * (lam * p) ^ 2) + U a b := by
 959  rw [exactCostKineticProfile, Jlog_two_arsinh]
 960
 961/-- A `CanonicalMom` target posting the exact recognition cost of the momentum
 962channel, with every site's cost weight required to satisfy the Recognition
 963Composition Law. Field-independence is absent from the hypothesis. -/
 964structure RCLKineticCanonicalMom where
 965  target : HKTPointSplitTargetDynCanonicalMom
 966  rcl_kinetic :
 967    ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (W : ℝ → ℝ → ℝ) (lam : ℝ)
 968      (U : ℝ → ℝ → ℝ),
 969      ContDiff ℝ 2 (profileMap h) ∧ lam ≠ 0 ∧ (∀ a b : ℝ, W a b ≠ 0) ∧
 970        (∀ (x : PhaseSpace 2) (j : ZMod 2),
 971          target.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
 972          (∀ a b p : ℝ, h a b p = exactCostKineticProfile W lam U a b p) ∧
 973          (∀ a b : ℝ, Cost.FunctionalEquation.SatisfiesCompositionLaw
 974            (fun x => W a b * Cost.Jcost x))
 975
 976/-- **Field-independence, derived from the composition law.** The law forces unit
 977weight at every site, so the momentum response is `4 λ ^ 2 p` everywhere, which is
 978the disclosed premise with `cKin = 2 λ ^ 2`. -/
 979theorem rclKinetic_hp_eq_linear
 980    (h : LocalHamProfile) (S : LocalHamSmooth h) (W : ℝ → ℝ → ℝ) (lam : ℝ)
 981    (U : ℝ → ℝ → ℝ)
 982    (hcd : ContDiff ℝ 2 (profileMap h))
 983    (hW : ∀ a b : ℝ, W a b ≠ 0)
 984    (hProf : ∀ a b p : ℝ, h a b p = exactCostKineticProfile W lam U a b p)
 985    (hRCL : ∀ a b : ℝ, Cost.FunctionalEquation.SatisfiesCompositionLaw
 986      (fun x => W a b * Cost.Jcost x))
 987    (a b p : ℝ) :
 988    S.hp a b p = (2 * (2 * lam ^ 2)) * p := by
 989  have hw : W a b = 1 := rcl_forces_field_independent_weight W hRCL hW a b
 990  have hS := hasDerivAt_hp_of_normalized h S hcd a b p
 991  have hfun : (fun t => h a b t) = fun t => 2 * (lam * t) ^ 2 + U a b := by
 992    funext t
 993    rw [hProf a b t, exactCostKineticProfile_quadratic, hw, one_mul]
 994  rw [hfun] at hS
 995  have hinner : HasDerivAt (fun t : ℝ => lam * t) lam p := by
 996    simpa using (hasDerivAt_id p).const_mul lam
 997  have hsq : HasDerivAt (fun t : ℝ => (lam * t) ^ 2) (2 * (lam * p) * lam) p := by
 998    simpa using hinner.pow 2
 999  have htwo := hsq.const_mul (2 : ℝ)
1000  rw [show (2 : ℝ) * (2 * (lam * p) * lam) = (2 * (2 * lam ^ 2)) * p by ring] at htwo
1001  exact hS.unique (htwo.add_const (U a b))
1002
1003/-- **Recognition fixes the sign.** The composition law admits no negative
1004weight, and the chart contributes a square, so the kinetic coefficient is
1005strictly positive. -/
1006theorem rclKinetic_cKin_pos {lam : ℝ} (hlam : lam ≠ 0) : 0 < 2 * lam ^ 2 := by
1007  have h1 : 0 < lam ^ 2 := by
1008    rcases hlam.lt_or_gt with h | h <;> nlinarith
1009  linarith
1010
1011theorem rclKinetic_cKin_ne_zero {lam : ℝ} (hlam : lam ≠ 0) : 2 * lam ^ 2 ≠ 0 :=
1012  ne_of_gt (rclKinetic_cKin_pos hlam)
1013
1014def RCLKineticCanonicalMom.toKineticNormalized
1015    (T : RCLKineticCanonicalMom) : KineticNormalizedCanonicalMom where
1016  target := T.target
1017  kinetic_normalized := by
1018    obtain ⟨h, S, W, lam, U, hcd, hlam, hW, hHam, hProf, hRCL⟩ := T.rcl_kinetic
1019    exact ⟨h, S, 2 * lam ^ 2, hcd, rclKinetic_cKin_ne_zero hlam, hHam,
1020      rclKinetic_hp_eq_linear h S W lam U hcd hW hProf hRCL⟩
1021
1022/-- Full ADM rigidity for targets posting the exact recognition cost. -/
1023theorem rclKinetic_ADM_rigidity (T : RCLKineticCanonicalMom) :
1024    ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
1025      cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
1026        (∀ (x : PhaseSpace 2) (j : ZMod 2),
1027          T.target.hamDensity x j =
1028            cKin * (x.2 j * x.2 j) +
1029              cGrad *
1030                (T.target.structureFunction x j *
1031                  ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
1032              V (x.1 j)) ∧
1033        (∀ (x : PhaseSpace 2) (j : ZMod 2),
1034          T.target.momDensity x j =
1035            cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
1036  HKTRigidityKineticNormalizedN2_holds T.toKineticNormalized
1037
1038/-- The kinetic coefficient of any target in the class is strictly positive, so
1039recognition rules out the wrong-sign kinetic term as well as the field-dependent
1040one. -/
1041theorem rclKinetic_positive_kinetic_coefficient (T : RCLKineticCanonicalMom) :
1042    ∃ cKin : ℝ, 0 < cKin ∧
1043      ∃ (h : LocalHamProfile) (S : LocalHamSmooth h),
1044        ∀ a b p : ℝ, S.hp a b p = (2 * cKin) * p := by
1045  obtain ⟨h, S, W, lam, U, hcd, hlam, hW, hHam, hProf, hRCL⟩ := T.rcl_kinetic
1046  exact ⟨2 * lam ^ 2, rclKinetic_cKin_pos hlam, h, S,
1047    rclKinetic_hp_eq_linear h S W lam U hcd hW hProf hRCL⟩
1048
1049/-- **The class is nonempty.** The ADM anchor posts the exact recognition cost at
1050unit weight in the chart `λ = 1/2`, and its composition-law clause is the repo's
1051own theorem that `J` satisfies the law.
1052
1053`λ = 1/2` **is** a fit, and an earlier version of this docstring claimed the
1054opposite. The chart constant is free, `cKin = 2 λ²`, and the value `1/2` was
1055chosen because it is what reproduces the anchor's coefficient. What is not
1056fitted is the weight, which the composition law forces to one, and the sign,
1057which `rclKinetic_cKin_pos` forces positive. The magnitude is open; see the
1058module header. -/
1059def hamDynRCLKinetic : RCLKineticCanonicalMom where
1060  target := hamDynPointSplitTargetCanonicalMom
1061  rcl_kinetic := by
1062    refine ⟨hamDynLocalProfile, hamDynLocalSmooth, (fun _ _ => 1), (1 / 2 : ℝ),
1063      (fun a b => (1 / 2 : ℝ) * ((1 + a * a) * ((b - a) * (b - a)))),
1064      hamDynLocalProfile_contDiff2, by norm_num, (fun _ _ => one_ne_zero),
1065      hamDynDensity_eq_localProfile, ?_, ?_⟩
1066    · intro a b p
1067      rw [exactCostKineticProfile_quadratic]
1068      simp only [hamDynLocalProfile]
1069      ring
1070    · intro _ _
1071      simpa only [one_mul] using
1072        Cost.SymplecticAction.jcost_satisfiesCompositionLaw_via_symplectic
1073
1074instance : Nonempty RCLKineticCanonicalMom := ⟨hamDynRCLKinetic⟩
1075
1076theorem hamDyn_satisfies_rclKinetic :
1077    ∃ cKin cGrad cMom : ℝ, ∃ V : ℝ → ℝ,
1078      cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
1079        (∀ (x : PhaseSpace 2) (j : ZMod 2),
1080          hamDynRCLKinetic.target.hamDensity x j =
1081            cKin * (x.2 j * x.2 j) +
1082              cGrad *
1083                (hamDynRCLKinetic.target.structureFunction x j *
1084                  ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
1085              V (x.1 j)) ∧
1086        (∀ (x : PhaseSpace 2) (j : ZMod 2),
1087          hamDynRCLKinetic.target.momDensity x j =
1088            cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
1089  rclKinetic_ADM_rigidity hamDynRCLKinetic
1090
1091/-! ### The removal test, exact this time -/
1092
1093/-- **Deleting the composition-law clause readmits the kill inhabitant exactly.**
1094At chart `λ = 1/2` with weights `W a b = 2 / (1 + a ^ 2)`, the exact-cost profile
1095*is* `vacuumKineticLocalProfile`. Nothing is approximated and nothing is
1096illustrative: the shape without the clause contains the very target that
1097`not_HKTRigidityModVacuumStatementN2` uses to refute rigidity. -/
1098theorem vacuumKineticLocalProfile_eq_exactCost :
1099    vacuumKineticLocalProfile
1100      = exactCostKineticProfile (fun a _ => 2 * vacuumKineticA a) (1 / 2)
1101          vacuumKineticW := by
1102  funext a b p
1103  rw [exactCostKineticProfile_quadratic]
1104  simp only [vacuumKineticLocalProfile]
1105  ring
1106
1107/-- Those weights are not recognition costs: at `a = 0` the weight is `2`, and
1108the composition law admits only `0` and `1`. -/
1109theorem vacuumKinetic_weight_not_rcl :
1110    ¬ Cost.FunctionalEquation.SatisfiesCompositionLaw
1111      (fun x => (2 * vacuumKineticA 0) * Cost.Jcost x) := by
1112  intro hComp
1113  rcases compositionLaw_forces_unit_weight _ hComp with h | h <;>
1114    · rw [show vacuumKineticA 0 = 1 by simp [vacuumKineticA]] at h
1115      norm_num at h
1116
1117/-- **Direct exclusion, consuming the clause.** No composition-law-certified
1118presentation of the kill inhabitant's profile exists, in any chart. This does not
1119route through the older kinetic-normalization exclusion: the law forces unit
1120weight, and then two field values disagree about the coefficient. -/
1121theorem no_rcl_presentation_of_vacuumKinetic
1122    (W : ℝ → ℝ → ℝ) (lam : ℝ) (U : ℝ → ℝ → ℝ)
1123    (hW : ∀ a b : ℝ, W a b ≠ 0)
1124    (hRCL : ∀ a b : ℝ, Cost.FunctionalEquation.SatisfiesCompositionLaw
1125      (fun x => W a b * Cost.Jcost x)) :
1126    vacuumKineticLocalProfile ≠ exactCostKineticProfile W lam U := by
1127  intro hEq
1128  have hval : ∀ a b p : ℝ,
1129      vacuumKineticA a * (p * p) + vacuumKineticW a b
1130        = 2 * (lam * p) ^ 2 + U a b := by
1131    intro a b p
1132    have h := congrFun (congrFun (congrFun hEq a) b) p
1133    rw [exactCostKineticProfile_quadratic,
1134      rcl_forces_field_independent_weight W hRCL hW a b, one_mul] at h
1135    exact h
1136  have hU : ∀ a b : ℝ, vacuumKineticW a b = U a b := by
1137    intro a b
1138    have h := hval a b 0
1139    nlinarith [h]
1140  have hA : ∀ a : ℝ, vacuumKineticA a = 2 * lam ^ 2 := by
1141    intro a
1142    have h := hval a 0 1
1143    have hu := hU a 0
1144    nlinarith [h, hu]
1145  have h0 := hA 0
1146  have h1 := hA 1
1147  rw [show vacuumKineticA 0 = 1 by simp [vacuumKineticA]] at h0
1148  rw [show vacuumKineticA 1 = 1 / 2 by norm_num [vacuumKineticA]] at h1
1149  linarith
1150
1151/-- **§7's family was not a recognition cost.** For every nonzero curvature the
1152jet family violates the composition law, the residual being
1153`-(c ^ 2 / 2) * (log x) ^ 2 * (log y) ^ 2`; at `x = y = e` the two sides are
1154`2 * c` and `c ^ 2 / 2 + 2 * c`. Calibration alone does not make an object a
1155recognition cost, which is the second reason §7 does not carry the load and §8
1156imposes the law itself. -/
1157theorem jetCost_not_rcl (c : ℝ) (hc : c ≠ 0) :
1158    ¬ Cost.FunctionalEquation.SatisfiesCompositionLaw (jetCost c) := by
1159  intro hComp
1160  have h := hComp (Real.exp 1) (Real.exp 1) (Real.exp_pos 1) (Real.exp_pos 1)
1161  have hmul : Real.exp 1 * Real.exp 1 = Real.exp 2 := by
1162    rw [← Real.exp_add]; norm_num
1163  have hdiv : Real.exp 1 / Real.exp 1 = 1 := div_self (Real.exp_ne_zero 1)
1164  rw [hmul, hdiv] at h
1165  simp only [jetCost, Real.log_exp, Real.log_one] at h
1166  have hc2 : c * c = 0 := by nlinarith [h]
1167  rcases mul_eq_zero.mp hc2 with h' | h' <;> exact hc h'
1168
1169/-! ## §9. Axiom audit -/
1170
1171#print axioms exists_structure_value_ne_zero
1172#print axioms kinetic_normalization_of_universal_response
1173#print axioms kinetic_coefficient_unique
1174#print axioms HKTRigidityUniversalKineticN2_holds
1175#print axioms universal_of_channelSeparated
1176#print axioms channelSeparated_of_universal
1177#print axioms costKinetic_hp_eq_sinh
1178#print axioms costKinetic_universal
1179#print axioms sinh_not_linear
1180#print axioms no_exact_cost_kinetic_canonicalMom
1181#print axioms recogCurvature_eq_one
1182#print axioms deriv2_Jlog_zero_eq_recogCurvature
1183#print axioms JlogQuad_matches_Jlog_to_second_order
1184#print axioms quadCost_hp_eq_linear
1185#print axioms quadCost_ADM_rigidity
1186#print axioms vacuumKinetic_not_universalKinetic
1187#print axioms hamDyn_satisfies_universalKinetic
1188#print axioms isCalibrated_jetCost_iff
1189#print axioms G_jetCost_recogCurvature
1190#print axioms isCalibrated_iff_density_curvature
1191#print axioms calibratedJet_hp_eq_linear
1192#print axioms calibratedJet_ADM_rigidity
1193#print axioms hamDyn_satisfies_calibratedJet
1194#print axioms vacuumKineticLocalProfile_eq_perSiteJet
1195#print axioms vacuumKinetic_jet_not_calibrated
1196#print axioms vacuumKinetic_not_calibratedJet
1197#print axioms compositionLaw_forces_unit_weight
1198#print axioms rcl_forces_field_independent_weight
1199#print axioms Jlog_two_arsinh
1200#print axioms exactCostKineticProfile_quadratic
1201#print axioms rclKinetic_hp_eq_linear
1202#print axioms rclKinetic_cKin_pos
1203#print axioms rclKinetic_ADM_rigidity
1204#print axioms rclKinetic_positive_kinetic_coefficient
1205#print axioms hamDyn_satisfies_rclKinetic
1206#print axioms vacuumKineticLocalProfile_eq_exactCost
1207#print axioms vacuumKinetic_weight_not_rcl
1208#print axioms no_rcl_presentation_of_vacuumKinetic
1209#print axioms jetCost_not_rcl
1210
1211end
1212
1213end HKTKineticFromRecognitionCost
1214end SevenGaps
1215end Gravity
1216end IndisputableMonolith
1217