IndisputableMonolith.Gravity.SevenGaps.Gap5ReparamAttackOnConstraintSector

   1import IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost
   2
   3/-!
   4# Campaign 2 Track A: the reparametrization attack on the constraint sector
   5
   6`HKTKineticFromRecognitionCost` §8 derives field-independence of the kinetic
   7weight from the Recognition Composition Law (RCL). The paper built on it,
   8`papers/QG_Constraint_Sector_Recognition_Premise_20260725.tex`, printed a
   9falsifier it had not run:
  10
  11> Exhibit a weight functional that is NOT `SatisfiesCompositionLaw`, satisfies
  12> the remaining clauses of the model class, and still forces unit weight.
  13
  14The same attack killed the framing of O5 (`Gap1ClassLengthsFromRecognitionCost`
  15§5b), where a strictly increasing reparametrization of the recognition cost
  16reproduced every rung of the ladder while violating the composition law, so the
  17ladder could not identify `J`. The paper's stated reason to expect the attack to
  18fail here was that §8's conclusion is a functional form rather than a level set.
  19This module settles it. The reason was wrong, and the attack lands, though at
  20lower severity than in O5.
  21
  22## What is established
  23
  24**§1. The forcing never looks at the recognition cost.** The proof of
  25`compositionLaw_forces_unit_weight` in §8 evaluates at the single point
  26`x = y = 2` and uses three numerical values of `J`. That is an artifact of the
  27proof, not of the theorem: `compositionLaw_forces_unit_weight_generic` shows the
  28same conclusion for an arbitrary `F` satisfying the law, with the only input
  29being that `F` is nonzero somewhere. The mechanism is that the law is quadratic
  30in the function, so scaling by `w` produces `w ^ 2 = w` on the quadratic term
  31and `w = w` on the linear ones. `Cost.Jcost` is not used.
  32
  33**§2. The law does not pin the recognition cost.** Substituting `x ↦ x ^ n`
  34carries solutions to solutions (`satisfiesCompositionLaw_comp_pow`), so
  35`fun x => J (x ^ n)` satisfies the law for every `n`, and differs from `J` for
  36`n ≥ 2` (`powCost_two_ne_Jcost`). Each member is a strictly increasing
  37reparametrization of `J` on `[1, ∞)`, since `J (x ^ n)` is `T n` applied to
  38`J x + 1`, minus one, with `T n` the Chebyshev polynomial. So the orbit under
  39reparametrization is nontrivial and lands inside the law's solution set rather
  40than outside it.
  41
  42This is the invariance test that Campaign 1's third acceptance rule demands, and
  43§8 fails it: the tested property is invariant under a group action that moves
  44`J`, so the test cannot pin `J`.
  45
  46**§3. Calibration, not recognition, is the discriminator.** Within the power
  47family the second log-derivative at the origin is `n ^ 2`
  48(`deriv2_G_powCost`), so exactly one member is calibrated
  49(`isCalibrated_powCost_iff`). This is the Lean form of what
  50`Cost.FunctionalEquation.law_of_logic_forces_jcost_with_regularization` already
  51required and §8 dropped: the uniqueness theorem for `J` takes RCL *and*
  52calibration, and §8 imposes only the first half.
  53
  54**§4. The falsifier as printed is met, and was ill-posed.** A one-point
  55normalization `w * J 2 = J 2` is not the composition law, leaves the other
  56clauses untouched, and forces `w = 1` on the nose, which is strictly sharper
  57than RCL's `w ∈ {0, 1}` (`calibratedWeightAtTwo_forces_one`). The two clauses
  58are genuinely different predicates: `w = 0` satisfies RCL's and not this one
  59(`rclWeight_zero`, `not_calibratedWeightAtTwo_zero`). So the falsifier is
  60satisfied by a cheaper clause, which means the falsifier as written could never
  61have discriminated: any predicate implying `w = 1` meets it, including `w = 1`.
  62Recorded as a defect in the paper's gate, not as a defect in its theorem.
  63
  64## §4b. Neither clause carries recognition content
  65
  66This module's first conclusion was a division of labour: the composition law buys
  67unit weight by generic algebra, and the recognition cost buys quadraticity of the
  68momentum sector, where it is not replaceable. A cross-family hostile panel
  69attacked that conclusion and the second half did not survive.
  70
  71The profile clause reads the cost in the chart `t = 2 arsinh (λ p)`, and that chart
  72is `J`'s own inverse: `chart_alone_forces_the_cost` proves that *any* function
  73exactly quadratic in it is a multiple of the cost, using no functional equation, no
  74regularity and no positivity. So the clause is a uniqueness theorem for the cost
  75wearing the clothes of a physical premise, its solution set is the one-parameter
  76scale family (`profile_clause_solution_set_is_a_scale_family`), and no substitution
  77into it could ever have succeeded. `oscCost_not_quadratic_in_log_chart` is
  78therefore true and nearly empty: it is one instance of a general fact that leaves
  79recognition out of it.
  80
  81Worse for the attribution, the chart is *typed in*. `exactCostKineticProfile`
  82writes `2 * Real.arsinh (lam * p)` as a literal and nothing derives it from the
  83substrate, so the clause does not derive a quadratic momentum sector from
  84recognition; it writes down a quadratic in a coordinate chosen to make the cost
  85look quadratic. The coefficient `2 λ ^ 2` is the double-angle identity.
  86
  87So the corrected reading of §8: the law clause contributes one bit (`w ^ 2 = w`) by
  88algebra generic to any equation quadratic in the unknown function, the profile
  89clause contributes a change of variables, and field-independence needs the model
  90class's separate nonvanishing clause `∀ a b, W a b ≠ 0` on top of the law, since
  91the law alone permits a field-dependent weight valued in `{0, 1}`. Nothing in
  92either clause is recognition-specific.
  93
  94## Scope
  95
  96The theorems are untouched. `RCLKineticCanonicalMom` is still inhabited, its
  97conclusion still holds, and the clause still excludes the kill inhabitant
  98(`no_rcl_presentation_of_vacuumKinetic`). What changes is what may be claimed about
  99why, and the claim shrinks to nothing on the recognition side.
 100
 101The power family here is indexed by natural exponents; the real-exponent family
 102`J (x ^ c)` would need `rpow` and is not formalized. The one thing that would
 103restore recognition content to the profile clause is a derivation of the
 104half-imbalance chart from the substrate rather than a stipulation of it. That is
 105the open successor, and it is now the only route by which this sector can carry
 106recognition content at all.
 107-/
 108
 109namespace IndisputableMonolith
 110namespace Gravity
 111namespace SevenGaps
 112namespace ConstraintSectorReparamAttack
 113
 114open IndisputableMonolith.Cost.FunctionalEquation
 115
 116/-- `Cost.Jcost` satisfies the composition law, routed through the repo's own
 117cosh-addition identity so this module stays on `FunctionalEquation`'s import
 118path rather than pulling in `CostUniqueness`. -/
 119theorem jcost_rcl : SatisfiesCompositionLaw Cost.Jcost :=
 120  (composition_law_equiv_coshAdd Cost.Jcost).2 Jcost_cosh_add_identity
 121
 122/-! ## §1. The forcing never looks at the recognition cost -/
 123
 124/-- **The composition law forces unit weight for any of its solutions.**
 125
 126If `F` satisfies the law and `w * F` satisfies it too, then `w` is `0` or `1`,
 127provided `F` is nonzero at some pair of points. No property of `Cost.Jcost`
 128beyond membership in the solution set is used.
 129
 130The mechanism: the law is quadratic in the function, so the scaling passes
 131through the linear terms as `w` and through the product term as `w ^ 2`,
 132leaving `w ^ 2 = w` once a nonvanishing product is available. -/
 133theorem compositionLaw_forces_unit_weight_generic (F : ℝ → ℝ) (w : ℝ)
 134    (hF : SatisfiesCompositionLaw F)
 135    (hwF : SatisfiesCompositionLaw (fun x => w * F x))
 136    {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hne : F x * F y ≠ 0) :
 137    w = 0 ∨ w = 1 := by
 138  have h1 := hF x y hx hy
 139  have h2 := hwF x y hx hy
 140  simp only at h2
 141  have hkey : (w * (w - 1)) * (2 * (F x * F y)) = 0 := by
 142    linear_combination w * h1 - h2
 143  have hfac : w * (w - 1) = 0 := by
 144    rcases mul_eq_zero.mp hkey with h | h
 145    · exact h
 146    · exact absurd (by linarith : F x * F y = 0) hne
 147  rcases mul_eq_zero.mp hfac with h | h
 148  · exact Or.inl h
 149  · exact Or.inr (by linarith)
 150
 151/-- The repo's §8 lemma is the `F = Cost.Jcost` instance of the generic one, so
 152the recognition cost was never load-bearing for that step. -/
 153theorem compositionLaw_forces_unit_weight_is_an_instance (w : ℝ)
 154    (hComp : SatisfiesCompositionLaw (fun x => w * Cost.Jcost x)) :
 155    w = 0 ∨ w = 1 :=
 156  compositionLaw_forces_unit_weight_generic Cost.Jcost w
 157    jcost_rcl hComp
 158    (x := 2) (y := 2) (by norm_num) (by norm_num)
 159    (by norm_num [Cost.Jcost])
 160
 161/-! ## §2. The law does not pin the recognition cost -/
 162
 163/-- **Argument rescaling carries solutions to solutions.** The law only sees the
 164multiplicative structure of the argument, and `x ↦ x ^ n` is a monoid
 165endomorphism of the positive reals, so it acts on the solution set. -/
 166theorem satisfiesCompositionLaw_comp_pow (F : ℝ → ℝ) (n : ℕ)
 167    (hF : SatisfiesCompositionLaw F) :
 168    SatisfiesCompositionLaw (fun x => F (x ^ n)) := by
 169  intro x y hx hy
 170  simp only
 171  rw [mul_pow, div_pow]
 172  exact hF (x ^ n) (y ^ n) (pow_pos hx n) (pow_pos hy n)
 173
 174/-- The `n`-th member of the power family: the recognition cost read at a
 175rescaled argument. `powCost 1` is `Cost.Jcost` and `powCost 0` is the zero
 176solution. -/
 177noncomputable def powCost (n : ℕ) : ℝ → ℝ := fun x => Cost.Jcost (x ^ n)
 178
 179theorem powCost_one : powCost 1 = Cost.Jcost := by
 180  funext x; simp [powCost]
 181
 182/-- Every member of the family satisfies the composition law. -/
 183theorem powCost_satisfiesCompositionLaw (n : ℕ) :
 184    SatisfiesCompositionLaw (powCost n) :=
 185  satisfiesCompositionLaw_comp_pow Cost.Jcost n
 186    jcost_rcl
 187
 188/-- The family is not constant: the square member already differs from `J`. -/
 189theorem powCost_two_ne_Jcost : powCost 2 ≠ Cost.Jcost := by
 190  intro h
 191  have := congrArg (fun f => f 2) h
 192  norm_num [powCost, Cost.Jcost] at this
 193
 194/-- `J` is strictly positive above one, which is the nonvanishing input §1
 195needs. -/
 196theorem Jcost_pos_of_one_lt {x : ℝ} (hx : 1 < x) : 0 < Cost.Jcost x := by
 197  have hx0 : (0 : ℝ) < x := lt_trans one_pos hx
 198  have hsq : 0 < (x - 1) ^ 2 := pow_pos (by linarith) 2
 199  have hinv : x⁻¹ * x = 1 := inv_mul_cancel₀ (ne_of_gt hx0)
 200  simp only [Cost.Jcost]
 201  nlinarith [hsq, hinv, hx0]
 202
 203/-- **The whole family forces unit weight.** So the conclusion §8 draws is
 204constant along the orbit, which is why the attack does not damage the theorem
 205even though it damages the attribution. -/
 206theorem powCost_forces_unit_weight (n : ℕ) (hn : n ≠ 0) (w : ℝ)
 207    (hw : SatisfiesCompositionLaw (fun x => w * powCost n x)) :
 208    w = 0 ∨ w = 1 := by
 209  have hpow : ∀ m : ℕ, (1 : ℝ) ≤ (2 : ℝ) ^ m := by
 210    intro m
 211    induction m with
 212    | zero => norm_num
 213    | succ k ih => rw [pow_succ]; nlinarith
 214  have h2 : (1 : ℝ) < (2 : ℝ) ^ n := by
 215    obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
 216    rw [pow_succ]
 217    nlinarith [hpow m]
 218  have hpos : 0 < powCost n 2 := Jcost_pos_of_one_lt h2
 219  exact compositionLaw_forces_unit_weight_generic (powCost n) w
 220    (powCost_satisfiesCompositionLaw n) hw
 221    (x := 2) (y := 2) (by norm_num) (by norm_num)
 222    (by positivity)
 223
 224/-! ## §2b. The law admits solutions that are not costs at all
 225
 226The power family stays inside the recognition family, which would make the
 227attack mild. The oscillatory branch of d'Alembert does not, and it is the reason
 228the verdict below is not mild. `cos (c log x) - 1` satisfies the composition
 229law, takes negative values, and so is not a cost under any reading, yet it
 230forces unit weight exactly as `J` does.
 231
 232What it cannot do is the other half of §8's job. `J` was chosen for the chart
 233identity `J (exp (2 arsinh u)) = 2 u ^ 2`, which is what makes the momentum
 234sector quadratic and hence the response linear. The oscillatory solution is
 235bounded, so no such identity exists for it
 236(`oscCost_not_quadratic_in_log_chart`). That is the division of labour, and
 237stating it is the substantive result of this track: the composition law buys
 238unit weight and knows nothing about recognition, while the recognition cost's
 239own functional form buys quadraticity and is not replaceable. -/
 240
 241/-- The oscillatory branch of the d'Alembert solution set. -/
 242noncomputable def oscCost (c : ℝ) : ℝ → ℝ :=
 243  fun x => Real.cos (c * Real.log x) - 1
 244
 245/-- **The oscillatory branch satisfies the composition law.** The law is the
 246cosine addition identity in disguise as much as it is the hyperbolic one. -/
 247theorem oscCost_satisfiesCompositionLaw (c : ℝ) :
 248    SatisfiesCompositionLaw (oscCost c) := by
 249  intro x y hx hy
 250  have hx0 : x ≠ 0 := ne_of_gt hx
 251  have hy0 : y ≠ 0 := ne_of_gt hy
 252  simp only [oscCost, Real.log_mul hx0 hy0, Real.log_div hx0 hy0, mul_add,
 253    mul_sub, Real.cos_add, Real.cos_sub]
 254  ring
 255
 256/-- It takes the value `-2`, so it is not a cost: `Cost.Jcost` and every
 257recognition cost is nonnegative on the positive reals. -/
 258theorem oscCost_neg_at_exp_pi : oscCost 1 (Real.exp Real.pi) = -2 := by
 259  simp [oscCost, Real.log_exp]
 260  norm_num
 261
 262/-- **A non-cost forces unit weight just as well.** So the forcing step cannot
 263be reading any recognition content out of the clause. -/
 264theorem oscCost_forces_unit_weight (w : ℝ)
 265    (hw : SatisfiesCompositionLaw (fun x => w * oscCost 1 x)) :
 266    w = 0 ∨ w = 1 := by
 267  have hx : (0 : ℝ) < Real.exp Real.pi := Real.exp_pos _
 268  refine compositionLaw_forces_unit_weight_generic (oscCost 1) w
 269    (oscCost_satisfiesCompositionLaw 1) hw hx hx ?_
 270  rw [oscCost_neg_at_exp_pi]
 271  norm_num
 272
 273/-- **But it cannot make the momentum sector quadratic.** `J` earns its place in
 274the model class through the chart identity `Jlog_two_arsinh`; the oscillatory
 275solution is bounded and admits no such identity, in the log chart or any
 276rescaling of it. This is what the composition law alone does not supply. -/
 277theorem oscCost_not_quadratic_in_log_chart :
 278    ¬ ∃ c : ℝ, ∀ t : ℝ, oscCost 1 (Real.exp t) = c * t ^ 2 := by
 279  rintro ⟨c, hc⟩
 280  have h2pi := hc (2 * Real.pi)
 281  have hpi := hc Real.pi
 282  simp only [oscCost, Real.log_exp, one_mul, Real.cos_two_pi, Real.cos_pi] at h2pi hpi
 283  have hc0 : c = 0 := by
 284    have hne : (2 * Real.pi) ^ 2 ≠ 0 := by positivity
 285    have : c * (2 * Real.pi) ^ 2 = 0 := by linarith
 286    exact by
 287      rcases mul_eq_zero.mp this with h | h
 288      · exact h
 289      · exact absurd h hne
 290  rw [hc0] at hpi
 291  norm_num at hpi
 292
 293/-! ## §3. Calibration, not recognition, is the discriminator -/
 294
 295/-- In the logarithmic chart the family is `cosh (n t) - 1`. -/
 296theorem G_powCost (n : ℕ) (t : ℝ) :
 297    G (powCost n) t = Real.cosh ((n : ℝ) * t) - 1 := by
 298  simp only [G, powCost, Cost.Jcost]
 299  rw [← Real.exp_nat_mul, Real.cosh_eq, ← Real.exp_neg]
 300
 301/-- The log-curvature of the `n`-th member is `n ^ 2`. -/
 302theorem deriv2_G_powCost (n : ℕ) :
 303    deriv (deriv (G (powCost n))) 0 = (n : ℝ) ^ 2 := by
 304  have hG : G (powCost n) = fun t => Real.cosh ((n : ℝ) * t) - 1 :=
 305    funext (G_powCost n)
 306  have hfirst : deriv (fun t : ℝ => Real.cosh ((n : ℝ) * t) - 1)
 307      = fun t : ℝ => Real.sinh ((n : ℝ) * t) * (n : ℝ) := by
 308    funext t
 309    have hin : HasDerivAt (fun s : ℝ => (n : ℝ) * s) (n : ℝ) t := by
 310      simpa using (hasDerivAt_id t).const_mul ((n : ℝ))
 311    exact (hin.cosh.sub_const 1).deriv
 312  have hin0 : HasDerivAt (fun s : ℝ => (n : ℝ) * s) (n : ℝ) 0 := by
 313    simpa using (hasDerivAt_id (0 : ℝ)).const_mul ((n : ℝ))
 314  have hsecond : HasDerivAt (fun t : ℝ => Real.sinh ((n : ℝ) * t) * (n : ℝ))
 315      (Real.cosh ((n : ℝ) * 0) * (n : ℝ) * (n : ℝ)) 0 :=
 316    hin0.sinh.mul_const ((n : ℝ))
 317  rw [hG, hfirst, hsecond.deriv]
 318  simp
 319  ring
 320
 321/-- **Exactly one member of the family is calibrated.** The composition law
 322leaves a one-parameter family; calibration is what collapses it to `J`. This is
 323the clause §8 does not impose. -/
 324theorem isCalibrated_powCost_iff (n : ℕ) :
 325    IsCalibrated (powCost n) ↔ n = 1 := by
 326  rw [IsCalibrated, deriv2_G_powCost]
 327  constructor
 328  · intro h
 329    have hn : (n : ℝ) ^ 2 = (1 : ℝ) ^ 2 := by simpa using h
 330    have : (n : ℝ) = 1 := by
 331      nlinarith [sq_nonneg ((n : ℝ) - 1), sq_nonneg ((n : ℝ) + 1),
 332        Nat.cast_nonneg (α := ℝ) n]
 333    exact_mod_cast this
 334  · rintro rfl; norm_num
 335
 336/-! ## §4. The falsifier as printed is met, and was ill-posed -/
 337
 338/-- A one-point normalization of the cost weight. This is not the composition
 339law and has no recognition content: it says the weighted cost agrees with the
 340cost at a single argument. -/
 341def CalibratedWeightAtTwo (w : ℝ) : Prop := w * Cost.Jcost 2 = Cost.Jcost 2
 342
 343/-- It forces unit weight, and does so more sharply than the law, which leaves
 344the `w = 0` branch open. -/
 345theorem calibratedWeightAtTwo_forces_one (w : ℝ) (h : CalibratedWeightAtTwo w) :
 346    w = 1 := by
 347  have hJ : Cost.Jcost 2 = 1 / 4 := by norm_num [Cost.Jcost]
 348  rw [CalibratedWeightAtTwo, hJ] at h
 349  linarith
 350
 351/-- The zero weight satisfies the composition-law clause. -/
 352theorem rclWeight_zero :
 353    SatisfiesCompositionLaw (fun x => (0 : ℝ) * Cost.Jcost x) := by
 354  intro x y _ _
 355  simp
 356
 357/-- The zero weight does not satisfy the normalization clause. -/
 358theorem not_calibratedWeightAtTwo_zero : ¬ CalibratedWeightAtTwo 0 := by
 359  intro h
 360  have := calibratedWeightAtTwo_forces_one 0 h
 361  norm_num at this
 362
 363/-- **The two clauses are different predicates.** So the normalization is a
 364genuine witness for the falsifier rather than the composition law in disguise. -/
 365theorem calibratedWeightAtTwo_ne_rclWeight :
 366    CalibratedWeightAtTwo
 367      ≠ fun w => SatisfiesCompositionLaw (fun x => w * Cost.Jcost x) := by
 368  intro h
 369  have := congrArg (fun P => P 0) h
 370  simp only [eq_iff_iff] at this
 371  exact not_calibratedWeightAtTwo_zero (this.mpr rclWeight_zero)
 372
 373/-- **The falsifier printed in the paper is met.**
 374
 375There is a clause that is not the composition law, that forces unit weight, and
 376that leaves every other clause of the model class alone. The falsifier is
 377therefore satisfied as written.
 378
 379The finding this records is about the gate, not the theorem. A falsifier of the
 380form "exhibit any non-`P` clause with the same consequence" is met by the
 381consequence itself, so it cannot discriminate and should never have been
 382printed. §5 states the repaired version. -/
 383theorem falsifier_as_printed_is_met :
 384    (CalibratedWeightAtTwo
 385      ≠ fun w => SatisfiesCompositionLaw (fun x => w * Cost.Jcost x))
 386    ∧ (∀ w : ℝ, CalibratedWeightAtTwo w → w = 1) :=
 387  ⟨calibratedWeightAtTwo_ne_rclWeight, calibratedWeightAtTwo_forces_one⟩
 388
 389/-! ## §4b. The profile clause needs no composition law at all
 390
 391A cross-family hostile panel attacked the §5 verdict below on 2026-07-25 and
 392found something sharper than either side of it. The verdict says the recognition
 393cost is load-bearing for quadraticity because the oscillatory branch cannot be
 394substituted into the profile clause. That is true, and it is nearly empty, because
 395the profile clause has exactly *one* solution and says so without help.
 396
 397The clause reads `h a b p = W a b * Jlog (2 * arsinh (lam * p)) + U a b`, and the
 398chart `2 * arsinh` is J's own inverse chart: `u ↦ 2 arsinh u` is the substitution
 399that turns `Jlog` into `2 u ^ 2`. So asking for a function that is quadratic in
 400that chart is asking for `Jlog` up to scale, and `chart_alone_forces_the_cost`
 401proves it: no functional equation, no regularity, no measurability, no positivity.
 402
 403Two consequences, and the second is why this section exists.
 404
 405First, "the recognition cost is not replaceable in the profile clause" is true but
 406carries no information about recognition. It holds for the same reason that
 407`f (f⁻¹ y) = y` holds.
 408
 409Second, the chart is *typed in*. `exactCostKineticProfile` in
 410`HKTKineticFromRecognitionCost` writes `2 * Real.arsinh (lam * p)` as a literal,
 411and no theorem in the repo derives that chart from the substrate. So the clause
 412does not derive a quadratic momentum sector from recognition; it writes a
 413quadratic in a coordinate chosen to make the recognition cost look quadratic, and
 414the coefficient `2 λ ^ 2` is the double-angle identity
 415`cosh 2θ = 1 + 2 sinh ^ 2 θ`. Until a substrate derivation of the chart exists,
 416the honest reading of §8 is that neither of its two clauses carries recognition
 417content: the law clause contributes one bit by generic algebra, and the profile
 418clause contributes a change of variables. -/
 419
 420/-- **The chart alone forces the cost.** If any `G` is exactly quadratic in the
 421half-imbalance chart, then `G` is a multiple of the recognition cost in the log
 422chart. The hypothesis mentions no functional equation and no regularity; the proof
 423is the substitution `u = sinh (t / 2)`, which is available because
 424`u ↦ 2 arsinh u` inverts it.
 425
 426This is the formal content of the panel's attack on §8: the profile clause is a
 427uniqueness theorem for `Jlog` disguised as a physical premise. -/
 428theorem chart_alone_forces_the_cost (G : ℝ → ℝ) (C : ℝ)
 429    (h : ∀ u : ℝ, G (2 * Real.arsinh u) = C * u ^ 2) :
 430    ∀ t : ℝ, G t = (C / 2) * Cost.Jlog t := by
 431  intro t
 432  have hinv : 2 * Real.arsinh (Real.sinh (t / 2)) = t := by
 433    rw [Real.arsinh_sinh]; ring
 434  have hG : G t = C * Real.sinh (t / 2) ^ 2 := by
 435    have hu := h (Real.sinh (t / 2))
 436    rwa [hinv] at hu
 437  have hJ : Cost.Jlog t = 2 * Real.sinh (t / 2) ^ 2 := by
 438    have hu := HKTKineticFromRecognitionCost.Jlog_two_arsinh (Real.sinh (t / 2))
 439    rwa [hinv] at hu
 440  rw [hG, hJ]
 441  ring
 442
 443/-- The recognition cost is the `C = 2` member, which is the identity the profile
 444clause is built on. This is `HKTKineticFromRecognitionCost.Jlog_two_arsinh`, named
 445here so that `profile_clause_solution_set_is_a_scale_family` reads as an
 446equivalence rather than a one-way bound. -/
 447theorem Jlog_is_the_C_two_solution :
 448    ∀ u : ℝ, Cost.Jlog (2 * Real.arsinh u) = 2 * u ^ 2 :=
 449  HKTKineticFromRecognitionCost.Jlog_two_arsinh
 450
 451/-- **The uniqueness in the profile clause is worth zero bits about recognition.**
 452The solution set of the clause is a one-parameter family of multiples of the cost,
 453so "only the recognition cost satisfies it" is a restatement of the clause and not
 454evidence for the cost. Compare `oscCost_not_quadratic_in_log_chart`, which is the
 455special case of this at one substituted function; the general statement makes it
 456clear that the special case was never going to fail. -/
 457theorem profile_clause_solution_set_is_a_scale_family (C : ℝ) :
 458    ∀ G : ℝ → ℝ, (∀ u : ℝ, G (2 * Real.arsinh u) = C * u ^ 2)
 459      ↔ (∀ t : ℝ, G t = (C / 2) * Cost.Jlog t) := by
 460  intro G
 461  constructor
 462  · exact chart_alone_forces_the_cost G C
 463  · intro hG u
 464    rw [hG, Jlog_is_the_C_two_solution u]
 465    ring
 466
 467/-! ## §5. The scoped verdict -/
 468
 469/-- **Track A verdict, as a single named proposition.**
 470
 471Six facts. The conjunction is the honest statement of what §8's recognition
 472clause buys and what it does not.
 473
 4741. The forcing is generic in the law's solution set, so `Cost.Jcost` is not used
 475   for it.
 4762. The solution set is strictly larger than `{Cost.Jcost}`: argument rescaling
 477   acts on it and moves `J`.
 4783. It also contains functions that are not costs, since the oscillatory branch
 479   takes the value `-2`.
 4804. Those non-costs force unit weight too, which is the O5 failure mode on this
 481   step.
 4825. Calibration is what collapses the power family to `J`, and §8 does not
 483   impose calibration.
 4846. But the oscillatory branch cannot be substituted into the profile clause,
 485   because it is bounded and so is not quadratic in any log chart.
 486
 487Read together, and **corrected by §4b**: the composition law is load-bearing for
 488field-independence and buys it by algebra that no recognition primitive enters.
 489Fact 6 is true and nearly empty, because `chart_alone_forces_the_cost` shows the
 490profile clause has a one-parameter solution set consisting of multiples of the
 491cost, so *no* substitution into it could have succeeded. The first draft of this
 492verdict read fact 6 as recognition doing real work in the profile clause. It is not
 493work; the clause is a change of variables into the chart that inverts `J`, and the
 494chart is typed in rather than derived. Field-independence also needs the
 495model class's separate nonvanishing clause `∀ a b, W a b ≠ 0`, since the law alone
 496permits a field-dependent weight valued in `{0, 1}`.
 497
 498So the corrected verdict is that neither clause of §8 carries recognition content,
 499and this proposition is retained with fact 6 relabelled rather than deleted, so
 500that the record shows what was claimed and what replaced it. -/
 501def constraint_sector_recognition_load_is_quadraticity_not_unit_weight : Prop :=
 502  (∀ (F : ℝ → ℝ) (w : ℝ), SatisfiesCompositionLaw F →
 503      SatisfiesCompositionLaw (fun x => w * F x) →
 504      ∀ {x y : ℝ}, 0 < x → 0 < y → F x * F y ≠ 0 → w = 0 ∨ w = 1)
 505  ∧ (∀ n : ℕ, SatisfiesCompositionLaw (powCost n)) ∧ powCost 2 ≠ Cost.Jcost
 506  ∧ (SatisfiesCompositionLaw (oscCost 1) ∧ oscCost 1 (Real.exp Real.pi) = -2)
 507  ∧ (∀ w : ℝ, SatisfiesCompositionLaw (fun x => w * oscCost 1 x) →
 508      w = 0 ∨ w = 1)
 509  ∧ (∀ n : ℕ, IsCalibrated (powCost n) ↔ n = 1)
 510  ∧ (¬ ∃ c : ℝ, ∀ t : ℝ, oscCost 1 (Real.exp t) = c * t ^ 2)
 511
 512theorem constraint_sector_recognition_load_is_quadraticity_not_unit_weight_holds :
 513    constraint_sector_recognition_load_is_quadraticity_not_unit_weight :=
 514  ⟨fun F w hF hwF _ _ hx hy hne =>
 515      compositionLaw_forces_unit_weight_generic F w hF hwF hx hy hne,
 516   powCost_satisfiesCompositionLaw,
 517   powCost_two_ne_Jcost,
 518   ⟨oscCost_satisfiesCompositionLaw 1, oscCost_neg_at_exp_pi⟩,
 519   oscCost_forces_unit_weight,
 520   isCalibrated_powCost_iff,
 521   oscCost_not_quadratic_in_log_chart⟩
 522
 523/-! ## §6. Axiom audit -/
 524
 525section Audit
 526
 527#print axioms compositionLaw_forces_unit_weight_generic
 528#print axioms compositionLaw_forces_unit_weight_is_an_instance
 529#print axioms satisfiesCompositionLaw_comp_pow
 530#print axioms powCost_satisfiesCompositionLaw
 531#print axioms powCost_two_ne_Jcost
 532#print axioms Jcost_pos_of_one_lt
 533#print axioms powCost_forces_unit_weight
 534#print axioms G_powCost
 535#print axioms deriv2_G_powCost
 536#print axioms isCalibrated_powCost_iff
 537#print axioms calibratedWeightAtTwo_forces_one
 538#print axioms rclWeight_zero
 539#print axioms not_calibratedWeightAtTwo_zero
 540#print axioms calibratedWeightAtTwo_ne_rclWeight
 541#print axioms falsifier_as_printed_is_met
 542#print axioms oscCost_satisfiesCompositionLaw
 543#print axioms oscCost_neg_at_exp_pi
 544#print axioms oscCost_forces_unit_weight
 545#print axioms oscCost_not_quadratic_in_log_chart
 546#print axioms chart_alone_forces_the_cost
 547#print axioms Jlog_is_the_C_two_solution
 548#print axioms profile_clause_solution_set_is_a_scale_family
 549#print axioms constraint_sector_recognition_load_is_quadraticity_not_unit_weight_holds
 550
 551end Audit
 552
 553end ConstraintSectorReparamAttack
 554end SevenGaps
 555end Gravity
 556end IndisputableMonolith
 557