IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly

   1import Mathlib.Analysis.SpecialFunctions.Arcosh
   2import Mathlib.Analysis.SpecialFunctions.Complex.Arg
   3import Mathlib.Analysis.SpecialFunctions.Complex.Log
   4import Mathlib.Analysis.SpecialFunctions.Pow.Complex
   5import Mathlib.Tactic.Linarith
   6import Mathlib.Tactic.NormNum
   7import Mathlib.Tactic.Ring
   8import IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D
   9import IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency
  10import IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst
  11import IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit
  12import IndisputableMonolith.Gravity.SevenGaps.WickActionEuclidSchlaefli
  13import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  14import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement
  15import IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
  16import IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges
  17
  18/-!
  19# Wave C4 R5: certificate assembly at α = 1 (partial receipt)
  20
  21Binding adjudication: `D-gap6-r5-assembly-adjudication-20260723`.
  22
  23## Obligation 0 (attack first)
  24
  25Compare the pointwise value `carccos (pentHingeCosPath 1 0)` with the N4
  26one-sided cut limit `π + I · arcosh(11/8)`.
  27
  28**Outcome B (landed):** they disagree. The principal log branch at the real
  29cut cosine `-(11/8)` yields
  30`carccos(-(11/8)) = π - I · arcosh(11/8)`, while N4's lower-half approach
  31lands on `π + I · arcosh(11/8)`. Hence the frozen `contAction` field
  32`ContinuousOn (wickActionPath 1) (Icc 0 1)` is unsatisfiable (value/limit
  33mismatch at the cut). We prove the named no-go and assemble the repaired
  34certificate `WickActionContinuationCertV2 1`.
  35
  36## Honesty walls
  37
  38* `euclidSchlaefli` certifies differentiability of the Euclidean-endpoint
  39  action on the collapsed one-hinge geometry, **not** classical multi-hinge
  40  Schläfli cancellation `Σ A θ' = 0` (which fails here; see
  41  `WickActionEuclidSchlaefli.euclid_angle_deriv_term_ne_zero_at_one`).
  42* Historical R5 partial receipt assembled CertV2 at α = 1 only. That
  43  partial-open posture is **superseded** (2026-07-23): family assembly
  44  landed in `WickActionCertFamilyAssembly.lean`; V2 terminal
  45  `wick_action_continuation_4d_v2_holds`; ledger flip receipted in
  46  `WickActionV2CloseStatus.lean` (`gap6_lorentzian_action_bound_to_v2`).
  47  Status block below records `gap6LorentzianAction := true` /
  48  `familyV2Open := false`. Frozen V1 `wick_action_continuation_4d` remains
  49  retired (`not_wick_action_continuation_4d` / contAction unsatisfiable).
  50-/
  51
  52namespace IndisputableMonolith
  53namespace Gravity
  54namespace SevenGaps
  55namespace WickActionInteriorHinge
  56
  57open Complex
  58open Filter Topology
  59open CausalSimplex4D
  60open ThreePentCausalConsistency
  61open WickActionComplexFirst
  62open WickFourOneAllHinges (csqrt_ofReal_neg csqrt_ofReal_nonneg)
  63open WickThreeTwoHinges
  64
  65noncomputable section
  66
  67/-! ## §0. Decisive cut computation (Outcome B) -/
  68
  69private lemma sqrt57_div_eight :
  70    Real.sqrt (57 / 64) = Real.sqrt 57 / 8 := by
  71  have h64 : Real.sqrt (64 : ℝ) = 8 := by
  72    have : (64 : ℝ) = 8 ^ 2 := by norm_num
  73    rw [this, Real.sqrt_sq (by norm_num)]
  74  calc
  75    Real.sqrt (57 / 64) = Real.sqrt 57 / Real.sqrt 64 :=
  76      Real.sqrt_div (by norm_num : (0 : ℝ) ≤ 57) 64
  77    _ = Real.sqrt 57 / 8 := by rw [h64]
  78
  79private lemma arcosh_eleven_over_eight :
  80    Real.arcosh (11 / 8) = Real.log ((11 + Real.sqrt 57) / 8) := by
  81  rw [Real.arcosh]
  82  have hsq : (11 / 8 : ℝ) ^ 2 - 1 = 57 / 64 := by norm_num
  83  have hsqrt : Real.sqrt ((11 / 8 : ℝ) ^ 2 - 1) = Real.sqrt 57 / 8 := by
  84    rw [hsq, sqrt57_div_eight]
  85  have hsum :
  86      (11 / 8 : ℝ) + Real.sqrt ((11 / 8) ^ 2 - 1) =
  87        (11 + Real.sqrt 57) / 8 := by
  88    rw [hsqrt]; ring
  89  rw [hsum]
  90
  91/-- Pointwise principal value of `carccos` at the Lorentzian cut cosine. -/
  92theorem carccos_at_lorentz_cut_one :
  93    carccos (pentHingeCosPath 1 0) =
  94      (↑(Real.pi) : ℂ) - I * ↑(Real.arcosh (11 / 8)) := by
  95  rw [pentHingeCosPath_one_zero, lorentzCos_one]
  96  set x : ℝ := -(11 / 8)
  97  have hone_sub :
  98      (1 : ℂ) - (↑x : ℂ) ^ 2 = ↑(-(57 / 64 : ℝ)) := by
  99    simp only [x, ofReal_neg, ofReal_div, ofReal_ofNat]
 100    norm_num
 101  have hcs :
 102      csqrt ((1 : ℂ) - (↑x : ℂ) ^ 2) =
 103        ↑(Real.sqrt (57 / 64)) * I := by
 104    have hneg : (-(57 / 64 : ℝ)) < 0 := by norm_num
 105    have h := csqrt_ofReal_neg hneg
 106    simpa [hone_sub, ofReal_neg] using h
 107  have hI :
 108      I * (↑(Real.sqrt 57 / 8 : ℝ) * I) = -↑(Real.sqrt 57 / 8 : ℝ) := by
 109    set r : ℂ := ↑(Real.sqrt 57 / 8 : ℝ)
 110    calc
 111      I * (r * I) = (I * I) * r := by ring
 112      _ = (-1 : ℂ) * r := by rw [I_mul_I]
 113      _ = -r := by ring
 114  have harg :
 115      (↑x : ℂ) + I * csqrt ((1 : ℂ) - (↑x : ℂ) ^ 2) =
 116        ↑(-(11 + Real.sqrt 57) / 8 : ℝ) := by
 117    rw [hcs, sqrt57_div_eight, hI]
 118    have hx : (↑x : ℂ) = ↑(-(11 / 8 : ℝ)) := by simp [x]
 119    rw [hx]
 120    have :
 121        (↑(-(11 / 8 : ℝ)) : ℂ) + (-↑(Real.sqrt 57 / 8 : ℝ)) =
 122          ↑(-(11 + Real.sqrt 57) / 8 : ℝ) := by
 123      simp [ofReal_neg, ofReal_div, ofReal_ofNat, ofReal_add]
 124      ring
 125    -- after hI rewrite the goal is ofReal + (-ofReal)
 126    simpa [sub_eq_add_neg] using this
 127  have harg_neg : (-(11 + Real.sqrt 57) / 8 : ℝ) < 0 := by
 128    have hsqrt : 0 ≤ Real.sqrt 57 := Real.sqrt_nonneg _
 129    linarith [hsqrt]
 130  have hlog :
 131      log (↑x + I * csqrt ((1 : ℂ) - (↑x : ℂ) ^ 2)) =
 132        ↑(Real.log ((11 + Real.sqrt 57) / 8)) + (Real.pi : ℂ) * I := by
 133    rw [harg]
 134    have hnorm :
 135        ‖(↑(-(11 + Real.sqrt 57) / 8 : ℝ) : ℂ)‖ =
 136          (11 + Real.sqrt 57) / 8 := by
 137      rw [Complex.norm_real, Real.norm_eq_abs, abs_of_neg harg_neg]
 138      ring
 139    apply Complex.ext
 140    · rw [log_re, hnorm]
 141      simp [add_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]
 142    · rw [log_im, arg_ofReal_of_neg harg_neg]
 143      simp [add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]
 144  have hnegI_pi : (-I) * ((Real.pi : ℂ) * I) = (Real.pi : ℂ) := by
 145    have hII : (-I) * I = (1 : ℂ) := by
 146      simp [neg_mul, I_mul_I]
 147    calc
 148      (-I) * ((Real.pi : ℂ) * I) = ((-I) * I) * (Real.pi : ℂ) := by ring
 149      _ = (1 : ℂ) * (Real.pi : ℂ) := by rw [hII]
 150      _ = (Real.pi : ℂ) := by ring
 151  have hcarc :
 152      carccos (↑x : ℂ) =
 153        (↑(Real.pi) : ℂ) - I * ↑(Real.log ((11 + Real.sqrt 57) / 8)) := by
 154    simp only [carccos, hlog]
 155    have h1 :
 156        (-I) * (↑(Real.log ((11 + Real.sqrt 57) / 8)) + (Real.pi : ℂ) * I) =
 157          (-I) * ↑(Real.log ((11 + Real.sqrt 57) / 8)) +
 158            (-I) * ((Real.pi : ℂ) * I) := by
 159      rw [mul_add]
 160    rw [h1, hnegI_pi]
 161    ring
 162  rw [hcarc, arcosh_eleven_over_eight]
 163
 164/-- N4 disclosed cut limit for `carccos` at α = 1. -/
 165theorem carccos_cut_limit_value_one :
 166    (↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1) =
 167      (↑(Real.pi) : ℂ) + I * ↑(Real.arcosh (11 / 8)) := by
 168  unfold lorentzAngleRe lorentzRapidity
 169  rw [lorentzCos_one, abs_neg, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 11 / 8)]
 170
 171/-- Decisive mismatch: pointwise principal value ≠ one-sided cut limit. -/
 172theorem carccos_value_ne_cut_limit_one :
 173    carccos (pentHingeCosPath 1 0) ≠
 174      (↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1) := by
 175  rw [carccos_at_lorentz_cut_one, carccos_cut_limit_value_one]
 176  set R : ℝ := Real.arcosh (11 / 8)
 177  have hR : 0 < R := by
 178    dsimp [R]
 179    exact Real.arcosh_pos (by norm_num : (1 : ℝ) < 11 / 8)
 180  intro h
 181  -- π - I R = π + I R ⇒ -I R = I R ⇒ 2 I R = 0 ⇒ R = 0
 182  have h' :
 183      (↑(Real.pi) : ℂ) - I * ↑R = (↑(Real.pi) : ℂ) + I * ↑R := h
 184  have hsub :
 185      ((↑(Real.pi) : ℂ) - I * ↑R) - ((↑(Real.pi) : ℂ) + I * ↑R) = 0 := by
 186    rw [h']; ring
 187  have h2 : (-(2 : ℂ) * I) * ↑R = 0 := by
 188    convert hsub using 1
 189    ring
 190  have hI2 : (-(2 : ℂ) * I) ≠ 0 :=
 191    mul_ne_zero (neg_ne_zero.mpr (by norm_num : (2 : ℂ) ≠ 0)) I_ne_zero
 192  have hR0 : (↑R : ℂ) = 0 :=
 193    (mul_eq_zero.mp h2).resolve_left hI2
 194  exact hR.ne' (ofReal_eq_zero.mp hR0)
 195
 196/-! ## §1. No-go: frozen `contAction` unsatisfiable at α = 1 -/
 197
 198private lemma wickActionPath_zero_ne_lorentz_limit :
 199    wickActionPath 1 0 ≠
 200      (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe 1) : ℝ) : ℂ) -
 201        I * ((hingeArea * (3 * lorentzRapidity 1) : ℝ) : ℂ)) := by
 202  intro heq
 203  -- Expand both sides through dihedralSumPath / carccos
 204  have hL :
 205      (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe 1) : ℝ) : ℂ) -
 206          I * ((hingeArea * (3 * lorentzRapidity 1) : ℝ) : ℂ)) =
 207        (hingeArea : ℂ) *
 208          ((2 * Real.pi : ℂ) -
 209            3 *
 210              ((↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1))) := by
 211    unfold lorentzAngleRe
 212    simp [ofReal_mul, ofReal_add, ofReal_sub, mul_add, sub_eq_add_neg]
 213    ring
 214  have hV :
 215      wickActionPath 1 0 =
 216        (hingeArea : ℂ) *
 217          ((2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath 1 0)) := by
 218    unfold wickActionPath dihedralSumPath; rfl
 219  rw [hV, hL] at heq
 220  have hA : (hingeArea : ℂ) ≠ 0 := by
 221    have : (0 : ℝ) < hingeArea :=
 222      Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 3 / 16)
 223    exact ofReal_ne_zero.mpr this.ne'
 224  have hmul := mul_left_cancel₀ hA heq
 225  -- 2π - 3 v = 2π - 3 L ⇒ v = L
 226  have hv :
 227      carccos (pentHingeCosPath 1 0) =
 228        (↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1) := by
 229    have h3 : (3 : ℂ) ≠ 0 := by norm_num
 230    -- hmul : 2π - 3 v = 2π - 3 L  ⇒  3 v = 3 L
 231    exact mul_left_cancel₀ h3 (sub_right_inj.mp hmul)
 232  exact carccos_value_ne_cut_limit_one hv
 233
 234/-- ContinuousOn on `Icc 0 1` forces the right-limit at 0 to equal `f 0`. -/
 235private lemma tendsto_Ioi_of_continuousOn_Icc
 236    {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Icc 0 1)) :
 237    Tendsto f (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (f 0)) := by
 238  rw [Metric.tendsto_nhdsWithin_nhds]
 239  intro ε hε
 240  have hcw :=
 241    hf.continuousWithinAt (Set.left_mem_Icc.mpr (by norm_num : (0 : ℝ) ≤ 1))
 242  rw [Metric.continuousWithinAt_iff] at hcw
 243  obtain ⟨δ, hδ, hδf⟩ := hcw ε hε
 244  refine ⟨min δ 1, lt_min hδ (by norm_num : (0 : ℝ) < 1), ?_⟩
 245  intro x hx hxδ
 246  have hxδ' : dist x (0 : ℝ) < δ := (lt_min_iff.mp hxδ).1
 247  have hxlt : x < 1 := by
 248    have : dist x (0 : ℝ) < 1 := (lt_min_iff.mp hxδ).2
 249    -- x > 0 ⇒ dist = x
 250    have hxpos : 0 < x := hx
 251    have : |x| < 1 := by simpa [Real.dist_eq] using this
 252    rw [abs_of_pos hxpos] at this
 253    exact this
 254  exact hδf ⟨le_of_lt hx, le_of_lt hxlt⟩ hxδ'
 255
 256/-- Named no-go: frozen `contAction` field is unsatisfiable at α = 1. -/
 257theorem contAction_not_satisfiable_at_one :
 258    ¬ ContinuousOn (wickActionPath 1) (Set.Icc 0 1) := by
 259  intro hcont
 260  have hval :=
 261    tendsto_Ioi_of_continuousOn_Icc (f := wickActionPath 1) hcont
 262  have hlim := lorentzAnchor_one_holds
 263  have huniq := tendsto_nhds_unique hval hlim
 264  exact wickActionPath_zero_ne_lorentz_limit huniq
 265
 266/-! ## §2. Repaired certificate schema (V2) -/
 267
 268/-- Repaired action-level Wick continuation certificate: replaces the
 269unsatisfiable closed-interval `contAction` by interior continuity on
 270`Ioc 0 1` plus an explicit one-sided cut `Tendsto` (standard branch-cut
 271resolution). All other fields match `WickActionContinuationCert` verbatim.
 272
 273Honesty (`euclidSchlaefli`): this field certifies differentiability of the
 274Euclidean endpoint action on the collapsed one-hinge geometry, **not**
 275classical multi-hinge Schläfli cancellation `Σ A θ' = 0` (provably fails
 276on one hinge; see `euclid_angle_deriv_term_ne_zero_at_one`). -/
 277structure WickActionContinuationCertV2 (α : ℝ) : Prop where
 278  causalRange : (7 / 12 : ℝ) < α
 279  chartsAgree :
 280    inducedSqEdges pentAVert 1 α =
 281        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α ∧
 282      inducedSqEdges pentBVert 1 α =
 283        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α ∧
 284      inducedSqEdges pentCVert 1 α =
 285        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α
 286  branchRegularSum :
 287    ∀ t ∈ Set.Ioo (0 : ℝ) 1,
 288      OffArccosCut (pentHingeCosPath α t) ∧
 289        (1 - pentHingeCosPath α t ^ 2) ∈ slitPlane ∧
 290          (pentHingeCosPath α t + I * csqrt (1 - pentHingeCosPath α t ^ 2)) ∈
 291            slitPlane
 292  /-- Continuous on the open-at-cut interval (honest replacement for
 293  closed-interval continuity through the branch cut). -/
 294  contActionInterior : ContinuousOn (wickActionPath α) (Set.Ioc 0 1)
 295  /-- One-sided cut limit pinned separately (disclosed Lorentzian boundary). -/
 296  cutLimit :
 297    Filter.Tendsto (wickActionPath α) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
 298      (nhds
 299        (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe α) : ℝ) : ℂ) -
 300          I * ((hingeArea * (3 * lorentzRapidity α) : ℝ) : ℂ)))
 301  euclidCosReal :
 302    pentHingeCosPath α 1 = ((euclidCos α : ℝ) : ℂ) ∧
 303      (α = 1 → euclidCos α = -(1 / 4))
 304  euclidAnchor :
 305    wickActionPath α 1 =
 306      ((hingeArea * (2 * Real.pi - 3 * Real.arccos (euclidCos α)) : ℝ) : ℂ)
 307  lorentzAnchor :
 308    Filter.Tendsto (wickActionPath α) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
 309      (nhds
 310        (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe α) : ℝ) : ℂ) -
 311          I * ((hingeArea * (3 * lorentzRapidity α) : ℝ) : ℂ)))
 312  rapidityPinned : lorentzRapidity α ≠ 0
 313  /-- Differentiability of Euclidean-endpoint action (NOT classical Schläfli
 314  cancellation; see module docstring). -/
 315  euclidSchlaefli :
 316    ∃ dS : ℝ, HasDerivAt (fun β : ℝ => (wickActionPath β 1).re) dS α
 317
 318/-- Ledger family Prop for the repaired certificate. LEFT OPEN / uninhabited. -/
 319def wick_action_continuation_v2_family : Prop :=
 320  ∀ α : ℝ, (7 / 12 : ℝ) < α → WickActionContinuationCertV2 α
 321
 322/-- Named α = 1 package Prop (inhabited below). Does **not** close the
 323ledger terminal `wick_action_continuation_4d`, which still demands the
 324frozen V1 family. -/
 325def wick_action_continuation_v2_at_one : Prop :=
 326  WickActionContinuationCertV2 1
 327
 328/-! ## §3. Interior continuity on `Ioc 0 1` -/
 329
 330theorem offArccosCut_pentHingeCosPath_Ioc_one {t : ℝ}
 331    (ht : t ∈ Set.Ioc (0 : ℝ) 1) :
 332    OffArccosCut (pentHingeCosPath 1 t) := by
 333  rcases ht with ⟨ht0, ht1⟩
 334  rcases lt_or_eq_of_le ht1 with ht1' | rfl
 335  · exact Or.inl (im_pentHingeCosPath_neg_one ⟨ht0, ht1'⟩).ne
 336  · -- t = 1: Euclidean cosine -(1/4) ∈ (-1,1)
 337    refine Or.inr ?_
 338    rw [pentHingeCosPath_one_one, euclidCos_one]
 339    constructor <;> norm_num
 340
 341theorem continuousOn_pentHingeCosPath_Ioc_one :
 342    ContinuousOn (pentHingeCosPath 1) (Set.Ioc 0 1) := by
 343  have h := (boundary_threeTwo_spacelike).1
 344  have heq : pentHingeCosPath 1 = threeTwoCosPath 3 4 :=
 345    pentHingeCosPath_one_eq_threeTwo
 346  simpa [heq] using h.mono Set.Ioc_subset_Icc_self
 347
 348theorem continuousOn_carccos_comp_pent_Ioc_one :
 349    ContinuousOn (fun t => carccos (pentHingeCosPath 1 t)) (Set.Ioc 0 1) := by
 350  have hpath := continuousOn_pentHingeCosPath_Ioc_one
 351  have hmaps :
 352      Set.MapsTo (pentHingeCosPath 1) (Set.Ioc 0 1) {w | OffArccosCut w} :=
 353    fun _ ht => offArccosCut_pentHingeCosPath_Ioc_one ht
 354  exact continuousOn_carccos.comp hpath hmaps
 355
 356theorem continuousOn_wickActionPath_Ioc_one :
 357    ContinuousOn (wickActionPath 1) (Set.Ioc 0 1) := by
 358  have hθ := continuousOn_carccos_comp_pent_Ioc_one
 359  have h3 : ContinuousOn (fun t => (3 : ℂ) * carccos (pentHingeCosPath 1 t))
 360      (Set.Ioc 0 1) :=
 361    continuousOn_const.mul hθ
 362  have hsub :
 363      ContinuousOn
 364        (fun t =>
 365          (2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath 1 t))
 366        (Set.Ioc 0 1) :=
 367    continuousOn_const.sub h3
 368  have hA :
 369      ContinuousOn
 370        (fun t =>
 371          (hingeArea : ℂ) *
 372            ((2 * Real.pi : ℂ) - 3 * carccos (pentHingeCosPath 1 t)))
 373        (Set.Ioc 0 1) :=
 374    continuousOn_const.mul hsub
 375  refine hA.congr ?_
 376  intro t _
 377  unfold wickActionPath dihedralSumPath
 378  rfl
 379
 380/-! ## §4. Assemble `WickActionContinuationCertV2 1` -/
 381
 382theorem chartsAgree_one :
 383    inducedSqEdges pentAVert 1 1 =
 384        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 1 ∧
 385      inducedSqEdges pentBVert 1 1 =
 386        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 1 ∧
 387      inducedSqEdges pentCVert 1 1 =
 388        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 1 :=
 389  ⟨induced_pentA_eq 1 1, induced_pentB_eq 1 1, induced_pentC_eq 1 1⟩
 390
 391theorem euclidAnchor_one :
 392    wickActionPath 1 1 =
 393      ((hingeArea * (2 * Real.pi - 3 * Real.arccos (euclidCos 1)) : ℝ) : ℂ) := by
 394  simpa [euclidAngle] using
 395    wickActionPath_eq_euclidRegge (by norm_num : (7 / 12 : ℝ) < 1)
 396
 397/-- Banked partial receipt: repaired V2 certificate at the physical coupling
 398α = 1. Does not inhabit `wick_action_continuation_4d`. -/
 399theorem wickActionContinuationCertV2_one :
 400    WickActionContinuationCertV2 1 where
 401  causalRange := by norm_num
 402  chartsAgree := chartsAgree_one
 403  branchRegularSum := branchRegularSum_one
 404  contActionInterior := continuousOn_wickActionPath_Ioc_one
 405  cutLimit := lorentzAnchor_one_holds
 406  euclidCosReal := by
 407    refine ⟨pentHingeCosPath_one_one, ?_⟩
 408    intro h; exact euclidCos_one
 409  euclidAnchor := euclidAnchor_one
 410  lorentzAnchor := lorentzAnchor_one_holds
 411  rapidityPinned := rapidityPinned_one
 412  -- Honesty: differentiability only; NOT classical Schläfli cancellation.
 413  euclidSchlaefli := euclidSchlaefli_field_inhabited_one
 414
 415theorem wick_action_continuation_v2_at_one_holds :
 416    wick_action_continuation_v2_at_one :=
 417  wickActionContinuationCertV2_one
 418
 419/-! ## §5. Codified decoys -/
 420
 421/-- Decoy: a Euclidean-only (real) certificate is falsified by the genuine
 422non-real Lorentzian endpoint. -/
 423theorem decoy_euclidean_only_falsified :
 424    (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe 1) : ℝ) : ℂ) -
 425        I * ((hingeArea * (3 * lorentzRapidity 1) : ℝ) : ℂ)).im ≠ 0 :=
 426  lorentz_endpoint_not_real
 427
 428/-- Decoy: an interior-point (`nhds`) limit cannot discharge `cutLimit`
 429(exact filter is `nhdsWithin 0 (Ioi 0)`). -/
 430theorem decoy_interior_nhds_not_cutLimit_filter :
 431    nhds (0 : ℝ) ≠ nhdsWithin (0 : ℝ) (Set.Ioi 0) := by
 432  intro h
 433  -- `Ioi 0` is a member of the cut filter, but not of plain `nhds 0`
 434  -- (every nhds-neighborhood of 0 contains 0 itself, which is outside `Ioi`).
 435  have hIoi : Set.Ioi (0 : ℝ) ∈ nhdsWithin (0 : ℝ) (Set.Ioi 0) :=
 436    self_mem_nhdsWithin
 437  have hIoi' : Set.Ioi (0 : ℝ) ∈ nhds (0 : ℝ) := by simpa [h] using hIoi
 438  exact absurd (mem_of_mem_nhds hIoi') (lt_irrefl (0 : ℝ))
 439
 440/-! ## §6. Status (partial receipt; gap6 unflipped) -/
 441
 442structure WickActionCertAssemblyStatus where
 443  gap6LorentzianAction : Bool
 444  contActionV1Unsatisfiable : Bool
 445  certV2AtOneClosed : Bool
 446  familyV2Open : Bool
 447  terminalV1Open : Bool
 448
 449def wickActionCertAssemblyStatus : WickActionCertAssemblyStatus where
 450  gap6LorentzianAction := true
 451  contActionV1Unsatisfiable := true
 452  certV2AtOneClosed := true
 453  familyV2Open := false
 454  terminalV1Open := false
 455
 456theorem wickActionCertAssemblyStatus_flags :
 457    wickActionCertAssemblyStatus.gap6LorentzianAction = true ∧
 458      wickActionCertAssemblyStatus.contActionV1Unsatisfiable = true ∧
 459        wickActionCertAssemblyStatus.certV2AtOneClosed = true ∧
 460          wickActionCertAssemblyStatus.familyV2Open = false ∧
 461            wickActionCertAssemblyStatus.terminalV1Open = false ∧
 462              (¬ ContinuousOn (wickActionPath 1) (Set.Icc 0 1)) ∧
 463                wick_action_continuation_v2_at_one :=
 464  ⟨rfl, rfl, rfl, rfl, rfl, contAction_not_satisfiable_at_one,
 465    wick_action_continuation_v2_at_one_holds⟩
 466
 467end
 468
 469end WickActionInteriorHinge
 470end SevenGaps
 471end Gravity
 472end IndisputableMonolith
 473