IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong

   1import IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget
   2
   3/-!
   4# Wave C2 repair: strengthened point-split HKT target (decoy excluded)
   5
   6Codex adversarial pass `D-qg-hkt-pointsplit-adjudication-20260722` found that
   7`HKTPointSplitTargetDyn` is decoy-inhabitable (quartic zero-momentum) and that
   8rigidity over the weak class is therefore not a load-bearing grind target.
   9
  10This module lands:
  111. `HKTPointSplitTargetDynStrong` with load-bearing momentum, advection tied to
  12   the Mom–Ham bracket calculus, and kinetic regularity;
  132. explicit `quarticZeroMomTarget` inhabiting the WEAK schema (formal witness of
  14   the critic finding) and excluded from the strong class by
  15   `mom_load_bearing`;
  163. honest `hamDynPointSplitTargetStrong` inhabiting the strong class;
  174. `HKTRigidityStatementPointSplitDynN2Strong` (now PROVEN FALSE via the
  18   balanced-quartic falsifier in `HKTCanonicalMomTarget`; binding rigidity
  19   moves to CanonicalMom).
  20
  21No ledger flag is flipped. Discrimination gate: honest inhabitant passes,
  22quartic zero-momentum decoy fails. Strong-class rigidity is dead; see
  23`HKTCanonicalMomTarget`.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Gravity
  28namespace SevenGaps
  29namespace HKTPointSplitStrong
  30
  31open HypersurfaceDeformation DynamicStructureBracket DynamicStructureFunctionBlocker
  32open HKTPointSplitTarget
  33
  34noncomputable section
  35
  36open Finset
  37
  38/-! ## Computed advection from the Mom–Ham bracket calculus -/
  39
  40/-- Kronecker lapse / shift weight on `ZMod n`. -/
  41def siteDelta {n : ℕ} [NeZero n] (k : ZMod n) : ZMod n → ℝ :=
  42  fun j => if j = k then (1 : ℝ) else 0
  43
  44lemma siteDelta_self {n : ℕ} [NeZero n] (k : ZMod n) : siteDelta k k = (1 : ℝ) := by
  45  simp [siteDelta]
  46
  47lemma siteDelta_ne {n : ℕ} [NeZero n] {k j : ZMod n} (h : j ≠ k) :
  48    siteDelta k j = (0 : ℝ) := by
  49  simp [siteDelta, h]
  50
  51/-- Source advection recovered by evaluating `{Mom δ_j, Ham δ_j}`. -/
  52def computedHamAdvFrom {n : ℕ} [NeZero n] (T : HKTPointSplitTargetDyn n)
  53    (x : PhaseSpace n) (j : ZMod n) : ℝ :=
  54  -bracket (fun y => ∑ i : ZMod n, siteDelta j i * T.momDensity y i)
  55    (fun y => ∑ i : ZMod n, siteDelta j i * T.hamDensity y i) x
  56
  57/-- Target advection recovered by evaluating `{Mom δ_j, Ham δ_{j+1}}`. -/
  58def computedHamAdvTo {n : ℕ} [NeZero n] (T : HKTPointSplitTargetDyn n)
  59    (x : PhaseSpace n) (j : ZMod n) : ℝ :=
  60  bracket (fun y => ∑ i : ZMod n, siteDelta j i * T.momDensity y i)
  61    (fun y => ∑ i : ZMod n, siteDelta (j + 1) i * T.hamDensity y i) x
  62
  63private lemma zmod2_succ_ne (j : ZMod 2) : (j + 1 : ZMod 2) ≠ j := by
  64  fin_cases j <;> decide
  65
  66private lemma zmod2_zero_add_one' : (0 : ZMod 2) + 1 = 1 := by decide
  67private lemma zmod2_one_add_one' : (1 : ZMod 2) + 1 = 0 := by decide
  68
  69/-- Under `mom_ham_split` at `n = 2`, source slots equal the bracket-calculus values. -/
  70theorem hamAdvFrom_eq_computed (T : HKTPointSplitTargetDyn 2)
  71    (x : PhaseSpace 2) (j : ZMod 2) :
  72    T.hamAdvFrom x j = computedHamAdvFrom T x j := by
  73  have h := T.mom_ham_split (siteDelta j) (siteDelta j) x
  74  unfold computedHamAdvFrom
  75  have hsum :
  76      (∑ i : ZMod 2,
  77          siteDelta j i *
  78            (siteDelta j (i + 1) * T.hamAdvTo x i -
  79              siteDelta j i * T.hamAdvFrom x i))
  80        = -T.hamAdvFrom x j := by
  81    rw [Finset.sum_eq_single j]
  82    · have hj : siteDelta j j = (1 : ℝ) := siteDelta_self j
  83      have hjp : siteDelta j (j + 1) = (0 : ℝ) := by
  84        simp [siteDelta, zmod2_succ_ne j]
  85      simp [hj, hjp]
  86    · intro i _ hi
  87      simp [siteDelta, hi]
  88    · simp
  89  have hbr :
  90      bracket (fun y => ∑ i : ZMod 2, siteDelta j i * T.momDensity y i)
  91          (fun y => ∑ i : ZMod 2, siteDelta j i * T.hamDensity y i) x
  92        = -T.hamAdvFrom x j :=
  93    h.trans hsum
  94  linarith
  95
  96/-- Under `mom_ham_split` at `n = 2`, target slots equal the bracket-calculus values. -/
  97theorem hamAdvTo_eq_computed (T : HKTPointSplitTargetDyn 2)
  98    (x : PhaseSpace 2) (j : ZMod 2) :
  99    T.hamAdvTo x j = computedHamAdvTo T x j := by
 100  have h := T.mom_ham_split (siteDelta j) (siteDelta (j + 1)) x
 101  unfold computedHamAdvTo
 102  have hsum :
 103      (∑ i : ZMod 2,
 104          siteDelta j i *
 105            (siteDelta (j + 1) (i + 1) * T.hamAdvTo x i -
 106              siteDelta (j + 1) i * T.hamAdvFrom x i))
 107        = T.hamAdvTo x j := by
 108    rw [Finset.sum_eq_single j]
 109    · have hj : siteDelta j j = (1 : ℝ) := siteDelta_self j
 110      have hTo : siteDelta (j + 1) (j + 1) = (1 : ℝ) := siteDelta_self (j + 1)
 111      have hFrom : siteDelta (j + 1) j = (0 : ℝ) := by
 112        have : j ≠ (j + 1 : ZMod 2) := (zmod2_succ_ne j).symm
 113        simp [siteDelta, this]
 114      simp [hj, hTo, hFrom]
 115    · intro i _ hi
 116      simp [siteDelta, hi]
 117    · simp
 118  have hbr :
 119      bracket (fun y => ∑ i : ZMod 2, siteDelta j i * T.momDensity y i)
 120          (fun y => ∑ i : ZMod 2, siteDelta (j + 1) i * T.hamDensity y i) x
 121        = T.hamAdvTo x j :=
 122    h.trans hsum
 123  linarith
 124
 125/-! ## Strengthened target -/
 126
 127/-- STRENGTHENED TARGET. Extends the weak schema with three critic strengthenings:
 128(1) load-bearing momentum (nontrivial `{Mom, Mom}` bracket);
 129(2) advection slots equal the Mom–Ham bracket-calculus extractions
 130    (`computedHamAdvFrom` / `computedHamAdvTo`), not free decorative choices;
 131(3) kinetic regularity (some smeared-Ham momentum partial is nonzero),
 132    excluding purely potential densities.
 133
 134The weak schema `HKTPointSplitTargetDyn` remains as documentation of the
 135decoy-inhabitable class. -/
 136structure HKTPointSplitTargetDynStrong (n : ℕ) [NeZero n]
 137    extends HKTPointSplitTargetDyn n where
 138  /-- (1) `momDensity` generates a nontrivial bracket. -/
 139  mom_load_bearing :
 140    ∃ (v w : ZMod n → ℝ) (x : PhaseSpace n),
 141      bracket (fun y => ∑ j : ZMod n, v j * momDensity y j)
 142          (fun y => ∑ j : ZMod n, w j * momDensity y j) x ≠ 0
 143  /-- (2) Source advection is the bracket-calculus value of `hamDensity`/`momDensity`. -/
 144  advFrom_tied : ∀ (x : PhaseSpace n) (j : ZMod n),
 145    hamAdvFrom x j = computedHamAdvFrom toHKTPointSplitTargetDyn x j
 146  /-- (2) Target advection is the bracket-calculus value of `hamDensity`/`momDensity`. -/
 147  advTo_tied : ∀ (x : PhaseSpace n) (j : ZMod n),
 148    hamAdvTo x j = computedHamAdvTo toHKTPointSplitTargetDyn x j
 149  /-- (3) Kinetic regularity: some π-partial of the unsmeared unit-lapse Ham is nonzero. -/
 150  kinetic_regular :
 151    ∃ (x : PhaseSpace n) (j : ZMod n),
 152      pderivP (fun y => ∑ i : ZMod n, hamDensity y i) j x ≠ 0
 153
 154/-! ## Quartic zero-momentum decoy (inhabits WEAK; fails STRONG) -/
 155
 156/-- MODEL. Quartic kinetic density on two sites: `h_j = π_j^4`. -/
 157def quarticHamDensity2 (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 158  (x.2 j) ^ 4
 159
 160/-- MODEL. Vanishing momentum density (the decoy). -/
 161def zeroMomDensity2 (_x : PhaseSpace 2) (_j : ZMod 2) : ℝ :=
 162  0
 163
 164/-- Decorative nonconstant structure (same shape as `structureDyn`). -/
 165def decorativeStructure2 (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 166  1 + x.1 j * x.1 j
 167
 168def quarticHam2 (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
 169  ∑ j : ZMod 2, N j * quarticHamDensity2 x j
 170
 171def quarticHam2D (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
 172  ∑ i : ZMod 2, N i • ((4 • (x.2 i) ^ 3) • coordP i)
 173
 174lemma hasFDerivAt_quarticHam2 (N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 175    HasFDerivAt (quarticHam2 N) (quarticHam2D N x) x := by
 176  unfold quarticHam2 quarticHam2D quarticHamDensity2
 177  exact HasFDerivAt.fun_sum fun i _ =>
 178    ((hasFDerivAt_coord_snd i x).pow 4).const_mul (N i)
 179
 180theorem differentiable_quarticHam2 (N : ZMod 2 → ℝ) :
 181    Differentiable ℝ (quarticHam2 N) :=
 182  fun x => (hasFDerivAt_quarticHam2 N x).differentiableAt
 183
 184lemma pderivQ_quarticHam2 (N : ZMod 2 → ℝ) (j : ZMod 2) (x : PhaseSpace 2) :
 185    pderivQ (quarticHam2 N) j x = 0 := by
 186  rw [pderivQ, (hasFDerivAt_quarticHam2 N x).fderiv, quarticHam2D,
 187    ContinuousLinearMap.sum_apply]
 188  refine Finset.sum_eq_zero fun i _ => ?_
 189  simp [coordP]
 190
 191theorem bracket_quarticHam2_quarticHam2 (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 192    bracket (quarticHam2 N) (quarticHam2 M) x = 0 := by
 193  simp only [bracket, pderivQ_quarticHam2]
 194  exact Finset.sum_eq_zero fun _ _ => by ring
 195
 196lemma zeroMom2_eq_zero (w : ZMod 2 → ℝ) :
 197    (fun x : PhaseSpace 2 => ∑ j : ZMod 2, w j * zeroMomDensity2 x j)
 198      = fun _ => (0 : ℝ) := by
 199  funext y
 200  simp [zeroMomDensity2]
 201
 202lemma differentiable_zeroMom2 (w : ZMod 2 → ℝ) :
 203    Differentiable ℝ
 204      (fun x : PhaseSpace 2 => ∑ j : ZMod 2, w j * zeroMomDensity2 x j) := by
 205  rw [zeroMom2_eq_zero]
 206  exact differentiable_const 0
 207
 208lemma bracket_zeroMom2_any (w : ZMod 2 → ℝ) (G : PhaseSpace 2 → ℝ)
 209    (x : PhaseSpace 2) :
 210    bracket (fun y => ∑ j : ZMod 2, w j * zeroMomDensity2 y j) G x = 0 := by
 211  have hz := zeroMom2_eq_zero w
 212  simp only [bracket, pderivQ, pderivP]
 213  have hQ : ∀ i, fderiv ℝ (fun y => ∑ j : ZMod 2, w j * zeroMomDensity2 y j) x
 214      (Pi.single i 1, 0) = 0 := by
 215    intro i
 216    rw [hz]
 217    simp
 218  have hP : ∀ i, fderiv ℝ (fun y => ∑ j : ZMod 2, w j * zeroMomDensity2 y j) x
 219      (0, Pi.single i 1) = 0 := by
 220    intro i
 221    rw [hz]
 222    simp
 223  refine Finset.sum_eq_zero fun i _ => ?_
 224  simp [hQ i, hP i]
 225
 226lemma decorativeStructure2_not_constant : ¬ PhaseSpaceConstant decorativeStructure2 := by
 227  intro h
 228  have hEq := h zeroPhasePoint unitConfigurationPoint (0 : ZMod 2)
 229  simp only [decorativeStructure2, zeroPhasePoint, unitConfigurationPoint] at hEq
 230  norm_num at hEq
 231
 232def quarticNondegPhase : PhaseSpace 2 :=
 233  (fun _ => (0 : ℝ), fun j => if j = (0 : ZMod 2) then (1 : ℝ) else 0)
 234
 235theorem quarticHamDensity2_nondeg :
 236    quarticHamDensity2 quarticNondegPhase (0 : ZMod 2) ≠ 0 := by
 237  simp only [quarticHamDensity2, quarticNondegPhase]
 238  norm_num
 239
 240/-- THEOREM. Quartic zero-momentum decoy inhabits the WEAK point-split schema.
 241Formal witness that `HKTPointSplitTargetDyn` is decoy-inhabitable
 242(`D-qg-hkt-pointsplit-adjudication-20260722`). -/
 243def quarticZeroMomTarget : HKTPointSplitTargetDyn 2 where
 244  hamDensity := quarticHamDensity2
 245  momDensity := zeroMomDensity2
 246  structureFunction := decorativeStructure2
 247  hamAdvFrom := fun _ _ => 0
 248  hamAdvTo := fun _ _ => 0
 249  momBracketDensity := fun _ _ => 0
 250  ham_differentiable := by
 251    intro N
 252    simpa [quarticHam2, quarticHamDensity2] using differentiable_quarticHam2 N
 253  mom_differentiable := differentiable_zeroMom2
 254  structure_nonconstant := decorativeStructure2_not_constant
 255  ham_local := by
 256    intro x y j _ _ hp
 257    dsimp only [quarticHamDensity2]
 258    rw [hp]
 259  ham_covariant := by
 260    intro x a j
 261    rfl
 262  structure_local := by
 263    intro x y j hx
 264    dsimp only [decorativeStructure2]
 265    rw [hx]
 266  mom_mom := by
 267    intro v w x
 268    have hL := bracket_zeroMom2_any v
 269      (fun y => ∑ j : ZMod 2, w j * zeroMomDensity2 y j) x
 270    -- Both sides vanish: LHS by zero mom, RHS by zero momBracketDensity.
 271    simpa [zeroMomDensity2] using hL
 272  mom_ham_split := by
 273    intro w N x
 274    have hL := bracket_zeroMom2_any w
 275      (fun y => ∑ j : ZMod 2, N j * quarticHamDensity2 y j) x
 276    -- Both sides vanish: LHS by zero mom, RHS by zero Adv slots.
 277    simpa [zeroMomDensity2] using hL
 278  ham_ham := by
 279    intro N M x
 280    have hL := bracket_quarticHam2_quarticHam2 N M x
 281    -- LHS vanishes (pure-π generators); RHS has zero momDensity factor.
 282    simpa [quarticHam2, quarticHamDensity2, zeroMomDensity2] using hL
 283  nondegenerate := ⟨quarticNondegPhase, (0 : ZMod 2), quarticHamDensity2_nondeg⟩
 284
 285theorem quarticZeroMomTarget_mom_vanishes (x : PhaseSpace 2) (j : ZMod 2) :
 286    quarticZeroMomTarget.momDensity x j = 0 :=
 287  rfl
 288
 289/-- The zero-momentum decoy has identically vanishing Mom–Mom brackets.
 290This is the strengthening field that kills it. -/
 291theorem quarticZeroMom_fails_mom_load_bearing :
 292    ¬ ∃ (v w : ZMod 2 → ℝ) (x : PhaseSpace 2),
 293      bracket (fun y => ∑ j : ZMod 2, v j * quarticZeroMomTarget.momDensity y j)
 294          (fun y => ∑ j : ZMod 2, w j * quarticZeroMomTarget.momDensity y j) x ≠ 0 := by
 295  rintro ⟨v, w, x, hne⟩
 296  have h := bracket_zeroMom2_any v
 297    (fun y => ∑ j : ZMod 2, w j * zeroMomDensity2 y j) x
 298  exact hne h
 299
 300/-- THEOREM. The quartic zero-momentum decoy does **not** inhabit the
 301strengthened class. Killed by `mom_load_bearing`. -/
 302theorem quarticZeroMomTarget_not_strong :
 303    ¬ ∃ S : HKTPointSplitTargetDynStrong 2,
 304      S.toHKTPointSplitTargetDyn = quarticZeroMomTarget := by
 305  rintro ⟨S, hEq⟩
 306  have hBear := S.mom_load_bearing
 307  have hMom : S.momDensity = quarticZeroMomTarget.momDensity := by
 308    rw [← hEq]
 309  rw [hMom] at hBear
 310  exact quarticZeroMom_fails_mom_load_bearing hBear
 311
 312/-! ## Honest HamDyn inhabitant of the strengthened class -/
 313
 314def momLoadBearingWitnessPhase : PhaseSpace 2 :=
 315  (fun j : ZMod 2 => if j = (0 : ZMod 2) then (0 : ℝ) else 1,
 316    fun j : ZMod 2 => if j = (0 : ZMod 2) then (1 : ℝ) else 0)
 317
 318private lemma momLoadBearingWitness_vals :
 319    momLoadBearingWitnessPhase.1 (0 : ZMod 2) = 0 ∧
 320      momLoadBearingWitnessPhase.1 (1 : ZMod 2) = 1 ∧
 321        momLoadBearingWitnessPhase.2 (0 : ZMod 2) = 1 ∧
 322          momLoadBearingWitnessPhase.2 (1 : ZMod 2) = 0 := by
 323  simp [momLoadBearingWitnessPhase]
 324
 325theorem hamDyn_mom_load_bearing_witness :
 326    bracket (MomDyn delta0) (MomDyn delta1) momLoadBearingWitnessPhase ≠ 0 := by
 327  have hv := momLoadBearingWitness_vals
 328  have h := bracket_MomDyn_MomDyn delta0 delta1 momLoadBearingWitnessPhase
 329  have hδ0 : delta0 (0 : ZMod 2) = (1 : ℝ) ∧ delta0 (1 : ZMod 2) = 0 := by simp [delta0]
 330  have hδ1 : delta1 (0 : ZMod 2) = (0 : ℝ) ∧ delta1 (1 : ZMod 2) = 1 := by simp [delta1]
 331  have hd0 : momDynBracketDensity momLoadBearingWitnessPhase (0 : ZMod 2) = (1 : ℝ) / 2 := by
 332    simp only [momDynBracketDensity, zmod2_zero_add_one', hv.1, hv.2.1, hv.2.2.1, hv.2.2.2]
 333    norm_num
 334  have hd1 : momDynBracketDensity momLoadBearingWitnessPhase (1 : ZMod 2) = (-1 : ℝ) / 2 := by
 335    simp only [momDynBracketDensity, zmod2_one_add_one', hv.1, hv.2.1, hv.2.2.1, hv.2.2.2]
 336    norm_num
 337  -- Coeffs: j=0 → 1, j=1 → -1; sum = 1/2 + 1/2 = 1.
 338  rw [h, sum_zmod2, zmod2_zero_add_one', zmod2_one_add_one', hδ0.1, hδ0.2, hδ1.1, hδ1.2, hd0,
 339    hd1]
 340  norm_num
 341
 342theorem hamDyn_kinetic_regular_witness :
 343    pderivP (fun y => ∑ i : ZMod 2, hamDynDensity y i) (0 : ZMod 2)
 344        hamDynNondegPhase ≠ 0 := by
 345  have hEq : (fun y => ∑ i : ZMod 2, hamDynDensity y i) = HamDyn (fun _ => (1 : ℝ)) := by
 346    funext y
 347    have h := congrArg (fun F : PhaseSpace 2 → ℝ => F y)
 348      (hamDynDensity_smear (fun _ => (1 : ℝ)))
 349    -- h : ∑ 1 * ham = HamDyn 1; simplify the unit weights.
 350    simpa using h
 351  rw [hEq, pderivP_HamDyn]
 352  simp only [hamDynNondegPhase]
 353  norm_num
 354
 355/-- THEOREM. Honest HamDyn inhabitant of the strengthened point-split target. -/
 356def hamDynPointSplitTargetStrong : HKTPointSplitTargetDynStrong 2 where
 357  toHKTPointSplitTargetDyn := hamDynPointSplitTarget
 358  mom_load_bearing := by
 359    refine ⟨delta0, delta1, momLoadBearingWitnessPhase, ?_⟩
 360    simpa [MomDyn] using hamDyn_mom_load_bearing_witness
 361  advFrom_tied := by
 362    intro x j
 363    simpa using hamAdvFrom_eq_computed hamDynPointSplitTarget x j
 364  advTo_tied := by
 365    intro x j
 366    simpa using hamAdvTo_eq_computed hamDynPointSplitTarget x j
 367  kinetic_regular :=
 368    ⟨hamDynNondegPhase, (0 : ZMod 2), hamDyn_kinetic_regular_witness⟩
 369
 370theorem hktPointSplitTargetDynStrong_two_nonvacuous :
 371    Nonempty (HKTPointSplitTargetDynStrong 2) :=
 372  ⟨hamDynPointSplitTargetStrong⟩
 373
 374/-- Discrimination receipt: honest passes strong; decoy fails strong. -/
 375theorem strong_target_discriminates_decoy :
 376    (Nonempty (HKTPointSplitTargetDynStrong 2)) ∧
 377      (¬ ∃ S : HKTPointSplitTargetDynStrong 2,
 378        S.toHKTPointSplitTargetDyn = quarticZeroMomTarget) :=
 379  ⟨hktPointSplitTargetDynStrong_two_nonvacuous, quarticZeroMomTarget_not_strong⟩
 380
 381/-! ## Binding rigidity Prop over the strengthened class (PROVEN FALSE) -/
 382
 383/-- PROVEN FALSE. Formerly the GR-strength rigidity target over
 384`HKTPointSplitTargetDynStrong` at `n = 2`. Killed by the balanced-quartic
 385inhabitant (`quarticBalancedStrongTarget`) in
 386`HKTCanonicalMomTarget.not_HKTRigidityStatementPointSplitDynN2Strong`
 387(`D-qg-hkt-rigidity-route-20260722`). Binding rigidity moves to
 388`HKTRigidityStatementPointSplitDynN2Canonical` over the CanonicalMom class. -/
 389def HKTRigidityStatementPointSplitDynN2Strong : Prop :=
 390  ∀ T : HKTPointSplitTargetDynStrong 2,
 391    ∃ cKin cGrad cVac : ℝ, ∀ (x : PhaseSpace 2) (j : ZMod 2),
 392      T.hamDensity x j
 393        = cKin * (x.2 j * x.2 j)
 394          + cGrad *
 395              (T.structureFunction x j *
 396                ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)))
 397          + cVac
 398
 399/-! ### Axiom receipts -/
 400
 401#print axioms hamAdvFrom_eq_computed
 402#print axioms hamAdvTo_eq_computed
 403#print axioms quarticZeroMomTarget_not_strong
 404#print axioms hamDyn_mom_load_bearing_witness
 405#print axioms hamDyn_kinetic_regular_witness
 406#print axioms hktPointSplitTargetDynStrong_two_nonvacuous
 407#print axioms strong_target_discriminates_decoy
 408
 409end
 410end HKTPointSplitStrong
 411end SevenGaps
 412end Gravity
 413end IndisputableMonolith
 414