Encyclopedia Gravity Gravity Seven Gaps Metric Refinement Carrier Blocker Causal Pent Metric Observab

ARTICLE 4 claims 3 theorems 1 model

Gravity Seven Gaps Metric Refinement Carrier Blocker Causal Pent Metric Observab

A single combinatorial shape can carry two different metric geometries, so no shape-based map can recover the metric information.

Verify this page

The metric observable varies

The recognition framework, a discrete record of events, builds its models from combinatorial objects that record only how parts connect, not their sizes. The declaration in question, a theorem in the framework's machine-checked library of formal theorems, shows a concrete consequence of that limitation. It takes a specific five-simplex, a higher-dimensional analogue of a triangle, and decorates it with two different metric geometries: one where a chosen edge has squared length 1, and another where the same edge has squared length 4. The theorem computes a geometric observable, the Cayley-Menger determinant, which measures something like a generalized volume. For the first decoration the observable equals 5; for the second it equals 1280.

The two decorated complexes are distinct, yet they share the same underlying combinatorial type. A function that sees only the combinatorial type cannot tell them apart, so no such function can recover either the edge length or the Cayley-Menger observable for both decorations. The framework proves this impossibility directly: any map from the combinatorial class to the real numbers must fail to match both values. The declaration formalizes that the metric observable genuinely varies across metric decorations, even when the combinatorial carrier is fixed.

In Recognition Science, this result is a carrier blocker. It shows that the current combinatorial quotient, which identifies shapes by their incidence structure, is too coarse for metric questions. The framework's response is to propose a richer carrier, a metric refinement family, that includes metric data alongside the combinatorial structure. That family is a model, a definitional choice, not a derived theorem. The construction of such a family from the recognition substrate, the derivation of its measure and action, and the proof of a continuum limit all remain open targets.

THEOREM causalPent_metric_observable_varies · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean
causalPent_metric_observable_varies · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean:198 
/-- The same combinatorial causal 4-simplex type has different 4-volume
observables at two lattice spacings. This is independent confirmation from
the 4D Cayley-Menger API that simplex type does not determine metric scale. -/
theorem causalPent_metric_observable_varies :
    CausalSimplex4D.cm4
        (CausalSimplex4D.euclideanSqEdges
          CausalSimplex4D.CausalPentType.fourOne 1 1) = 5 ∧
      CausalSimplex4D.cm4
        (CausalSimplex4D.euclideanSqEdges
          CausalSimplex4D.CausalPentType.fourOne 2 1) = 1280 := by
  constructor
  · rw [CausalSimplex4D.cm4_euclidean_fourOne]
    norm_num
  · rw [CausalSimplex4D.cm4_euclidean_fourOne]
    norm_num
THEOREM causalPent_metric_observable_varies · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean
causalPent_metric_observable_varies · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean:198 
/-- The same combinatorial causal 4-simplex type has different 4-volume
observables at two lattice spacings. This is independent confirmation from
the 4D Cayley-Menger API that simplex type does not determine metric scale. -/
theorem causalPent_metric_observable_varies :
    CausalSimplex4D.cm4
        (CausalSimplex4D.euclideanSqEdges
          CausalSimplex4D.CausalPentType.fourOne 1 1) = 5 ∧
      CausalSimplex4D.cm4
        (CausalSimplex4D.euclideanSqEdges
          CausalSimplex4D.CausalPentType.fourOne 2 1) = 1280 := by
  constructor
  · rw [CausalSimplex4D.cm4_euclidean_fourOne]
    norm_num
  · rw [CausalSimplex4D.cm4_euclidean_fourOne]
    norm_num
THEOREM no_class_only_cayleyMenger_recovers_both · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean
no_class_only_cayleyMenger_recovers_both · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean:151 
/-- The same obstruction holds for an action-relevant Cayley-Menger
observable, not only for a chosen edge coordinate. -/
theorem no_class_only_cayleyMenger_recovers_both
    (observable : TriangulationClass 6 → ℝ) :
    ¬ (observable oneTetClass = cayleyMengerObservable unitDecoration ∧
      observable oneTetClass = cayleyMengerObservable doubleDecoration) := by
  rw [unitDecoration_cayleyMenger, doubleDecoration_cayleyMenger]
  rintro ⟨h₁, h₂⟩
  linarith
MODEL MetricRefinementFamily · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean
MetricRefinementFamily · IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean:223 
/-- Minimal metric-refinement and action-control data needed to replace a
bare complexity cutoff by a geometric refinement sequence.

`Config n` is the finite metric-decorated configuration space at level `n`.
`coarsen` identifies the adjacent-level histories whose action increments are
controlled. `mesh_tendsto_zero` is geometric refinement; `cap_strictMono`
separately records increasing combinatorial capacity. The summable
`actionStepError` is a local quantitative premise, not the desired path-sum
convergence conclusion. -/
structure MetricRefinementFamily where
  Config : ℕ → Type
  finiteConfig : ∀ n, Fintype (Config n)
  cap : ℕ → ℕ
  cap_strictMono : StrictMono cap
  decorated : ∀ n, Config n → MetricDecoratedComplex (cap n)
  coarsen : ∀ n, Config (n + 1) → Config n
  mesh : ℕ → ℝ
  mesh_pos : ∀ n, 0 < mesh n
  edgeLength_le_mesh :
    ∀ n (c : Config n) (e : Fin (decorated n c).carrier.nE),
      Real.sqrt ((decorated n c).metric.sqEdge e) ≤ mesh n
  mesh_attained :
    ∀ n, ∃ c : Config n, ∃ e : Fin (decorated n c).carrier.nE,
      Real.sqrt ((decorated n c).metric.sqEdge e) = mesh n
  mesh_tendsto_zero :
    Filter.Tendsto mesh Filter.atTop (nhds 0)
  action : ∀ n, Config n → ℝ
  actionStepError : ℕ → ℝ
  actionStepError_nonneg : ∀ n, 0 ≤ actionStepError n
  actionStepError_summable : Summable actionStepError
  action_step_control :
    ∀ n (c : Config (n + 1)),
      |action (n + 1) c - action n (coarsen n c)| ≤ actionStepError n

What this page does not claim

This theorem does not construct a metric refinement family from the recognition substrate. This theorem does not prove that any continuum limit exists for the proposed metric refinement family. This theorem does not change any full-theory flag or resolve the complexity-cutoff convergence question.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND