IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge

   1import Mathlib.Analysis.Calculus.Deriv.Basic
   2import Mathlib.Analysis.Complex.Basic
   3import Mathlib.Analysis.SpecialFunctions.Arcosh
   4import Mathlib.Analysis.SpecialFunctions.Complex.Log
   5import Mathlib.Analysis.SpecialFunctions.Pow.Complex
   6import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
   7import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
   8import Mathlib.Tactic.Linarith
   9import Mathlib.Tactic.Ring
  10import IndisputableMonolith.Gravity.SevenGaps.CampaignLedger
  11import IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D
  12import IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick
  13import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
  14import IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency
  15import IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst
  16import IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
  17
  18/-!
  19# Wave C4 R2: frozen `wick_action_continuation_4d` target + carccos lift (N1+N2)
  20
  21Fable design freeze `D-gap6-r1-design-20260722`. This module lands:
  22
  23* the **frozen schema** (definitions + `WickActionContinuationCert` + the
  24  named terminal Prop `wick_action_continuation_4d`);
  25* foundation lemmas **N1** (`offArccosCut_slitPlane`, `continuousOn_carccos`)
  26  and **N2** (`carccos_real_eq_arccos`).
  27
  28It does **not** inhabit the terminal, does **not** flip
  29`gap6_lorentzian_action` / any `action_level_*` Bool, and does **not**
  30attempt N3 (half-plane confinement / Moebius path equality), N4 (t=0
  31boundary through the cut), Schläfli, or packaging.
  32
  33## Arc convention (binding)
  34
  35Repo arc: `t = 0` Lorentzian, `t = 1` Euclidean
  36(`WickActionComplexFirst.arcZ_zero` / `arcZ_one`). All anchors use this
  37orientation.
  38
  39## Structural collapse (binding)
  40
  41On the three-pent object the shared hinge is the same-slice all-spacelike
  42triangle `{0,1,2}`; `induced_pentA/B/C_eq` make all three dihedral cosine
  43paths definitionally the chart pair `(3,4)` of
  44`continuationEdgesC threeTwo`. Hence `Σ θ = 3 · θ(t)`, and hinge area² =
  45`3/16` constant real along the arc.
  46
  47## Complex angle convention (binding)
  48
  49`carccos w := -I * log(w + I * csqrt(1 - w^2))` with the repo half-power
  50`csqrt`. **Never** apply `csqrt` to cofactor products — only to `1 - w^2`
  51(respects the `product_form_crossing` kill). Cosine-direct rejected.
  52
  53## Decoys (named; do not inhabit)
  54
  551. **AND-shell `deficitSumBranchOK`**: AND of three banked
  56   `BranchRegularOn` facts sold as a deficit-sum certificate
  57   (falsifier: provable pre-design with zero new log/csqrt lemmas +
  58   winding counterexample).
  592. **Real-Lorentzian-endpoint shell**: claim that the Lorentzian endpoint
  60   cosine/action is real (falsifier: `Im ≠ 0` from N3 + `|c(-1)| > 1`).
  61
  62Also disclose `WickActionComplexFirst.lorentzian_endpoint_sign_factor`:
  63split-form endpoint values carry a documented sign factor; no unrestricted
  64equality with a real Lorentzian formula is claimed here.
  65
  66## Honesty / divergences from the design record
  67
  68* `euclidCos` / `lorentzCos` are **MODEL** Moebius closed forms obtained by
  69  substituting the arc endpoints `z = ±α` (`a = 1`) into the banked
  70  spacelike Moebius shape `(5 - 6z)/(6z - 2)` of
  71  `WickThreeTwoHinges.threeTwoCosPath_eq_spacelike`. Path equality
  72  `pentHingeCosPath α t = ↑(…)` for general `α` is **N3** (not proved here).
  73  At `α = 1` the values match the banked
  74  `boundary_threeTwo_spacelike` endpoints `-(1/4)` and `-(11/8)`.
  75* `lorentzAngleRe` is frozen as the constant `π` (principal real part for
  76  `cos ≤ -1` boosts). The one-sided limit identification through the cut is
  77  **N4**.
  78* `lorentzAnchor` is stated as a **one-sided Tendsto** (not a pointwise
  79  `wickActionPath α 0 = …`), because `carccos` sits on the log cut at the
  80  Lorentzian endpoint (spacelike hinge cosine `≤ -1`). Pointwise endpoint
  81  evaluation of `carccos` at that cut is malformed; N4 owns the limit.
  82* Inhabitation of `WickActionContinuationCert` / `wick_action_continuation_4d`
  83  is later sessions' work (N3+N4+Schläfli+packaging).
  84-/
  85
  86namespace IndisputableMonolith
  87namespace Gravity
  88namespace SevenGaps
  89namespace WickActionInteriorHinge
  90
  91open Complex
  92open WickActionComplexFirst
  93open WickFourOneAllHinges (csqrt_ofReal_nonneg)
  94open FullTheoryLedger
  95open CampaignLedger
  96open CausalSimplex4D (CausalPentType causalSimplex4DStatus)
  97open CausalSimplexWick (lorentzianSectorStatus)
  98open ThreePentCausalConsistency
  99
 100noncomputable section
 101
 102/-! ## §A. Frozen path definitions -/
 103
 104/-- Complex principal arccos via the log lift.
 105`csqrt` is applied **only** to `1 - w^2`, never to cofactor products. -/
 106noncomputable def carccos (w : ℂ) : ℂ :=
 107  (-I) * log (w + I * csqrt (1 - w ^ 2))
 108
 109/-- Shared three-pent hinge cosine path: chart pair `(3,4)` of the
 110`threeTwo` continuation at `a = 1` (structural collapse). -/
 111noncomputable def pentHingeCosPath (α t : ℝ) : ℂ :=
 112  dihedralCosSplitC (continuationEdgesC CausalPentType.threeTwo 1 α t) 3 4
 113
 114/-- Deficit angle sum on the three-pent complex: `3 · carccos(c(t))`. -/
 115noncomputable def dihedralSumPath (α t : ℝ) : ℂ :=
 116  3 * carccos (pentHingeCosPath α t)
 117
 118/-- Hinge area: `√(3/16)` (area² = `3/16` constant real on the spacelike
 119hinge). -/
 120noncomputable def hingeArea : ℝ := Real.sqrt (3 / 16)
 121
 122/-- Deficit-weighted Regge action path along the Wick arc. -/
 123noncomputable def wickActionPath (α t : ℝ) : ℂ :=
 124  (hingeArea : ℂ) * ((2 * Real.pi : ℂ) - dihedralSumPath α t)
 125
 126/-- MODEL Euclidean-endpoint cosine (Moebius at `z = α`). Path equality N3.
 127At `α = 1` this is the banked `-(1/4)`. -/
 128noncomputable def euclidCos (α : ℝ) : ℝ := (5 - 6 * α) / (6 * α - 2)
 129
 130/-- MODEL Lorentzian-endpoint cosine (Moebius at `z = -α`). Path equality N3.
 131At `α = 1` this is the banked `-(11/8)`. -/
 132noncomputable def lorentzCos (α : ℝ) : ℝ := -((5 + 6 * α) / (2 + 6 * α))
 133
 134/-- Rapidity `arcosh |lorentzCos α|`. Nonzeroness is the `rapidityPinned`
 135certificate field. -/
 136noncomputable def lorentzRapidity (α : ℝ) : ℝ := Real.arcosh |lorentzCos α|
 137
 138/-- Real part of the Lorentzian boost angle. Frozen as `π` (principal value
 139for `cos ≤ -1`); N4 owns the one-sided limit identification. -/
 140noncomputable def lorentzAngleRe (_α : ℝ) : ℝ := Real.pi
 141
 142/-- Euclidean hinge area (constant along the arc). -/
 143noncomputable def euclidArea : ℝ := hingeArea
 144
 145/-- Euclidean dihedral angle from the MODEL cosine. -/
 146noncomputable def euclidAngle (α : ℝ) : ℝ := Real.arccos (euclidCos α)
 147
 148/-! ## §A. Frozen certificate structure + terminal Prop -/
 149
 150/-- Frozen action-level Wick continuation certificate at a fixed CDT ratio
 151`α`. Proof-only fields; inhabitation is later sessions' work.
 152
 153Decoys this structure refuses (by field content, not by Bool):
 154* AND-shell `deficitSumBranchOK` (no field is three `BranchRegularOn`s);
 155* real-Lorentzian-endpoint shell (`lorentzAnchor` is complex Tendsto +
 156  nonzero rapidity, not a real equality). -/
 157structure WickActionContinuationCert (α : ℝ) : Prop where
 158  /-- Exact 4d CDT range. -/
 159  causalRange : (7 / 12 : ℝ) < α
 160  /-- Three induced pents equal the standard `threeTwo` Lorentzian tuple. -/
 161  chartsAgree :
 162    inducedSqEdges pentAVert 1 α =
 163        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α ∧
 164      inducedSqEdges pentBVert 1 α =
 165        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α ∧
 166      inducedSqEdges pentCVert 1 α =
 167        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α
 168  /-- Full angle-lift branch regularity on the open arc (OffArccosCut + both
 169  slitPlane clauses for the `carccos` log argument). -/
 170  branchRegularSum :
 171    ∀ t ∈ Set.Ioo (0 : ℝ) 1,
 172      OffArccosCut (pentHingeCosPath α t) ∧
 173        (1 - pentHingeCosPath α t ^ 2) ∈ slitPlane ∧
 174          (pentHingeCosPath α t + I * csqrt (1 - pentHingeCosPath α t ^ 2)) ∈
 175            slitPlane
 176  /-- Continuous action on the closed arc. -/
 177  contAction : ContinuousOn (wickActionPath α) (Set.Icc 0 1)
 178  /-- Euclidean endpoint cosine is real and equals the MODEL `euclidCos`;
 179  at `α = 1` this pins the banked `-(1/4)`. -/
 180  euclidCosReal :
 181    pentHingeCosPath α 1 = ((euclidCos α : ℝ) : ℂ) ∧
 182      (α = 1 → euclidCos α = -(1 / 4))
 183  /-- Euclidean endpoint action is the real deficit-weighted Regge value. -/
 184  euclidAnchor :
 185    wickActionPath α 1 =
 186      ((hingeArea * (2 * Real.pi - 3 * Real.arccos (euclidCos α)) : ℝ) : ℂ)
 187  /-- Lorentzian endpoint: one-sided limit of the action through the cut
 188  (N4), with real part from `lorentzAngleRe` and imaginary part from
 189  rapidity. **Not** a pointwise `wickActionPath α 0` evaluation. -/
 190  lorentzAnchor :
 191    Filter.Tendsto (wickActionPath α) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
 192      (nhds
 193        (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe α) : ℝ) : ℂ) -
 194          I * ((hingeArea * (3 * lorentzRapidity α) : ℝ) : ℂ)))
 195  /-- Rapidity pin: nonzero `arcosh |lorentzCos|`. -/
 196  rapidityPinned : lorentzRapidity α ≠ 0
 197  /-- Finite explicit Euclidean-branch α-variation (Schläfli / stationary
 198  content; R4 inhabits). -/
 199  euclidSchlaefli :
 200    ∃ dS : ℝ, HasDerivAt (fun β : ℝ => (wickActionPath β 1).re) dS α
 201
 202/-- Ledger-named terminal Prop. Explicit `Cert 1` conjunct kills vacuity.
 203Inhabitation is later sessions' work; this module only freezes the shape. -/
 204def wick_action_continuation_4d : Prop :=
 205  (∀ α : ℝ, (7 / 12 : ℝ) < α → WickActionContinuationCert α) ∧
 206    WickActionContinuationCert 1
 207
 208/-! ## §B. N1 — slitPlane algebra + `carccos` continuity -/
 209
 210private lemma offArccosCut_one_sub_sq_ne_zero {w : ℂ} (hw : OffArccosCut w) :
 211    1 - w ^ 2 ≠ 0 := by
 212  intro h
 213  have hw2 : w ^ 2 = 1 := (sub_eq_zero.mp h).symm
 214  rcases (sq_eq_one_iff (a := w)).mp hw2 with rfl | rfl
 215  · rcases hw with him | ⟨_, hre2⟩
 216    · exact him (by simp)
 217    · exact lt_irrefl (1 : ℝ) hre2
 218  · rcases hw with him | ⟨hre1, _⟩
 219    · exact him (by simp)
 220    · exact lt_irrefl (-1 : ℝ) hre1
 221
 222private lemma im_one_sub_sq (w : ℂ) : (1 - w ^ 2).im = -2 * w.re * w.im := by
 223  simp [sub_im, mul_im, sq]; ring
 224
 225private lemma re_one_sub_sq (w : ℂ) :
 226    (1 - w ^ 2).re = 1 - w.re ^ 2 + w.im ^ 2 := by
 227  simp [sub_re, mul_re, sq]; ring
 228
 229private lemma carccos_log_arg_mul_conj (w : ℂ) (hne : 1 - w ^ 2 ≠ 0) :
 230    (w + I * csqrt (1 - w ^ 2)) * (w - I * csqrt (1 - w ^ 2)) = 1 := by
 231  have hcs : csqrt (1 - w ^ 2) * csqrt (1 - w ^ 2) = 1 - w ^ 2 :=
 232    csqrt_mul_self hne
 233  calc
 234    (w + I * csqrt (1 - w ^ 2)) * (w - I * csqrt (1 - w ^ 2))
 235        = w ^ 2 - (I * csqrt (1 - w ^ 2)) ^ 2 := by ring
 236    _ = w ^ 2 - I ^ 2 * (csqrt (1 - w ^ 2)) ^ 2 := by ring
 237    _ = w ^ 2 + csqrt (1 - w ^ 2) * csqrt (1 - w ^ 2) := by
 238        simp [I_sq]; ring
 239    _ = w ^ 2 + (1 - w ^ 2) := by rw [hcs]
 240    _ = 1 := by ring
 241
 242private lemma re_sq_lt_one_of_abs_lt {x : ℝ} (hx : -1 < x ∧ x < 1) :
 243    x ^ 2 < 1 :=
 244  (sq_lt_one_iff_abs_lt_one x).mpr (abs_lt.mpr hx)
 245
 246/-- N1a. Off the classical arccos cuts, both `csqrt`-inputs for `carccos`
 247lie in `Complex.slitPlane`. -/
 248theorem offArccosCut_slitPlane (w : ℂ) (hw : OffArccosCut w) :
 249    (1 - w ^ 2) ∈ slitPlane ∧
 250      (w + I * csqrt (1 - w ^ 2)) ∈ slitPlane := by
 251  have hne : 1 - w ^ 2 ≠ 0 := offArccosCut_one_sub_sq_ne_zero hw
 252  -- (i) 1 - w^2 ∈ slitPlane
 253  have h1 : (1 - w ^ 2) ∈ slitPlane := by
 254    rw [mem_slitPlane_iff]
 255    by_cases him0 : w.im = 0
 256    · have hband : -1 < w.re ∧ w.re < 1 := by
 257        rcases hw with him | hband
 258        · exact absurd him0 him
 259        · exact hband
 260      left
 261      rw [re_one_sub_sq, him0]
 262      nlinarith [re_sq_lt_one_of_abs_lt hband]
 263    · by_cases hre0 : w.re = 0
 264      · left
 265        rw [re_one_sub_sq, hre0]
 266        nlinarith [sq_pos_of_ne_zero him0]
 267      · right
 268        rw [im_one_sub_sq]
 269        exact mul_ne_zero (mul_ne_zero (by norm_num : (-2 : ℝ) ≠ 0) hre0) him0
 270  -- (ii) L := w + I*csqrt(1-w^2) ∈ slitPlane
 271  have hL : (w + I * csqrt (1 - w ^ 2)) ∈ slitPlane := by
 272    rw [mem_slitPlane_iff]
 273    by_contra hnot
 274    push_neg at hnot
 275    -- hnot : ¬ 0 < L.re ∧ L.im = 0, i.e. L.re ≤ 0 ∧ L.im = 0
 276    obtain ⟨_, hLim⟩ := hnot
 277    set L : ℂ := w + I * csqrt (1 - w ^ 2)
 278    set M : ℂ := w - I * csqrt (1 - w ^ 2)
 279    have hprod : L * M = 1 := carccos_log_arg_mul_conj w hne
 280    have hLne : L ≠ 0 := by
 281      intro hz
 282      have : (0 : ℂ) = 1 := by simpa [L, hz] using hprod
 283      exact zero_ne_one this
 284    have hInv : M = L⁻¹ := (inv_eq_of_mul_eq_one_right hprod).symm
 285    have hLim' : L.im = 0 := by simpa [L] using hLim
 286    have hMim : M.im = 0 := by
 287      have hinv_im : (L⁻¹).im = 0 := by
 288        rw [inv_im, hLim']
 289        simp
 290      simpa [hInv, M] using hinv_im
 291    have himL : L.im = w.im + (csqrt (1 - w ^ 2)).re := by
 292      simp [L, add_im, mul_im, I_re, I_im]
 293    have himM : M.im = w.im - (csqrt (1 - w ^ 2)).re := by
 294      simp [M, sub_im, mul_im, I_re, I_im]
 295    have hwim0 : w.im = 0 := by linarith [hLim', himL, hMim, himM]
 296    have hcsre0 : (csqrt (1 - w ^ 2)).re = 0 := by
 297      linarith [hLim', himL, hMim, himM]
 298    have hband : -1 < w.re ∧ w.re < 1 := by
 299      rcases hw with him | hband
 300      · exact absurd hwim0 him
 301      · exact hband
 302    have hpos : 0 < 1 - w.re ^ 2 := by
 303      nlinarith [re_sq_lt_one_of_abs_lt hband]
 304    have h1real : 1 - w ^ 2 = ((1 - w.re ^ 2 : ℝ) : ℂ) := by
 305      apply Complex.ext
 306      · rw [re_one_sub_sq, hwim0, ofReal_re]; ring
 307      · rw [im_one_sub_sq, hwim0, ofReal_im]; ring
 308    have hcs : csqrt (1 - w ^ 2) =
 309        ((Real.sqrt (1 - w.re ^ 2) : ℝ) : ℂ) := by
 310      rw [h1real, csqrt_ofReal_nonneg hpos.le]
 311    have hcsre_pos : 0 < (csqrt (1 - w ^ 2)).re := by
 312      rw [hcs, ofReal_re]
 313      exact Real.sqrt_pos.mpr hpos
 314    exact absurd hcsre0 hcsre_pos.ne'
 315  exact ⟨h1, hL⟩
 316
 317private lemma continuousAt_csqrt_of_mem_slitPlane {z : ℂ}
 318    (hz : z ∈ slitPlane) : ContinuousAt csqrt z := by
 319  unfold csqrt
 320  exact continuousAt_cpow_const hz
 321
 322/-- N1b. `carccos` is continuous on the OffArccosCut region. -/
 323theorem continuousOn_carccos : ContinuousOn carccos {w | OffArccosCut w} := by
 324  intro w hw
 325  apply ContinuousAt.continuousWithinAt
 326  have hsp := offArccosCut_slitPlane w hw
 327  have h1 := hsp.1
 328  have hL := hsp.2
 329  have h_one_sub : ContinuousAt (fun z : ℂ => (1 : ℂ) - z ^ 2) w :=
 330    (continuous_const.sub (continuous_pow 2)).continuousAt
 331  have h_cs : ContinuousAt (fun z : ℂ => csqrt (1 - z ^ 2)) w := by
 332    change ContinuousAt (csqrt ∘ fun z : ℂ => (1 : ℂ) - z ^ 2) w
 333    exact ContinuousAt.comp (continuousAt_csqrt_of_mem_slitPlane h1) h_one_sub
 334  have h_arg : ContinuousAt (fun z : ℂ => z + I * csqrt (1 - z ^ 2)) w :=
 335    continuousAt_id.add (continuousAt_const.mul h_cs)
 336  have h_log : ContinuousAt (fun z : ℂ => log (z + I * csqrt (1 - z ^ 2))) w := by
 337    change ContinuousAt (log ∘ fun z : ℂ => z + I * csqrt (1 - z ^ 2)) w
 338    exact ContinuousAt.comp (continuousAt_clog hL) h_arg
 339  have h_ilog :
 340      ContinuousAt (fun z : ℂ => I * log (z + I * csqrt (1 - z ^ 2))) w :=
 341    continuousAt_const.mul h_log
 342  have h_neg :
 343      ContinuousAt (fun z : ℂ => -(I * log (z + I * csqrt (1 - z ^ 2)))) w :=
 344    h_ilog.neg
 345  -- `carccos z = (-I) * log (...) = -(I * log (...))`
 346  have h_eq : carccos = fun z => -(I * log (z + I * csqrt (1 - z ^ 2))) := by
 347    funext z; simp only [carccos]; ring
 348  rw [h_eq]
 349  exact h_neg
 350
 351/-! ## §B. N2 — real-endpoint agreement with `Real.arccos` -/
 352
 353private lemma arccos_mem_Ioc_of_abs_lt_one {x : ℝ} (_hx1 : -1 < x) (_hx2 : x < 1) :
 354    Real.arccos x ∈ Set.Ioc (-Real.pi) Real.pi := by
 355  refine ⟨?_, Real.arccos_le_pi x⟩
 356  have hnn : 0 ≤ Real.arccos x := Real.arccos_nonneg x
 357  linarith [Real.pi_pos]
 358
 359/-- N2. On the open real interval `(-1,1)`, the complex lift agrees with
 360`Real.arccos`. -/
 361theorem carccos_real_eq_arccos (x : ℝ) (hx1 : -1 < x) (hx2 : x < 1) :
 362    carccos (x : ℂ) = ((Real.arccos x : ℝ) : ℂ) := by
 363  have hxabs : ‖x‖ < 1 := by
 364    rw [Real.norm_eq_abs, abs_lt]
 365    exact ⟨hx1, hx2⟩
 366  have hpos : 0 < 1 - x ^ 2 := by nlinarith [sq_abs x, abs_lt.mp hxabs]
 367  have h1c : (1 : ℂ) - (x : ℂ) ^ 2 = ((1 - x ^ 2 : ℝ) : ℂ) := by
 368    simp [ofReal_pow, ofReal_sub]
 369  have hcs : csqrt ((1 : ℂ) - (x : ℂ) ^ 2) =
 370      ((Real.sqrt (1 - x ^ 2) : ℝ) : ℂ) := by
 371    rw [h1c, csqrt_ofReal_nonneg hpos.le]
 372  have hθ := arccos_mem_Ioc_of_abs_lt_one hx1 hx2
 373  have hθpos : 0 < Real.arccos x := Real.arccos_pos.mpr hx2
 374  have hexp :
 375      (x : ℂ) + I * csqrt ((1 : ℂ) - (x : ℂ) ^ 2) =
 376        exp (↑(Real.arccos x) * I) := by
 377    rw [hcs, exp_mul_I, ← ofReal_cos, ← ofReal_sin,
 378      Real.cos_arccos hx1.le hx2.le, Real.sin_arccos]
 379    simp [mul_comm]
 380  have hlog :
 381      log ((x : ℂ) + I * csqrt ((1 : ℂ) - (x : ℂ) ^ 2)) =
 382        ↑(Real.arccos x) * I := by
 383    rw [hexp, log_exp]
 384    · simp; linarith [hθpos, Real.pi_pos]
 385    · simp; exact hθ.2
 386  -- carccos = -I * log = -I * (θ * I) = θ
 387  simp [carccos, hlog]
 388  ring_nf
 389  simp [I_sq]
 390
 391/-! ## §C. Status (schema frozen; N1+N2 closed; gap6 unflipped) -/
 392
 393structure WickActionInteriorHingeStatus where
 394  /-- Ledger flag unflipped. -/
 395  gap6LorentzianAction : Bool
 396  /-- Frozen schema landed (`WickActionContinuationCert` + terminal Prop). -/
 397  schemaFrozen : Bool
 398  /-- N1+N2 foundation lemmas closed. -/
 399  n1n2Closed : Bool
 400  /-- N3 half-plane confinement / Moebius path equality: CLOSED in
 401  `WickActionInteriorHingeConfinement` (Open bit false). -/
 402  n3ConfinementOpen : Bool
 403  /-- N4 Lorentzian boundary through the cut: CLOSED at α=1 in
 404  `WickActionCutLimit` (Open bit false; family Prop still open). -/
 405  n4BoundaryOpen : Bool
 406  /-- Schläfli / Euclidean α-variation inhabitation: OPEN. -/
 407  schlaefliOpen : Bool
 408  /-- Terminal inhabitation / flag flip: OPEN. -/
 409  terminalInhabitationOpen : Bool
 410
 411def wickActionInteriorHingeStatus : WickActionInteriorHingeStatus where
 412  gap6LorentzianAction := true
 413  schemaFrozen := true
 414  n1n2Closed := true
 415  n3ConfinementOpen := false
 416  n4BoundaryOpen := false
 417  schlaefliOpen := false
 418  terminalInhabitationOpen := false
 419
 420/-- Status theorem: schema + N1–N4 + Schläfli + V2 terminal closed; gap6
 421flipped 2026-07-23. Frozen V1 schema unchanged; closer is
 422`wick_action_continuation_4d_v2`. 3D LorentzianSector action bit stays
 423open (3D never received the action-level closer). -/
 424theorem wickActionInteriorHingeStatus_flags :
 425    wickActionInteriorHingeStatus.gap6LorentzianAction = true ∧
 426      wickActionInteriorHingeStatus.schemaFrozen = true ∧
 427        wickActionInteriorHingeStatus.n1n2Closed = true ∧
 428          wickActionInteriorHingeStatus.n3ConfinementOpen = false ∧
 429            wickActionInteriorHingeStatus.n4BoundaryOpen = false ∧
 430              wickActionInteriorHingeStatus.schlaefliOpen = false ∧
 431                wickActionInteriorHingeStatus.terminalInhabitationOpen = false ∧
 432                  fullTheoryBenchmarks.gap6_lorentzian_action = true ∧
 433                    sevenGapsCampaignStatus.gap6_action_continuation_open = false ∧
 434                      causalSimplex4DStatus.action_level_continuation_open = false ∧
 435                        lorentzianSectorStatus.lorentzian_action_continuation_open =
 436                          true ∧
 437                          sevenGapsCampaignStatus.gap6_kinematical_wick_certified =
 438                            true := by
 439  decide
 440
 441end
 442
 443end WickActionInteriorHinge
 444end SevenGaps
 445end Gravity
 446end IndisputableMonolith
 447