Encyclopedia Gravity Gravity Track1 Bcorrected Quadratic Regge Local Quadratic Correspondence Quadrat

ARTICLE 3 claims 3 theorems

Gravity Track1 Bcorrected Quadratic Regge Local Quadratic Correspondence Quadrat

In a discrete model of gravity, a machine-checked theorem shows that only one quadratic energy expression can match the local curvature, settling a dispute between two candidate formulas.

Verify this page

The uniqueness theorem

In the Recognition Science framework's discrete model of gravity, space is built from tetrahedra, and the central quantity is the Regge action, a sum over the edges of the tetrahedra that measures how much the geometry bends. The framework's library of formal theorems asks a precise question: when you look at a tiny, nearly flat region of this discrete space, which quadratic expression in the vertex potentials best approximates the curvature? A recognition event, a discrete record of a comparison, is what the framework uses to force the answer.

The theorem reggeLocalQuadraticCorrespondence_quadratic_unique states that if two quadratic functions both satisfy the same local correspondence condition on the same triangulation, then they are pointwise equal. In plain language: there is only one quadratic expression that can serve as the local Taylor coefficient of the Regge action. The proof requires both quadratics to be homogeneous of degree two, meaning scaling the input by a factor scales the output by the square of that factor, and it requires the correspondence condition to hold, which means the quadratic matches the Regge action up to cubic error terms.

This uniqueness result has a direct consequence for two competing stencils, the legacy edge stencil and the corrected axis stencil. The theorem not_both_correspondences_of_quadratics_differ shows that if the two stencils differ on any single vertex potential, then they cannot both satisfy the correspondence. A separate audit, the Session 202 mismatch witness, proves that at the N = 5 single-vertex bump the two stencils do differ: the mixed quadratic evaluates to 12 while the edge stencil evaluates to 6 + 6√2 + 2√3. Therefore at most one of them can be the true quadratic coefficient, and the audit selects the axis stencil as the corrected endpoint.

The theorem does not claim that the corrected axis stencil is the unique quadratic for all possible triangulations. It only establishes uniqueness among quadratics that satisfy the correspondence on the same fixed triangulation. The all-cardinality generalization, a single explicit-fiber coefficient identity for arbitrary N, remains open. The N = 5 gate itself is closed by a separate theorem, correctedTrack1BGateAtN5_closed, which uses a finite coefficient certificate, but that is a different statement from the uniqueness theorem.

What the uniqueness theorem changes is the status of the correction. The corrected axis stencil is not a stylistic preference or an aesthetic improvement; it is the only quadratic that can consistently play the role of the local Taylor coefficient. The legacy stencil, once shown to differ, is excluded by the rigidity result. The framework's library proves that the correction is forced, not chosen.

THEOREM reggeLocalQuadraticCorrespondence_quadratic_unique · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
reggeLocalQuadraticCorrespondence_quadratic_unique · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:171 
/-- **RIGIDITY.**  If two quadratically homogeneous candidates both satisfy
the local correspondence on the same complex, they are pointwise equal.  The
quadratic coefficient of a cubic-Taylor expansion is unique, so at most one
stencil can be the true second-order content of the Regge action. -/
theorem reggeLocalQuadraticCorrespondence_quadratic_unique
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (Q₁ Q₂ : VertexPotential K → ℝ)
    (hQ₁ : ∀ (a : ℝ) (ξ : VertexPotential K), Q₁ (a • ξ) = a ^ (2 : ℕ) * Q₁ ξ)
    (hQ₂ : ∀ (a : ℝ) (ξ : VertexPotential K), Q₂ (a • ξ) = a ^ (2 : ℕ) * Q₂ ξ)
    (h₁ : ReggeLocalQuadraticCorrespondence K hK Q₁)
    (h₂ : ReggeLocalQuadraticCorrespondence K hK Q₂) :
    ∀ ξ : VertexPotential K, Q₁ ξ = Q₂ ξ := by
  obtain ⟨r₁, C₁, hr₁, hC₁, hb₁⟩ := h₁
  obtain ⟨r₂, C₂, hr₂, hC₂, hb₂⟩ := h₂
  intro ξ
  by_contra hne
  have hΔpos : 0 < |Q₁ ξ - Q₂ ξ| := abs_pos.mpr (sub_ne_zero.mpr hne)
  set Δ : ℝ := |Q₁ ξ - Q₂ ξ| with hΔdef
  -- Choose the probe scale `t`.
  have hA : (0 : ℝ) < 1 + ‖ξ‖ := by positivity
  have hB : (0 : ℝ) < 1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ) := by positivity
  set t : ℝ :=
    min (min r₁ r₂ / (1 + ‖ξ‖)) (Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)))
    with ht_def
  have ht_pos : 0 < t := by
    refine lt_min (div_pos (lt_min hr₁ hr₂) hA) (div_pos hΔpos hB)
  -- The scaled probe sits inside both radii.
  have ht_norm : ‖t • ξ‖ = t * ‖ξ‖ := by
    rw [norm_smul, Real.norm_eq_abs, abs_of_pos ht_pos]
  have hsmall : t * ‖ξ‖ < min r₁ r₂ := by
    have h1 : t ≤ min r₁ r₂ / (1 + ‖ξ‖) := min_le_left _ _
    have h2 : ‖ξ‖ < 1 + ‖ξ‖ := by linarith [norm_nonneg ξ]
    have hq_pos : 0 < min r₁ r₂ / (1 + ‖ξ‖) := div_pos (lt_min hr₁ hr₂) hA
    calc t * ‖ξ‖ ≤ (min r₁ r₂ / (1 + ‖ξ‖)) * ‖ξ‖ :=
          mul_le_mul_of_nonneg_right h1 (norm_nonneg ξ)
      _ < (min r₁ r₂ / (1 + ‖ξ‖)) * (1 + ‖ξ‖) :=
          mul_lt_mul_of_pos_left h2 hq_pos
      _ = min r₁ r₂ := div_mul_cancel₀ _ hA.ne'
  have hsmall₁ : ‖t • ξ‖ < r₁ := by
    rw [ht_norm]; exact lt_of_lt_of_le hsmall (min_le_left _ _)
  have hsmall₂ : ‖t • ξ‖ < r₂ := by
    rw [ht_norm]; exact lt_of_lt_of_le hsmall (min_le_right _ _)
  -- The two cubic bounds at the scaled probe.
  have hb₁' := hb₁ (t • ξ) hsmall₁
  have hb₂' := hb₂ (t • ξ) hsmall₂
  rw [hQ₁ t ξ, Real.norm_eq_abs, ht_norm] at hb₁'
  rw [hQ₂ t ξ, Real.norm_eq_abs, ht_norm] at hb₂'
  -- Triangle inequality forces the quadratic gap below a linear-in-`t` bound.
  have hdiff :
      (reggeAction K hK (t • ξ) - reggeAction K hK (zeroPotential K) -
          (1 / 2) * (t ^ (2 : ℕ) * Q₂ ξ)) -
        (reggeAction K hK (t • ξ) - reggeAction K hK (zeroPotential K) -
          (1 / 2) * (t ^ (2 : ℕ) * Q₁ ξ)) =
        (1 / 2) * t ^ (2 : ℕ) * (Q₁ ξ - Q₂ ξ) := by ring
  have hgap : (1 / 2) * t ^ (2 : ℕ) * Δ ≤ (C₁ + C₂) * (t * ‖ξ‖) ^ (3 : ℕ) := by
    have htri :
        |(1 / 2) * t ^ (2 : ℕ) * (Q₁ ξ - Q₂ ξ)| ≤
          C₂ * (t * ‖ξ‖) ^ (3 : ℕ) + C₁ * (t * ‖ξ‖) ^ (3 : ℕ) := by
      rw [← hdiff]
      exact le_trans (abs_sub _ _) (add_le_add hb₂' hb₁')
    have habs :
        |(1 / 2) * t ^ (2 : ℕ) * (Q₁ ξ - Q₂ ξ)| =
          (1 / 2) * t ^ (2 : ℕ) * Δ := by
      rw [abs_mul, abs_of_nonneg (by positivity : (0:ℝ) ≤ (1/2) * t ^ (2:ℕ))]
    rw [habs] at htri
    linarith
  -- Divide by `t²` and contradict the choice of `t`.
  have ht2_pos : (0 : ℝ) < t ^ (2 : ℕ) := by positivity
  have hΔle : Δ ≤ 2 * (C₁ + C₂) * t * ‖ξ‖ ^ (3 : ℕ) := by
    have hexp : (t * ‖ξ‖) ^ (3 : ℕ) = t ^ (2 : ℕ) * (t * ‖ξ‖ ^ (3 : ℕ)) := by
      ring
    rw [hexp] at hgap
    calc Δ = (1 / 2) * t ^ (2 : ℕ) * Δ * (2 / t ^ (2 : ℕ)) := by
          field_simp
      _ ≤ (C₁ + C₂) * (t ^ (2 : ℕ) * (t * ‖ξ‖ ^ (3 : ℕ))) * (2 / t ^ (2 : ℕ)) :=
          mul_le_mul_of_nonneg_right hgap (by positivity)
      _ = 2 * (C₁ + C₂) * t * ‖ξ‖ ^ (3 : ℕ) := by
          field_simp
  have ht_le : t ≤ Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := min_le_right _ _
  have hfinal : Δ < Δ := by
    have hC12 : 0 ≤ C₁ + C₂ := by linarith
    have hfrac :
        2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ) <
          1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ) := by linarith
    calc Δ ≤ 2 * (C₁ + C₂) * t * ‖ξ‖ ^ (3 : ℕ) := hΔle
      _ = t * (2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := by ring
      _ ≤ (Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ))) *
            (2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := by
          refine mul_le_mul_of_nonneg_right ht_le ?_
          positivity
      _ < (Δ / (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ))) *
            (1 + 2 * (C₁ + C₂) * ‖ξ‖ ^ (3 : ℕ)) := by
          refine mul_lt_mul_of_pos_left hfrac ?_
          exact div_pos hΔpos hB
      _ = Δ := div_mul_cancel₀ _ hB.ne'
  exact absurd hfinal (lt_irrefl Δ)
THEOREM not_both_correspondences_of_quadratics_differ · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
not_both_correspondences_of_quadratics_differ · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:300 
/-- **EXCLUSIVITY.**  Given the audit witness, the legacy seven-class endpoint
and the corrected axis endpoint are mutually exclusive: at most one of them is
the true cubic-Taylor statement for the Regge action. -/
theorem not_both_correspondences_of_quadratics_differ
    (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
    (hdiff : AxisEdgeStencilQuadraticsDiffer Nx Ny Nz hx hy hz) :
    ¬(CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz ∧
      CanonicalPeriodicAxisStencilLocalCorrespondence Nx Ny Nz hx hy hz) := by
  rintro ⟨hLegacy, hCorrected⟩
  obtain ⟨ξ, hξ⟩ := hdiff
  exact hξ (both_correspondences_force_equal_quadratics
    Nx Ny Nz hx hy hz hLegacy hCorrected ξ)
THEOREM correctedTrack1BGateAtN5_closed · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
correctedTrack1BGateAtN5_closed · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:395 
/-- **The corrected `N = 5` gate is closed** (2026-06-17). It is discharged by
`FreudenthalAxisStencilCoeffCert.canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5`,
which proves the explicit-fiber axis-stencil coefficient identity via a finite
`native_decide` certificate over the 125 = 5³ vertex table. Honest caveat: that
certificate's axiom basis includes `Lean.ofReduceBool` and `Lean.trustCompiler`
(compiler trust) on top of `propext / Classical.choice / Quot.sound`. -/
theorem correctedTrack1BGateAtN5_closed : CanonicalPeriodicCorrectedTrack1BGateAtN5 :=
  FreudenthalAxisStencilCoeffCert.canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5

What this page does not claim

The theorem does not prove the axis stencil is the unique quadratic for all possible triangulations, only for a fixed one. The theorem does not establish the all-cardinality generalization, which remains an open target. The theorem does not itself close the N = 5 gate; that is a separate theorem using a finite coefficient certificate.

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/Track1BCorrectedQuadratic.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