IndisputableMonolith.Gravity.SevenGaps.MetricRefinementCarrierBlocker

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker
   3import IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick
   4import IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D
   5
   6/-!
   7# Seven Gaps, P2.5: metric-refinement carrier blocker
   8
   9`PathSumMeasure.BoundedComplex B` contains only cardinalities and incidence
  10maps. Its quotient `TriangulationClass B` therefore identifies combinatorial
  11types, not metric geometries. This file gives a concrete kernel certificate
  12of the resulting P2.5 obstruction.
  13
  14The existing nonempty simplicial witness `oneTetComplex` admits two positive,
  15nondegenerate metric decorations at the same cap and in the same quotient
  16class. Their edge lengths differ, and their Cayley-Menger observable differs.
  17Consequently no function on `TriangulationClass 6` alone can recover either
  18observable for both decorations. The forgetful map from metric-decorated
  19simplicial complexes to the current quotient is explicitly non-injective.
  20
  21The final section supplies the missing carrier shape
  22`MetricRefinementFamily`. It has finite metric-decorated configuration spaces,
  23a genuine mesh tending to zero, coarse projections, and summable local
  24action-step control. It does not assume convergence of the path sum. With a
  25measure supplied separately, it is just enough to define the geometric
  26finite-level path sum and state its continuum-limit proposition.
  27
  28Honesty boundary:
  29* THEOREM: all obstruction and witness results below.
  30* MODEL/API: `MetricDecoration`, `MetricDecoratedComplex`, and
  31  `MetricRefinementFamily` are the minimal proposed carrier interface.
  32* OPEN: construction of such a family from the recognition substrate,
  33  derivation of its measure and action, and the geometric continuum theorem.
  34
  35No full-theory flag is changed. Complexity-cutoff convergence remains
  36different from metric mesh refinement.
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Gravity
  41namespace SevenGaps
  42namespace MetricRefinementCarrierBlocker
  43
  44open PathSumMeasure
  45open ExactShellGaugeUV
  46open ZqContinuumBlocker
  47open Geometry.CayleyMengerPolynomial
  48
  49noncomputable section
  50
  51/-! ## 1. Metric data missing from `BoundedComplex` -/
  52
  53/-- Positive squared-edge data decorating one combinatorial carrier. The
  54carrier itself remains exactly the existing `BoundedComplex`. -/
  55structure MetricDecoration {B : ℕ} (K : BoundedComplex B) where
  56  sqEdge : Fin K.nE → ℝ
  57  sqEdge_pos : ∀ e, 0 < sqEdge e
  58
  59/-- A simplicial carrier together with metric data. This is the smallest
  60configuration object on which mesh-sensitive observables can be evaluated. -/
  61structure MetricDecoratedComplex (B : ℕ) where
  62  carrier : BoundedComplex B
  63  simplicial : IsSimplicial carrier
  64  metric : MetricDecoration carrier
  65
  66/-- Forgetting the metric returns exactly the current combinatorial quotient
  67class. -/
  68def MetricDecoratedComplex.toClass {B : ℕ} (G : MetricDecoratedComplex B) :
  69    TriangulationClass B :=
  70  Quotient.mk (relabelSetoid B) G.carrier
  71
  72/-! ## 2. Two metrics on the same admissible combinatorial class -/
  73
  74/-- Unit squared-edge metric on the existing one-tetrahedron simplicial
  75carrier. -/
  76def unitDecoration : MetricDecoration oneTetComplex where
  77  sqEdge := fun _ => 1
  78  sqEdge_pos := fun _ => one_pos
  79
  80/-- Squared-edge metric of a regular tetrahedron with edge length two, on the
  81same one-tetrahedron simplicial carrier. -/
  82def doubleDecoration : MetricDecoration oneTetComplex where
  83  sqEdge := fun _ => 4
  84  sqEdge_pos := fun _ => by norm_num
  85
  86/-- The length of the first edge. This is a genuine metric observable because
  87it reads the square root of the stored squared-edge datum. -/
  88def firstEdgeLength (D : MetricDecoration oneTetComplex) : ℝ :=
  89  Real.sqrt (D.sqEdge (show Fin oneTetComplex.nE from (0 : Fin 6)))
  90
  91/-- The Cayley-Menger observable of the decorated tetrahedron. It is
  92`288 * volume^2` on realizable tetrahedra and enters the Regge metric API. -/
  93def cayleyMengerObservable (D : MetricDecoration oneTetComplex) : ℝ :=
  94  cm3 D.sqEdge
  95
  96theorem unitDecoration_firstEdgeLength :
  97    firstEdgeLength unitDecoration = 1 := by
  98  norm_num [firstEdgeLength, unitDecoration]
  99
 100theorem doubleDecoration_firstEdgeLength :
 101    firstEdgeLength doubleDecoration = 2 := by
 102  norm_num [firstEdgeLength, doubleDecoration]
 103
 104theorem unitDecoration_cayleyMenger :
 105    cayleyMengerObservable unitDecoration = 4 := by
 106  norm_num [cayleyMengerObservable, unitDecoration, cm3]
 107
 108theorem doubleDecoration_cayleyMenger :
 109    cayleyMengerObservable doubleDecoration = 256 := by
 110  norm_num [cayleyMengerObservable, doubleDecoration, cm3]
 111
 112/-- The two metric decorations are distinct, witnessed by their first edge
 113lengths. -/
 114theorem unitDecoration_ne_doubleDecoration :
 115    unitDecoration ≠ doubleDecoration := by
 116  intro h
 117  have hobs := congrArg firstEdgeLength h
 118  rw [unitDecoration_firstEdgeLength, doubleDecoration_firstEdgeLength] at hobs
 119  norm_num at hobs
 120
 121/-- Both decorations live over one genuine simplicial carrier of exact
 122combinatorial complexity six, but have different edge and volume data. -/
 123theorem oneTetClass_has_two_metric_decorations :
 124    IsSimplicial oneTetComplex ∧
 125      complexity oneTetComplex = 6 ∧
 126      ∃ D₁ D₂ : MetricDecoration oneTetComplex,
 127        D₁ ≠ D₂ ∧
 128        firstEdgeLength D₁ = 1 ∧ firstEdgeLength D₂ = 2 ∧
 129        cayleyMengerObservable D₁ = 4 ∧
 130          cayleyMengerObservable D₂ = 256 := by
 131  refine ⟨oneTetComplex_isSimplicial, rfl,
 132    unitDecoration, doubleDecoration, unitDecoration_ne_doubleDecoration,
 133    unitDecoration_firstEdgeLength, doubleDecoration_firstEdgeLength,
 134    unitDecoration_cayleyMenger, doubleDecoration_cayleyMenger⟩
 135
 136/-- The one-tetrahedron quotient class at cap six. -/
 137def oneTetClass : TriangulationClass 6 :=
 138  Quotient.mk (relabelSetoid 6) oneTetComplex
 139
 140/-- **P2.5 MESH BLOCKER.** No function of the current combinatorial quotient
 141class alone can recover the first-edge length of both admissible metric
 142decorations. -/
 143theorem no_class_only_mesh_recovers_both
 144    (mesh : TriangulationClass 6 → ℝ) :
 145    ¬ (mesh oneTetClass = firstEdgeLength unitDecoration ∧
 146      mesh oneTetClass = firstEdgeLength doubleDecoration) := by
 147  rw [unitDecoration_firstEdgeLength, doubleDecoration_firstEdgeLength]
 148  rintro ⟨h₁, h₂⟩
 149  linarith
 150
 151/-- The same obstruction holds for an action-relevant Cayley-Menger
 152observable, not only for a chosen edge coordinate. -/
 153theorem no_class_only_cayleyMenger_recovers_both
 154    (observable : TriangulationClass 6 → ℝ) :
 155    ¬ (observable oneTetClass = cayleyMengerObservable unitDecoration ∧
 156      observable oneTetClass = cayleyMengerObservable doubleDecoration) := by
 157  rw [unitDecoration_cayleyMenger, doubleDecoration_cayleyMenger]
 158  rintro ⟨h₁, h₂⟩
 159  linarith
 160
 161/-- The unit metric packaged as a metric-decorated simplicial complex. -/
 162def unitMetricOneTet : MetricDecoratedComplex 6 where
 163  carrier := oneTetComplex
 164  simplicial := oneTetComplex_isSimplicial
 165  metric := unitDecoration
 166
 167/-- The edge-length-two metric packaged over the identical carrier. -/
 168def doubleMetricOneTet : MetricDecoratedComplex 6 where
 169  carrier := oneTetComplex
 170  simplicial := oneTetComplex_isSimplicial
 171  metric := doubleDecoration
 172
 173theorem unitMetricOneTet_ne_doubleMetricOneTet :
 174    unitMetricOneTet ≠ doubleMetricOneTet := by
 175  intro h
 176  have hsig := congrArg
 177    (fun G : MetricDecoratedComplex 6 =>
 178      (⟨G.carrier, G.metric⟩ : Σ K : BoundedComplex 6, MetricDecoration K)) h
 179  simp only [Sigma.mk.injEq] at hsig
 180  exact unitDecoration_ne_doubleDecoration (eq_of_heq hsig.2)
 181
 182theorem unit_double_toClass_eq :
 183    unitMetricOneTet.toClass = doubleMetricOneTet.toClass := rfl
 184
 185/-- **CARRIER BLOCKER.** The current `TriangulationClass` quotient forgets
 186physical metric data: its forgetful map from decorated simplicial geometries
 187is not injective. -/
 188theorem metricForget_not_injective :
 189    ¬ Function.Injective
 190      (MetricDecoratedComplex.toClass :
 191        MetricDecoratedComplex 6 → TriangulationClass 6) := by
 192  intro hinj
 193  exact unitMetricOneTet_ne_doubleMetricOneTet
 194    (hinj unit_double_toClass_eq)
 195
 196/-! ## 3. Independent check against the causal four-simplex metric API -/
 197
 198/-- The same combinatorial causal 4-simplex type has different 4-volume
 199observables at two lattice spacings. This is independent confirmation from
 200the 4D Cayley-Menger API that simplex type does not determine metric scale. -/
 201theorem causalPent_metric_observable_varies :
 202    CausalSimplex4D.cm4
 203        (CausalSimplex4D.euclideanSqEdges
 204          CausalSimplex4D.CausalPentType.fourOne 1 1) = 5 ∧
 205      CausalSimplex4D.cm4
 206        (CausalSimplex4D.euclideanSqEdges
 207          CausalSimplex4D.CausalPentType.fourOne 2 1) = 1280 := by
 208  constructor
 209  · rw [CausalSimplex4D.cm4_euclidean_fourOne]
 210    norm_num
 211  · rw [CausalSimplex4D.cm4_euclidean_fourOne]
 212    norm_num
 213
 214/-! ## 4. The minimal missing geometric-refinement carrier
 215
 216This interface deliberately assumes neither a path-sum limit nor an action
 217limit. It asks for finite metric-decorated levels, an actual mesh tending to
 218zero, a coarse projection between adjacent levels, and a summable local bound
 219on action changes. Those data are absent from `BoundedComplex`,
 220`TriangulationClass`, `ExactPathClass`, and `CapShellCompatibility`.
 221-/
 222
 223/-- Minimal metric-refinement and action-control data needed to replace a
 224bare complexity cutoff by a geometric refinement sequence.
 225
 226`Config n` is the finite metric-decorated configuration space at level `n`.
 227`coarsen` identifies the adjacent-level histories whose action increments are
 228controlled. `mesh_tendsto_zero` is geometric refinement; `cap_strictMono`
 229separately records increasing combinatorial capacity. The summable
 230`actionStepError` is a local quantitative premise, not the desired path-sum
 231convergence conclusion. -/
 232structure MetricRefinementFamily where
 233  Config : ℕ → Type
 234  finiteConfig : ∀ n, Fintype (Config n)
 235  cap : ℕ → ℕ
 236  cap_strictMono : StrictMono cap
 237  decorated : ∀ n, Config n → MetricDecoratedComplex (cap n)
 238  coarsen : ∀ n, Config (n + 1) → Config n
 239  mesh : ℕ → ℝ
 240  mesh_pos : ∀ n, 0 < mesh n
 241  edgeLength_le_mesh :
 242    ∀ n (c : Config n) (e : Fin (decorated n c).carrier.nE),
 243      Real.sqrt ((decorated n c).metric.sqEdge e) ≤ mesh n
 244  mesh_attained :
 245    ∀ n, ∃ c : Config n, ∃ e : Fin (decorated n c).carrier.nE,
 246      Real.sqrt ((decorated n c).metric.sqEdge e) = mesh n
 247  mesh_tendsto_zero :
 248    Filter.Tendsto mesh Filter.atTop (nhds 0)
 249  action : ∀ n, Config n → ℝ
 250  actionStepError : ℕ → ℝ
 251  actionStepError_nonneg : ∀ n, 0 ≤ actionStepError n
 252  actionStepError_summable : Summable actionStepError
 253  action_step_control :
 254    ∀ n (c : Config (n + 1)),
 255      |action (n + 1) c - action n (coarsen n c)| ≤ actionStepError n
 256
 257/-- The finite-level path sum on the metric-decorated carrier. The measure is
 258an explicit argument because its substrate derivation is the separate P2.2
 259obligation. -/
 260noncomputable def metricZ (F : MetricRefinementFamily)
 261    (measure : ∀ n, F.Config n → ℝ) (n : ℕ) : ℂ := by
 262  letI := F.finiteConfig n
 263  exact ∑ c : F.Config n,
 264    (measure n c : ℂ) * Complex.exp (Complex.I * (F.action n c : ℂ))
 265
 266/-- The geometric Z_RS continuum target that becomes well-typed only after a
 267`MetricRefinementFamily` and an explicit measure are supplied. This is a
 268definition of the OPEN target, not a theorem asserting it. -/
 269def HasGeometricZRSContinuumLimit (F : MetricRefinementFamily)
 270    (measure : ∀ n, F.Config n → ℝ) : Prop :=
 271  ∃ L : ℂ, Filter.Tendsto (fun n => metricZ F measure n)
 272    Filter.atTop (nhds L)
 273
 274#print axioms oneTetClass_has_two_metric_decorations
 275#print axioms no_class_only_mesh_recovers_both
 276#print axioms no_class_only_cayleyMenger_recovers_both
 277#print axioms metricForget_not_injective
 278#print axioms causalPent_metric_observable_varies
 279
 280end
 281
 282end MetricRefinementCarrierBlocker
 283end SevenGaps
 284end Gravity
 285end IndisputableMonolith
 286