IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumBridge

   1import IndisputableMonolith.Gravity.SevenGaps.Gap5NetImbalanceDerivation
   2
   3/-!
   4# The momentum-magnitude bridge: the scale wall, the exact residual, and what the bridge buys
   5
   6**Verdict, stated first.** The momentum-magnitude bridge `|p| = |imbalance|` does
   7**not** derive from the conjunction of every momentum-selecting property the
   8substrate arc has produced, and this module kernel-checks that wall with the
   9selection package named exactly. The exhibited family is the scaled ray
  10
  11    scaledImbalance a z := a * imbalance z        (a ≠ 0)
  12
  13Every selection property used anywhere in the six-module arc
  14(`Gap5ChartFromLedgerMomentum` through `Gap5NetImbalanceDerivation`) is
  15**scale-invariant**: continuity, swap-oddness under the debit-credit exchange,
  16additivity under ledger consolidation, balance-vanishing, column posting
  17incidence, net-imbalance reading, debit-axis Cauchy additivity, and
  18canonical-momentum status against the ledger total all hold of the whole ray at
  19once (`scaleFreePackage_on_ray`). The bridge holds on the ray exactly at the
  20unit scale, in three kernel-checked equivalent forms:
  21
  22    KineticCondition (scaledImbalance a)   ↔  a ^ 2 = 1
  23    EnergyEqualsCost (scaledImbalance a)   ↔  a ^ 2 = 1
  24    scaledImbalance a (1, 0) ^ 2 = 1       ↔  a ^ 2 = 1
  25
  26Hence the conjunction of the scale-free package cannot force the bridge
  27(`bridge_not_forced_by_scale_free_package`): the unit and double scales agree on
  28everything the substrate fixes and disagree on the bridge
  29(`exhibited_pair_disagrees_on_bridge`). The entire residual of flags 6 and 12 on
  30this lane is one real condition: **the momentum's scale in posting units**. A
  31derivation must therefore import a scale-bearing premise, and the library names
  32exactly one candidate: `EnergyEqualsCost` ("energy is the recognition cost"), a
  33foundational identification of the same kind as T10's R4, recorded as a named
  34premise in `Gap5MomentumMagnitudeBridge` and shown independent of the B1 package
  35there. The alternative door is the posting-dynamics conversion theorem
  36`IsPhysicalMomentumFromPostingDynamics p → p = imbalance` for a stated
  37scale-bearing predicate, named in the campaign ledger and absent from the
  38library; the naive generator version of it is already refuted (the orbit
  39Hamiltonian vector field is `(d / 2, -c / 2)`, not the imbalance).
  40
  41## The sign is a second, independent residue
  42
  43The magnitude bridge is sign-blind. `scaledImbalance (-1)` passes the whole
  44scale-free package and the unit scale, satisfies the kinetic condition and
  45`EnergyEqualsCost`, and is not `imbalance` (`sign_not_forced_with_unit_scale`).
  46So even the scale-free package plus the unit scale does not force the signed
  47identity `p = imbalance`; the sign is pinned only by the signed chart theorem
  48(`chart_is_the_imbalance_coordinate`), exactly as the campaign plan records.
  49The constants cluster never sees the sign: `cKin = 2 * lam ^ 2` and
  50`cMom = 4 * cKin * cGrad` depend on `lam` only through `lam ^ 2`.
  51
  52## What the bridge buys, kernel-checked as conditionals
  53
  541. Equating the stipulated half-imbalance chart `t = 2 * arsinh (lam * p)` with
  55   the derived imbalance-coordinate chart forces the chart product
  56   `lam * p = imbalance / (2 * sqrt k)` on every orbit
  57   (`chart_product_of_stipulated_chart`, via `arsinh` injectivity).
  582. With the signed bridge `p = imbalance` the product cancels at any unbalanced
  59   orbit point: `lam = 1 / (2 * sqrt k)` (`lam_of_signed_bridge`), and at the
  60   balanced ground state's Casimir `k = 1` this is `lam = 1 / 2`
  61   (`lam_ground_state_of_signed_bridge`).
  623. The magnitude bridge alone (no sign) pins `lam ^ 2 = 1 / (4 * k)` on every
  63   orbit (`lam_sq_of_magnitude_bridge`), hence at the ground state
  64   `cKin = 1 / 2` and `cMom = 2 * cGrad`
  65   (`constants_cluster_of_magnitude_bridge`). The bridge therefore reduces the
  66   flag-12 constants cluster by one derived number and one derived ratio:
  67   `{lam, cKin, cGrad, cMom}` with two equations becomes `{cGrad, cMom}` with
  68   `cMom = 2 * cGrad`, leaving `cGrad` the cluster's one free constant.
  69
  70## What is NOT claimed
  71
  72* No flag flip, and no new premise is asserted as derived. The wall is a
  73  theorem about the named package on the stated `LedgerState` chart carrier
  74  (quantifier first, per `L-qg-witness-is-not-a-class-20260729`): it refutes
  75  derivations whose inputs are the scale-free selection properties of the
  76  existing arc, all at once. It does not touch a derivation importing a
  77  scale-bearing premise (`EnergyEqualsCost` accepted as a foundational MODEL,
  78  or a posting-dynamics conversion with scale content).
  79* The B1 conditional closure is neither used nor strengthened. B1's residue and
  80  flag 12's blocker are the scale, and the scale is now exhibited as a single
  81  real condition rather than a predicate on observables.
  82* The two prior walls this one conjoins stay theorem: the Hamiltonian-data
  83  polarization witness (`energyEqualsCost_independent_of_hamiltonian_data`)
  84  and the composition-law independence witness
  85  (`momentum_additivity_independent_of_composition_law`).
  86
  87## Scope
  88
  89Chart carrier `LedgerState` only. No flag moves.
  90-/
  91
  92namespace IndisputableMonolith
  93namespace Gravity
  94namespace SevenGaps
  95namespace MomentumBridge
  96
  97open ChartFromLedgerMomentum MomentumAdditivity MomentumMagnitudeBridge
  98open EnergyEqualsCostDerivation MomentumAdditivityComposition NetImbalanceDerivation
  99
 100noncomputable section
 101
 102/-! ## §0. The scaled ray -/
 103
 104/-- The scaled imbalance ray: the momentum observable at scale `a` in posting
 105units. `a = 1` is the library `imbalance`; the bridge asks why `a ^ 2 = 1`. -/
 106def scaledImbalance (a : ℝ) (z : LedgerState) : ℝ := a * imbalance z
 107
 108/-! ## §1. Every selection property of the arc is scale-invariant -/
 109
 110theorem scaledImbalance_continuous (a : ℝ) : Continuous (scaledImbalance a) :=
 111  continuous_const.mul continuous_imbalance
 112
 113theorem scaledImbalance_swapOdd (a : ℝ) : SwapOdd (scaledImbalance a) := by
 114  intro z
 115  show a * imbalance (z.2, z.1) = -(a * imbalance z)
 116  rw [imbalance_swap]
 117  ring
 118
 119theorem scaledImbalance_additive (a : ℝ) (z w : LedgerState) :
 120    scaledImbalance a (z + w) = scaledImbalance a z + scaledImbalance a w := by
 121  show a * imbalance (z + w) = a * imbalance z + a * imbalance w
 122  rw [imbalance_add]
 123  ring
 124
 125theorem scaledImbalance_balance_vanishing (a : ℝ) (z : LedgerState) (hz : Balanced z) :
 126    scaledImbalance a z = 0 := by
 127  have hi : imbalance z = 0 := sub_eq_zero.mpr hz
 128  show a * imbalance z = 0
 129  rw [hi, mul_zero]
 130
 131theorem scaledImbalance_postingIncidence (a : ℝ) :
 132    PostingIncidence (scaledImbalance a) := by
 133  intro d c
 134  show a * imbalance (d, c) = a * imbalance (d, 0) + a * imbalance (0, c)
 135  simp only [imbalance, sub_zero, zero_sub]
 136  ring
 137
 138theorem scaledImbalance_readsNet (a : ℝ) : ReadsNetImbalance (scaledImbalance a) := by
 139  intro z
 140  show a * imbalance z = a * imbalance (imbalance z, 0)
 141  simp only [imbalance, sub_zero]
 142
 143theorem scaledImbalance_additiveOnDebitAxis (a : ℝ) :
 144    AdditiveOnDebitAxis (scaledImbalance a) := by
 145  intro m n
 146  show a * imbalance (m, 0) + a * imbalance (n, 0) = a * imbalance (m + n, 0)
 147  simp only [imbalance, sub_zero]
 148  ring
 149
 150/-- The Poisson bracket of the scaled imbalance with the ledger total, in the
 151coefficient form of `EnergyEqualsCostDerivation.poissonLin`: `{a • imbalance,
 152total} = 2 a`, nonzero at every nonzero scale. Canonical-momentum status is
 153therefore scale-invariant. -/
 154theorem scaledImbalance_conjugate_bracket (a : ℝ) :
 155    poissonLin a (-a) 1 1 = 2 * a := by
 156  show a * 1 - (-a) * 1 = 2 * a
 157  ring
 158
 159/-! ## §2. The bridge on the ray is exactly the unit-scale condition -/
 160
 161theorem scaledImbalance_unit_sq (a : ℝ) :
 162    scaledImbalance a ((1, 0) : LedgerState) ^ 2 = a ^ 2 := by
 163  simp only [scaledImbalance, imbalance, sub_zero, mul_one]
 164
 165/-- **The kinetic condition on the ray is `a ^ 2 = 1`.** Forward by evaluation
 166at the pure unit debit; backward by factoring the square. -/
 167theorem kineticCondition_on_ray_iff (a : ℝ) :
 168    KineticCondition (scaledImbalance a) ↔ a ^ 2 = 1 := by
 169  constructor
 170  · intro h
 171    have h1 := h ((1, 0) : LedgerState)
 172    have hi : imbalance ((1, 0) : LedgerState) = 1 := by simp [imbalance]
 173    rw [hi, scaledImbalance_unit_sq, one_pow] at h1
 174    exact h1
 175  · intro h z
 176    show (a * imbalance z) ^ 2 = imbalance z ^ 2
 177    rw [mul_pow, h, one_mul]
 178
 179/-- **Energy-equals-cost on the ray is `a ^ 2 = 1`.** Forward by cancelling the
 180orbit imbalance at a point where it is nonzero; backward by the existing
 181exactness theorem `energy_equals_cost_of_imbalance`. -/
 182theorem energyEqualsCost_on_ray_iff (a : ℝ) :
 183    EnergyEqualsCost (scaledImbalance a) ↔ a ^ 2 = 1 := by
 184  constructor
 185  · intro h
 186    have h1 := h 1 2 one_pos
 187    change (a * imbalance (orbitPoint (1 : ℝ) 2)) ^ 2 =
 188      2 * (1 : ℝ) * Cost.Jlog 2 at h1
 189    have hbase := energy_equals_cost_of_imbalance 1 2 one_pos
 190    have himb_ne : imbalance (orbitPoint (1 : ℝ) 2) ≠ 0 := by
 191      have e : imbalance (orbitPoint (1 : ℝ) 2) = 2 * Real.sinh 1 := by
 192        rw [orbitPoint_imbalance, Real.sqrt_one, one_mul,
 193          show (2 : ℝ) / 2 = 1 from by norm_num]
 194      have hsin : 0 < Real.sinh 1 := by
 195        have hs := Real.sinh_lt_sinh.mpr (by norm_num : (0 : ℝ) < 1)
 196        rwa [Real.sinh_zero] at hs
 197      rw [e]
 198      exact (mul_pos (by norm_num) hsin).ne'
 199    have e : (a * imbalance (orbitPoint (1 : ℝ) 2)) ^ 2 =
 200        imbalance (orbitPoint (1 : ℝ) 2) ^ 2 := h1.trans hbase.symm
 201    rw [mul_pow] at e
 202    have e2 : a ^ 2 * imbalance (orbitPoint (1 : ℝ) 2) ^ 2 =
 203        1 * imbalance (orbitPoint (1 : ℝ) 2) ^ 2 := by
 204      rw [e, one_mul]
 205    exact mul_right_cancel₀ (pow_ne_zero 2 himb_ne) e2
 206  · intro h k t hk
 207    show (a * imbalance (orbitPoint k t)) ^ 2 = 2 * k * Cost.Jlog t
 208    rw [mul_pow, h, one_mul]
 209    exact energy_equals_cost_of_imbalance k t hk
 210
 211/-- The unit normalization on the ray is the same condition. -/
 212theorem unit_norm_on_ray_iff (a : ℝ) :
 213    scaledImbalance a ((1, 0) : LedgerState) ^ 2 = 1 ↔ a ^ 2 = 1 := by
 214  rw [scaledImbalance_unit_sq]
 215
 216/-! ## §3. The scale-free package, named exactly, and the wall -/
 217
 218/-- **The scale-free momentum package: X, named exactly.** Every property the
 219six-module substrate arc used to select the momentum observable, gathered as
 220one predicate. The wall theorem below shows the package holds of the whole
 221scaled ray, while the bridge holds only at unit scale. -/
 222structure ScaleFreeMomentumPackage (p : LedgerState → ℝ) : Prop where
 223  /-- Regularity premise of the B1 certificate. -/
 224  continuous : Continuous p
 225  /-- Oddness under the substrate's debit-credit exchange. -/
 226  swap_odd : SwapOdd p
 227  /-- Extensivity under ledger consolidation. -/
 228  consolidation_additive : ∀ z w : LedgerState, p (z + w) = p z + p w
 229  /-- Vanishing on the double-entry balance locus. -/
 230  balance_vanishing : ∀ z : LedgerState, Balanced z → p z = 0
 231  /-- Column posting incidence: the two columns contribute independently. -/
 232  posting_incidence : PostingIncidence p
 233  /-- The momentum reads only the net charge. -/
 234  reads_net_imbalance : ReadsNetImbalance p
 235  /-- The one-dimensional Cauchy property on the pure-debit axis. -/
 236  debit_axis_additive : AdditiveOnDebitAxis p
 237  /-- Canonical-momentum status: `p` is a linear observable with nonzero
 238  Poisson bracket against the ledger total (conjugate up to normalization). -/
 239  canonical_bracket : ∃ a₁ b₁ : ℝ, poissonLin a₁ b₁ 1 1 ≠ 0 ∧
 240    (∀ z : LedgerState, p z = a₁ * z.1 + b₁ * z.2)
 241
 242/-- **The package is scale-invariant.** Every nonzero rescaling of the
 243imbalance satisfies all eight selection properties at once. -/
 244theorem scaleFreePackage_on_ray {a : ℝ} (ha : a ≠ 0) :
 245    ScaleFreeMomentumPackage (scaledImbalance a) where
 246  continuous := scaledImbalance_continuous a
 247  swap_odd := scaledImbalance_swapOdd a
 248  consolidation_additive := scaledImbalance_additive a
 249  balance_vanishing := scaledImbalance_balance_vanishing a
 250  posting_incidence := scaledImbalance_postingIncidence a
 251  reads_net_imbalance := scaledImbalance_readsNet a
 252  debit_axis_additive := scaledImbalance_additiveOnDebitAxis a
 253  canonical_bracket :=
 254    ⟨a, -a, by
 255      rw [scaledImbalance_conjugate_bracket]
 256      exact mul_ne_zero two_ne_zero ha,
 257      fun z => by
 258        simp only [scaledImbalance, imbalance]
 259        ring⟩
 260
 261/-- **THE WALL: the bridge is not forced by the scale-free package.** The
 262eight-property package holds of the entire ray (`∀ a ≠ 0`); the kinetic
 263condition, `EnergyEqualsCost`, and the unit normalization each hold on the ray
 264exactly at `a ^ 2 = 1`; and the double-scale member exhibits all eight
 265properties together with the failure of the bridge. X is the package above,
 266named property by property. -/
 267theorem bridge_not_forced_by_scale_free_package :
 268    (∀ a : ℝ, a ≠ 0 → ScaleFreeMomentumPackage (scaledImbalance a)) ∧
 269    (∀ a : ℝ, KineticCondition (scaledImbalance a) ↔ a ^ 2 = 1) ∧
 270    (∀ a : ℝ, EnergyEqualsCost (scaledImbalance a) ↔ a ^ 2 = 1) ∧
 271    (∀ a : ℝ, scaledImbalance a ((1, 0) : LedgerState) ^ 2 = 1 ↔ a ^ 2 = 1) ∧
 272    (ScaleFreeMomentumPackage (scaledImbalance 2) ∧
 273      ¬ KineticCondition (scaledImbalance 2) ∧
 274      ¬ EnergyEqualsCost (scaledImbalance 2)) ∧
 275    (ScaleFreeMomentumPackage (scaledImbalance 1) ∧
 276      KineticCondition (scaledImbalance 1) ∧
 277      EnergyEqualsCost (scaledImbalance 1)) :=
 278  ⟨fun a ha => scaleFreePackage_on_ray ha,
 279    kineticCondition_on_ray_iff, energyEqualsCost_on_ray_iff, unit_norm_on_ray_iff,
 280    ⟨scaleFreePackage_on_ray two_ne_zero,
 281      (kineticCondition_on_ray_iff 2).not.mpr (by norm_num),
 282      (energyEqualsCost_on_ray_iff 2).not.mpr (by norm_num)⟩,
 283    ⟨scaleFreePackage_on_ray one_ne_zero,
 284      (kineticCondition_on_ray_iff 1).mpr (by norm_num),
 285      (energyEqualsCost_on_ray_iff 1).mpr (by norm_num)⟩⟩
 286
 287/-- **The exhibited pair.** Unit and double scale agree on everything the
 288substrate fixes (all eight selection properties) and disagree on the bridge.
 289This is the "agreeing on X, differing on the bridge" witness the campaign asked
 290for, with X the package named above. -/
 291theorem exhibited_pair_disagrees_on_bridge :
 292    ScaleFreeMomentumPackage (scaledImbalance 1) ∧
 293    ScaleFreeMomentumPackage (scaledImbalance 2) ∧
 294    KineticCondition (scaledImbalance 1) ∧ ¬ KineticCondition (scaledImbalance 2) :=
 295  ⟨scaleFreePackage_on_ray one_ne_zero, scaleFreePackage_on_ray two_ne_zero,
 296    (kineticCondition_on_ray_iff 1).mpr (by norm_num),
 297    (kineticCondition_on_ray_iff 2).not.mpr (by norm_num)⟩
 298
 299/-! ## §4. The sign is a second residue -/
 300
 301/-- **The sign wall.** `scaledImbalance (-1)` passes the entire scale-free
 302package, the unit scale, the kinetic condition, and `EnergyEqualsCost`, and is
 303not `imbalance`. The scale-free package plus the unit scale therefore does not
 304force the signed identity `p = imbalance`; the sign is pinned only by the
 305signed chart. The magnitude bridge and the constants cluster are sign-blind. -/
 306theorem sign_not_forced_with_unit_scale :
 307    ScaleFreeMomentumPackage (scaledImbalance (-1)) ∧
 308    scaledImbalance (-1) ((1, 0) : LedgerState) ^ 2 = 1 ∧
 309    KineticCondition (scaledImbalance (-1)) ∧
 310    EnergyEqualsCost (scaledImbalance (-1)) ∧
 311    scaledImbalance (-1) ≠ imbalance := by
 312  refine ⟨scaleFreePackage_on_ray (by norm_num), ?_, ?_, ?_, ?_⟩
 313  · rw [scaledImbalance_unit_sq]
 314    norm_num
 315  · exact (kineticCondition_on_ray_iff _).mpr (by norm_num)
 316  · exact (energyEqualsCost_on_ray_iff _).mpr (by norm_num)
 317  · intro h
 318    have h1 := congrFun h ((1, 0) : LedgerState)
 319    have e1 : scaledImbalance (-1) ((1, 0) : LedgerState) = -1 := by
 320      simp only [scaledImbalance, imbalance, sub_zero, mul_one]
 321    have e2 : imbalance ((1, 0) : LedgerState) = 1 := by simp [imbalance]
 322    rw [e1, e2] at h1
 323    norm_num at h1
 324
 325/-! ## §5. What the bridge buys on the cMom cluster -/
 326
 327/-- **The chart product from the two chart forms.** The stipulated chart
 328`t = 2 * arsinh (lam * p)` and the derived imbalance-coordinate chart
 329(`chart_is_the_imbalance_coordinate`) agree on every orbit, and `arsinh` is
 330injective, so `lam * p = imbalance / (2 * sqrt k)` on every orbit. This is the
 331joint product the C2 Casimir lead could not split. -/
 332theorem chart_product_of_stipulated_chart (k lam : ℝ) (p : LedgerState → ℝ)
 333    (hk : 0 < k)
 334    (hstip : ∀ t : ℝ, t = 2 * Real.arsinh (lam * p (orbitPoint k t))) (t : ℝ) :
 335    lam * p (orbitPoint k t) = imbalance (orbitPoint k t) / (2 * Real.sqrt k) := by
 336  have h2 := chart_is_the_imbalance_coordinate k t hk
 337  have h3 : 2 * Real.arsinh (lam * p (orbitPoint k t)) =
 338      2 * Real.arsinh (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) := by
 339    rw [← hstip t]
 340    exact h2
 341  have h4 : Real.arsinh (lam * p (orbitPoint k t)) =
 342      Real.arsinh (imbalance (orbitPoint k t) / (2 * Real.sqrt k)) := by
 343    linarith [h3]
 344  exact Real.arsinh_injective h4
 345
 346/-- The orbit imbalance at `t = 2 * arsinh 1` is `2 * sqrt k`, nonzero at
 347positive Casimir: the cancellation point for splitting the chart product. -/
 348theorem imbalance_orbitPoint_at_two_arsinh_one (k : ℝ) :
 349    imbalance (orbitPoint k (2 * Real.arsinh 1)) = 2 * Real.sqrt k := by
 350  rw [orbitPoint_imbalance,
 351    show (2 * Real.arsinh (1 : ℝ)) / 2 = Real.arsinh 1 from by ring,
 352    Real.sinh_arsinh]
 353  ring
 354
 355/-- **With the signed bridge, the chart's free constant is the inverse ledger
 356scale.** `lam = 1 / (2 * sqrt k)`: the product the C2 Casimir lead wanted is
 357split by the bridge, and `k` is the only remaining freedom (the orbit's
 358Casimir, fixed at `1` on the balanced ground state). -/
 359theorem lam_of_signed_bridge (k lam : ℝ) (hk : 0 < k)
 360    (hchart : ∀ t : ℝ, lam * imbalance (orbitPoint k t) =
 361      imbalance (orbitPoint k t) / (2 * Real.sqrt k)) :
 362    lam = 1 / (2 * Real.sqrt k) := by
 363  have hsk : 0 < Real.sqrt k := Real.sqrt_pos.mpr hk
 364  have himb := imbalance_orbitPoint_at_two_arsinh_one k
 365  have hne : imbalance (orbitPoint k (2 * Real.arsinh 1)) ≠ 0 := by
 366    rw [himb]
 367    exact (mul_pos (by norm_num) hsk).ne'
 368  have h0 := hchart (2 * Real.arsinh 1)
 369  rw [himb] at h0
 370  have h1 : lam * (2 * Real.sqrt k) = 1 := by
 371    rw [h0]
 372    exact div_self (mul_ne_zero two_ne_zero hsk.ne')
 373  exact (eq_div_iff (mul_ne_zero two_ne_zero hsk.ne')).mpr h1
 374
 375/-- The signed bridge composed with the stipulated chart: `lam` is the inverse
 376ledger scale. This is the C2 Casimir lead's conclusion, now with its premise
 377(the signed bridge) named in the hypothesis instead of smuggled. -/
 378theorem lam_of_signed_bridge_at_stipulated_chart (k lam : ℝ) (p : LedgerState → ℝ)
 379    (hk : 0 < k) (hp : p = imbalance)
 380    (hstip : ∀ t : ℝ, t = 2 * Real.arsinh (lam * p (orbitPoint k t))) :
 381    lam = 1 / (2 * Real.sqrt k) := by
 382  apply lam_of_signed_bridge k lam hk
 383  intro t
 384  have h := chart_product_of_stipulated_chart k lam p hk hstip t
 385  rwa [hp] at h
 386
 387/-- **The magnitude bridge alone pins `lam ^ 2` on every orbit.** Squaring the
 388chart product and using the kinetic identity kills the momentum factor and the
 389sign: no signed identification is needed for the constants cluster. -/
 390theorem lam_sq_of_magnitude_bridge (k lam : ℝ) (p : LedgerState → ℝ) (hk : 0 < k)
 391    (hkin : ∀ t : ℝ, p (orbitPoint k t) ^ 2 = imbalance (orbitPoint k t) ^ 2)
 392    (hchart : ∀ t : ℝ, lam * p (orbitPoint k t) =
 393      imbalance (orbitPoint k t) / (2 * Real.sqrt k)) :
 394    lam ^ 2 = 1 / (4 * k) := by
 395  have hsk : 0 < Real.sqrt k := Real.sqrt_pos.mpr hk
 396  have himb := imbalance_orbitPoint_at_two_arsinh_one k
 397  have hne : imbalance (orbitPoint k (2 * Real.arsinh 1)) ≠ 0 := by
 398    rw [himb]
 399    exact (mul_pos (by norm_num) hsk).ne'
 400  have h0 := hchart (2 * Real.arsinh 1)
 401  have hk0 := hkin (2 * Real.arsinh 1)
 402  have hsq : lam ^ 2 * p (orbitPoint k (2 * Real.arsinh 1)) ^ 2 =
 403      imbalance (orbitPoint k (2 * Real.arsinh 1)) ^ 2 / (4 * k) := by
 404    have e : (lam * p (orbitPoint k (2 * Real.arsinh 1))) ^ 2 =
 405        (imbalance (orbitPoint k (2 * Real.arsinh 1)) / (2 * Real.sqrt k)) ^ 2 := by
 406      rw [h0]
 407    rw [mul_pow, div_pow] at e
 408    have hden : (2 * Real.sqrt k) ^ 2 = 4 * k := by
 409      calc (2 * Real.sqrt k) ^ 2 = 4 * (Real.sqrt k ^ 2) := by ring
 410        _ = 4 * k := by rw [Real.sq_sqrt hk.le]
 411    rw [hden] at e
 412    exact e
 413  rw [hk0] at hsq
 414  have hm2 : imbalance (orbitPoint k (2 * Real.arsinh 1)) ^ 2 ≠ 0 :=
 415    pow_ne_zero 2 hne
 416  have hsq2 : lam ^ 2 * imbalance (orbitPoint k (2 * Real.arsinh 1)) ^ 2 =
 417      (1 / (4 * k)) * imbalance (orbitPoint k (2 * Real.arsinh 1)) ^ 2 := by
 418    rw [hsq, ← mul_one_div (imbalance (orbitPoint k (2 * Real.arsinh 1)) ^ 2) (4 * k)]
 419    exact mul_comm _ _
 420  exact mul_right_cancel₀ hm2 hsq2
 421
 422/-- **What the bridge buys on `cMom = 4 * cKin * cGrad`.** At the balanced
 423ground state's Casimir (`k = 1`) the magnitude bridge gives `lam ^ 2 = 1 / 4`;
 424with `cKin = 2 * lam ^ 2` derived this is `cKin = 1 / 2`, and the cMom equation
 425collapses to `cMom = 2 * cGrad`. One derived number and one derived ratio;
 426`cGrad` remains the cluster's one free constant. -/
 427theorem constants_cluster_of_magnitude_bridge {lam cKin cGrad cMom : ℝ}
 428    (hlam : lam ^ 2 = 1 / 4) (hcKin : cKin = 2 * lam ^ 2)
 429    (hcMom : cMom = 4 * cKin * cGrad) :
 430    cKin = 1 / 2 ∧ cMom = 2 * cGrad := by
 431  refine ⟨?_, ?_⟩
 432  · rw [hcKin, hlam]
 433    norm_num
 434  · rw [hcMom, hcKin, hlam]
 435    ring
 436
 437/-- At the ground state the signed bridge gives `lam = 1 / 2`. -/
 438theorem lam_ground_state_of_signed_bridge {lam : ℝ}
 439    (hstip : ∀ t : ℝ, t = 2 * Real.arsinh (lam * imbalance (orbitPoint 1 t))) :
 440    lam = 1 / 2 := by
 441  have h := lam_of_signed_bridge_at_stipulated_chart 1 lam imbalance one_pos rfl hstip
 442  rwa [Real.sqrt_one, mul_one] at h
 443
 444/-- The full ground-state cluster from the signed bridge, composed:
 445`lam = 1 / 2`, `cKin = 1 / 2`, `cMom = 2 * cGrad`. -/
 446theorem ground_state_cluster_of_signed_bridge {lam cKin cGrad cMom : ℝ}
 447    (hstip : ∀ t : ℝ, t = 2 * Real.arsinh (lam * imbalance (orbitPoint 1 t)))
 448    (hcKin : cKin = 2 * lam ^ 2) (hcMom : cMom = 4 * cKin * cGrad) :
 449    lam = 1 / 2 ∧ cKin = 1 / 2 ∧ cMom = 2 * cGrad := by
 450  have hlam := lam_ground_state_of_signed_bridge hstip
 451  refine ⟨hlam, ?_, ?_⟩
 452  · rw [hcKin, hlam]
 453    norm_num
 454  · rw [hcMom, hcKin, hlam]
 455    ring
 456
 457/-! ## §6. The verdict certificate -/
 458
 459/-- **The bridge verdict, packaged.** The scale-free package is scale-invariant;
 460the bridge on the ray is exactly the unit-scale condition in three equivalent
 461forms; the unit/double pair disagrees on the bridge while agreeing on the
 462package; the sign survives the unit scale; and the bridge's downstream content
 463for the cMom cluster is the four conditional theorems. -/
 464structure MomentumBridgeVerdict : Prop where
 465  /-- X, named exactly, holds of the whole ray. -/
 466  package_scale_free : ∀ a : ℝ, a ≠ 0 → ScaleFreeMomentumPackage (scaledImbalance a)
 467  /-- The kinetic condition on the ray is the unit-scale condition. -/
 468  kinetic_on_ray_iff_unit : ∀ a : ℝ, KineticCondition (scaledImbalance a) ↔ a ^ 2 = 1
 469  /-- Energy-equals-cost on the ray is the unit-scale condition. -/
 470  eec_on_ray_iff_unit : ∀ a : ℝ, EnergyEqualsCost (scaledImbalance a) ↔ a ^ 2 = 1
 471  /-- The unit normalization on the ray is the unit-scale condition. -/
 472  unit_norm_on_ray_iff_unit : ∀ a : ℝ,
 473    scaledImbalance a ((1, 0) : LedgerState) ^ 2 = 1 ↔ a ^ 2 = 1
 474  /-- The wall, pair form. -/
 475  pair_disagrees_on_bridge :
 476    ScaleFreeMomentumPackage (scaledImbalance 1) ∧
 477    ScaleFreeMomentumPackage (scaledImbalance 2) ∧
 478    KineticCondition (scaledImbalance 1) ∧ ¬ KineticCondition (scaledImbalance 2)
 479  /-- The sign wall. -/
 480  sign_free_at_unit_scale :
 481    ScaleFreeMomentumPackage (scaledImbalance (-1)) ∧
 482    scaledImbalance (-1) ((1, 0) : LedgerState) ^ 2 = 1 ∧
 483    KineticCondition (scaledImbalance (-1)) ∧
 484    EnergyEqualsCost (scaledImbalance (-1)) ∧
 485    scaledImbalance (-1) ≠ imbalance
 486  /-- The chart product from the two chart forms. -/
 487  chart_product : ∀ (k lam : ℝ) (p : LedgerState → ℝ), 0 < k →
 488    (∀ t : ℝ, t = 2 * Real.arsinh (lam * p (orbitPoint k t))) → ∀ t : ℝ,
 489      lam * p (orbitPoint k t) = imbalance (orbitPoint k t) / (2 * Real.sqrt k)
 490  /-- Signed bridge splits the product. -/
 491  lam_of_signed : ∀ (k lam : ℝ), 0 < k →
 492    (∀ t : ℝ, lam * imbalance (orbitPoint k t) =
 493      imbalance (orbitPoint k t) / (2 * Real.sqrt k)) →
 494      lam = 1 / (2 * Real.sqrt k)
 495  /-- Magnitude bridge pins `lam ^ 2`. -/
 496  lam_sq_of_magnitude : ∀ (k lam : ℝ) (p : LedgerState → ℝ), 0 < k →
 497    (∀ t : ℝ, p (orbitPoint k t) ^ 2 = imbalance (orbitPoint k t) ^ 2) →
 498    (∀ t : ℝ, lam * p (orbitPoint k t) =
 499      imbalance (orbitPoint k t) / (2 * Real.sqrt k)) →
 500      lam ^ 2 = 1 / (4 * k)
 501  /-- Ground-state constants from the magnitude bridge. -/
 502  ground_cluster_of_magnitude : ∀ lam cKin cGrad cMom : ℝ,
 503    lam ^ 2 = 1 / 4 → cKin = 2 * lam ^ 2 → cMom = 4 * cKin * cGrad →
 504      cKin = 1 / 2 ∧ cMom = 2 * cGrad
 505  /-- Ground-state `lam` from the signed bridge. -/
 506  ground_lam_of_signed : ∀ lam : ℝ,
 507    (∀ t : ℝ, t = 2 * Real.arsinh (lam * imbalance (orbitPoint 1 t))) → lam = 1 / 2
 508
 509theorem momentumBridgeVerdict : MomentumBridgeVerdict where
 510  package_scale_free := fun _a ha => scaleFreePackage_on_ray ha
 511  kinetic_on_ray_iff_unit := kineticCondition_on_ray_iff
 512  eec_on_ray_iff_unit := energyEqualsCost_on_ray_iff
 513  unit_norm_on_ray_iff_unit := unit_norm_on_ray_iff
 514  pair_disagrees_on_bridge := exhibited_pair_disagrees_on_bridge
 515  sign_free_at_unit_scale := sign_not_forced_with_unit_scale
 516  chart_product := chart_product_of_stipulated_chart
 517  lam_of_signed := lam_of_signed_bridge
 518  lam_sq_of_magnitude := lam_sq_of_magnitude_bridge
 519  ground_cluster_of_magnitude := fun lam cKin cGrad cMom =>
 520    constants_cluster_of_magnitude_bridge (lam := lam) (cKin := cKin) (cGrad := cGrad)
 521      (cMom := cMom)
 522  ground_lam_of_signed := fun lam => lam_ground_state_of_signed_bridge (lam := lam)
 523
 524/-! ## Axiom audit -/
 525
 526#print axioms scaledImbalance_continuous
 527#print axioms scaledImbalance_swapOdd
 528#print axioms scaledImbalance_additive
 529#print axioms scaledImbalance_balance_vanishing
 530#print axioms scaledImbalance_postingIncidence
 531#print axioms scaledImbalance_readsNet
 532#print axioms scaledImbalance_additiveOnDebitAxis
 533#print axioms scaledImbalance_conjugate_bracket
 534#print axioms scaledImbalance_unit_sq
 535#print axioms kineticCondition_on_ray_iff
 536#print axioms energyEqualsCost_on_ray_iff
 537#print axioms unit_norm_on_ray_iff
 538#print axioms scaleFreePackage_on_ray
 539#print axioms bridge_not_forced_by_scale_free_package
 540#print axioms exhibited_pair_disagrees_on_bridge
 541#print axioms sign_not_forced_with_unit_scale
 542#print axioms chart_product_of_stipulated_chart
 543#print axioms imbalance_orbitPoint_at_two_arsinh_one
 544#print axioms lam_of_signed_bridge
 545#print axioms lam_of_signed_bridge_at_stipulated_chart
 546#print axioms lam_sq_of_magnitude_bridge
 547#print axioms constants_cluster_of_magnitude_bridge
 548#print axioms lam_ground_state_of_signed_bridge
 549#print axioms ground_state_cluster_of_signed_bridge
 550#print axioms momentumBridgeVerdict
 551
 552end
 553
 554end MomentumBridge
 555end SevenGaps
 556end Gravity
 557end IndisputableMonolith
 558