IndisputableMonolith.Gravity.SevenGaps.WickActionCertFamilyAssembly

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly
   2import IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamily
   3
   4/-!
   5# Wave C4 F2: family `WickActionContinuationCertV2` assembly
   6
   7Binding design: `D-gap6-v2-succession-family-design-20260723`.
   8
   9Assembles every banked family ingredient into
  10`wickActionContinuationCertV2_of_causal` under `7/12 < α`, then lands the
  11succession terminal
  12
  13`wick_action_continuation_4d_v2 :=
  14  (∀ α, 7/12 < α → CertV2 α) ∧ CertV2 1`
  15
  16and retires the frozen V1 terminal via `not_wick_action_continuation_4d`
  17(from `contAction_not_satisfiable_at_one`).
  18
  19## Honesty (disclosed)
  20
  21* **V1 retirement.** The frozen closed-interval `contAction` field is
  22  unsatisfiable at the cut (`contAction_not_satisfiable_at_one`); hence
  23  `¬ wick_action_continuation_4d`. Succession is choice (a): the v2
  24  terminal replaces V1 as the ledger target.
  25* **`euclidSchlaefli`.** Differentiability of the Euclidean-endpoint
  26  action on the collapsed one-hinge geometry, **not** classical
  27  multi-hinge Schläfli cancellation `Σ A θ' = 0`.
  28* **One-hinge MODEL scoping.** Charts collapse to a single angle path
  29  (`induced_pent*_eq`); the certificate is the three-pent one-hinge
  30  model, not a full multi-hinge complex.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Gravity
  35namespace SevenGaps
  36namespace WickActionInteriorHinge
  37
  38open Complex
  39open Filter Topology
  40open CausalSimplex4D
  41open ThreePentCausalConsistency
  42
  43noncomputable section
  44
  45/-! ## §F2. Family certificate assembly -/
  46
  47theorem chartsAgree_of_causal (α : ℝ) :
  48    inducedSqEdges pentAVert 1 α =
  49        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α ∧
  50      inducedSqEdges pentBVert 1 α =
  51        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α ∧
  52      inducedSqEdges pentCVert 1 α =
  53        CausalSimplex4D.lorentzianSqEdges CausalPentType.threeTwo 1 α :=
  54  ⟨induced_pentA_eq 1 α, induced_pentB_eq 1 α, induced_pentC_eq 1 α⟩
  55
  56theorem euclidCosReal_of_causal {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
  57    pentHingeCosPath α 1 = ((euclidCos α : ℝ) : ℂ) ∧
  58      (α = 1 → euclidCos α = -(1 / 4)) :=
  59  ⟨pentHingeCosPath_eq_euclidCos hα, fun h => by
  60    subst h
  61    exact euclidCos_one⟩
  62
  63theorem euclidAnchor_of_causal {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
  64    wickActionPath α 1 =
  65      ((hingeArea * (2 * Real.pi - 3 * Real.arccos (euclidCos α)) : ℝ) : ℂ) := by
  66  simpa [euclidAngle] using wickActionPath_eq_euclidRegge hα
  67
  68/-- Family-wide repaired V2 certificate on the causal range `7/12 < α`. -/
  69theorem wickActionContinuationCertV2_of_causal {α : ℝ}
  70    (hα : (7 / 12 : ℝ) < α) : WickActionContinuationCertV2 α where
  71  causalRange := hα
  72  chartsAgree := chartsAgree_of_causal α
  73  branchRegularSum := branchRegularSum_of_causal hα
  74  contActionInterior := continuousOn_wickActionPath_Ioc_of_causal hα
  75  cutLimit := lorentzAnchor_of_causal hα
  76  euclidCosReal := euclidCosReal_of_causal hα
  77  euclidAnchor := euclidAnchor_of_causal hα
  78  lorentzAnchor := lorentzAnchor_of_causal hα
  79  rapidityPinned := rapidityPinned_of_causal hα
  80  euclidSchlaefli := euclidSchlaefli_field_inhabited hα
  81
  82/-! ## §F3a. Succession terminal (V2) + V1 retirement -/
  83
  84/-- Ledger-named V2 terminal. Family conjunct plus the physical coupling
  85`α = 1`. Succeeds the frozen V1 terminal `wick_action_continuation_4d`,
  86which is provably unsatisfiable (`not_wick_action_continuation_4d`).
  87
  88Honesty: `euclidSchlaefli` is differentiability-only on the one-hinge
  89MODEL; classical multi-hinge Schläfli cancellation is not claimed. -/
  90def wick_action_continuation_4d_v2 : Prop :=
  91  (∀ α : ℝ, (7 / 12 : ℝ) < α → WickActionContinuationCertV2 α) ∧
  92    WickActionContinuationCertV2 1
  93
  94theorem wick_action_continuation_4d_v2_holds :
  95    wick_action_continuation_4d_v2 :=
  96  ⟨fun _α hα => wickActionContinuationCertV2_of_causal hα,
  97    wickActionContinuationCertV2_one⟩
  98
  99/-- V1 terminal retirement: frozen `contAction` is unsatisfiable at α = 1. -/
 100theorem not_wick_action_continuation_4d : ¬ wick_action_continuation_4d := by
 101  intro h
 102  exact contAction_not_satisfiable_at_one h.2.contAction
 103
 104/-- Family Prop alias inhabited by the V2 terminal's first conjunct. -/
 105theorem wick_action_continuation_v2_family_holds :
 106    wick_action_continuation_v2_family :=
 107  fun _α hα => wickActionContinuationCertV2_of_causal hα
 108
 109end
 110
 111end WickActionInteriorHinge
 112end SevenGaps
 113end Gravity
 114end IndisputableMonolith
 115