Encyclopedia Gravity Gravity Track1 Bcorrected Quadratic Both Correspondences Force Equal Quadratics

ARTICLE 3 claims 3 theorems

Gravity Track1 Bcorrected Quadratic Both Correspondences Force Equal Quadratics

In the framework's discrete model of gravity, two candidate quadratic approximations to the same action cannot both be correct unless they are the same quadratic.

Verify this page

The rigidity theorem

The theorem named both_correspondences_force_equal_quadratics is a uniqueness result inside the Recognition Science framework's discrete model of gravity. The framework works with a discrete record of events, a ledger, on a three-dimensional periodic lattice. On such a lattice, the framework defines an action, a number assigned to each possible configuration of vertex potentials, which are real numbers attached to the lattice points. The action is a discrete analogue of the Regge action from classical lattice gravity. The theorem concerns two specific quadratic forms, which are homogeneous degree-two functions of the vertex potentials, that serve as candidate leading-order approximations to this action near the zero configuration.

The first candidate is the legacy edge stencil, a quadratic form built from sums over the lattice's edges. The second is the corrected axis stencil, a quadratic form built from sums over the lattice's axes. Each stencil is said to satisfy a local correspondence if it approximates the action's quadratic Taylor coefficient in a precise, uniform sense on a small neighborhood of the zero potential. The theorem states that if both the legacy and the corrected stencils satisfy this local correspondence on the same lattice, then the two stencils are pointwise equal as functions of the vertex potentials. In other words, two distinct quadratic approximations cannot both be correct; the correspondence is rigid.

This rigidity is a consequence of a more general theorem proved in the same module: any two homogeneous quadratics that satisfy the local correspondence on the same triangulation must be identical. The specialized theorem for the two stencils follows directly. The proof is machine-checked in the framework's library of formal theorems, with no unproved axioms beyond the standard logical ones. The theorem does not itself say which stencil is the correct one; it only says they cannot both be. A separate, earlier audit found a specific configuration where the two stencils differ, so the rigidity theorem implies that at most one of them can be the true Taylor coefficient. A further result, the corrected gate at lattice size five, is what selects the axis stencil.

What the theorem does not claim is just as important. It does not establish that either stencil actually satisfies the local correspondence; that is a separate hypothesis. It does not prove that the axis stencil is the correct one; that requires the additional gate result. It does not apply to arbitrary lattices, only to the specific periodic Freudenthal tori with each side length greater than two. And it says nothing about the all-cardinality generalization, which remains an open target in the framework.

THEOREM both_correspondences_force_equal_quadratics · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
both_correspondences_force_equal_quadratics · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:268 
/-- The legacy and corrected endpoints can both hold only if the two stencils
are pointwise equal. -/
theorem both_correspondences_force_equal_quadratics
    (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
    (hLegacy : CanonicalPeriodicEdgeStencilLocalCorrespondence Nx Ny Nz hx hy hz)
    (hCorrected : CanonicalPeriodicAxisStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
    ∀ ξ : VertexPotential
        (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K,
      periodicEdgeStencilDirichletAction
          (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz) ξ =
        canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ :=
  reggeLocalQuadraticCorrespondence_quadratic_unique
    (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
    (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
    _ _
    (periodicEdgeStencilDirichletAction_smul Nx Ny Nz hx hy hz)
    (canonicalPeriodicMixedAxisStencilAction_smul Nx Ny Nz hx hy hz)
    ((edgeStencilLocalCorrespondence_iff Nx Ny Nz hx hy hz).mp hLegacy)
    hCorrected
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 ξ)

What this page does not claim

The theorem does not prove that either stencil satisfies the local correspondence. The theorem does not establish that the axis stencil is the correct one. The theorem does not apply to lattices with any side length less than or equal to two.

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