Encyclopedia Gravity Gravity Track1 Bcorrected Quadratic Normalized Regge Sub Half Quadratic Abs Le

ARTICLE 3 claims 3 theorems

Gravity Track1 Bcorrected Quadratic Normalized Regge Sub Half Quadratic Abs Le

A machine-checked inequality that controls how a discrete geometry's energy behaves under scaling, and the precise limit of what that control proves.

Verify this page

The normalized bound

The declaration normalized_regge_sub_half_quadratic_abs_le is a theorem about a discrete geometry: a triangulated space, built from flat tetrahedra glued along faces, with a number attached to each vertex. The theorem bounds how a certain energy, the Regge action, changes when you scale all vertex values by a common factor. It states that after dividing by the square of that scale factor, the difference between the scaled energy and half a quadratic form is controlled by a constant times the scale factor times the cube of the vertex values. In plain terms, it says that for small perturbations, the energy behaves like a quadratic function, with the error shrinking as the perturbation shrinks, and it quantifies exactly how fast that error shrinks.

The bound is parametric: it works for any quadratic form Q that satisfies a homogeneity condition, meaning that scaling the input scales the output by the square of the scale factor. This generality is what makes the theorem a hook for a larger program. The framework's machine-checked library of formal theorems proves the bound once, parametrically, and the same proof then transfers to any specific quadratic that meets the condition. The axis stencil, a particular quadratic form defined by a pattern of edge weights, is the corrected endpoint in this program, and the theorem supplies the normalized bound for it as a special case.

The theorem does not claim that the quadratic form Q is the true second-order Taylor coefficient of the Regge action. That identification is a separate question, settled by a different theorem that proves uniqueness: if two homogeneous quadratics both satisfy the local correspondence with the Regge action, they are equal. The normalized bound only controls the error term, given that a correspondence already holds. It also does not assert that the energy itself is quadratic, only that it is quadratically approximated near zero. The bound is a tool for the damped-schedule closure, a later stage of the framework's derivation, not a standalone statement about the physical content of gravity.

THEOREM normalized_regge_sub_half_quadratic_abs_le · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
normalized_regge_sub_half_quadratic_abs_le · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:317 
/-- The normalized per-tetrahedron residual bound, proved for an arbitrary
homogeneous quadratic satisfying the cubic bound.  This is the exact bound
the damped-schedule D2 closure consumes, so the whole damped pipeline
transfers to the corrected quadratic the day the corrected gate closes. -/
theorem normalized_regge_sub_half_quadratic_abs_le
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (Q : VertexPotential K → ℝ)
    (hQ : ∀ (a : ℝ) (ξ : VertexPotential K), Q (a • ξ) = a ^ (2 : ℕ) * Q ξ)
    (h0 : reggeAction K hK (zeroPotential K) = 0)
    (r C : ℝ)
    (hb : ∀ ξ : VertexPotential K, ‖ξ‖ < r →
      ‖reggeAction K hK ξ - reggeAction K hK (zeroPotential K) -
        (1 / 2) * Q ξ‖ ≤ C * ‖ξ‖ ^ (3 : ℕ))
    (s : ℝ) (hs : s ≠ 0)
    (ξ : VertexPotential K) (hsmall : ‖s • ξ‖ < r) :
    |reggeAction K hK (s • ξ) / s ^ (2 : ℕ) - (1 / 2) * Q ξ| ≤
      C * |s| * ‖ξ‖ ^ (3 : ℕ) := by
  have hb' := hb (s • ξ) hsmall
  rw [h0, sub_zero, hQ s ξ, Real.norm_eq_abs] at hb'
  have hs2 : (0 : ℝ) < s ^ (2 : ℕ) := by positivity
  have key :
      reggeAction K hK (s • ξ) / s ^ (2 : ℕ) - (1 / 2) * Q ξ =
        (reggeAction K hK (s • ξ) - (1 / 2) * (s ^ (2 : ℕ) * Q ξ)) / s ^ (2 : ℕ) := by
    field_simp
  rw [key, abs_div, abs_of_pos hs2]
  have hnorm3 : ‖s • ξ‖ ^ (3 : ℕ) = |s| ^ (3 : ℕ) * ‖ξ‖ ^ (3 : ℕ) := by
    rw [norm_smul, Real.norm_eq_abs, mul_pow]
  have habs3 : |s| ^ (3 : ℕ) = |s| * s ^ (2 : ℕ) := by
    rw [pow_succ, sq_abs, mul_comm]
  have hdivle :
      |reggeAction K hK (s • ξ) - (1 / 2) * (s ^ (2 : ℕ) * Q ξ)| / s ^ (2 : ℕ) ≤
        (C * ‖s • ξ‖ ^ (3 : ℕ)) / s ^ (2 : ℕ) := by
    gcongr
  refine le_trans hdivle (le_of_eq ?_)
  rw [hnorm3, habs3]
  field_simp
THEOREM normalized_regge_sub_half_quadratic_abs_le · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
normalized_regge_sub_half_quadratic_abs_le · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:317 
/-- The normalized per-tetrahedron residual bound, proved for an arbitrary
homogeneous quadratic satisfying the cubic bound.  This is the exact bound
the damped-schedule D2 closure consumes, so the whole damped pipeline
transfers to the corrected quadratic the day the corrected gate closes. -/
theorem normalized_regge_sub_half_quadratic_abs_le
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (Q : VertexPotential K → ℝ)
    (hQ : ∀ (a : ℝ) (ξ : VertexPotential K), Q (a • ξ) = a ^ (2 : ℕ) * Q ξ)
    (h0 : reggeAction K hK (zeroPotential K) = 0)
    (r C : ℝ)
    (hb : ∀ ξ : VertexPotential K, ‖ξ‖ < r →
      ‖reggeAction K hK ξ - reggeAction K hK (zeroPotential K) -
        (1 / 2) * Q ξ‖ ≤ C * ‖ξ‖ ^ (3 : ℕ))
    (s : ℝ) (hs : s ≠ 0)
    (ξ : VertexPotential K) (hsmall : ‖s • ξ‖ < r) :
    |reggeAction K hK (s • ξ) / s ^ (2 : ℕ) - (1 / 2) * Q ξ| ≤
      C * |s| * ‖ξ‖ ^ (3 : ℕ) := by
  have hb' := hb (s • ξ) hsmall
  rw [h0, sub_zero, hQ s ξ, Real.norm_eq_abs] at hb'
  have hs2 : (0 : ℝ) < s ^ (2 : ℕ) := by positivity
  have key :
      reggeAction K hK (s • ξ) / s ^ (2 : ℕ) - (1 / 2) * Q ξ =
        (reggeAction K hK (s • ξ) - (1 / 2) * (s ^ (2 : ℕ) * Q ξ)) / s ^ (2 : ℕ) := by
    field_simp
  rw [key, abs_div, abs_of_pos hs2]
  have hnorm3 : ‖s • ξ‖ ^ (3 : ℕ) = |s| ^ (3 : ℕ) * ‖ξ‖ ^ (3 : ℕ) := by
    rw [norm_smul, Real.norm_eq_abs, mul_pow]
  have habs3 : |s| ^ (3 : ℕ) = |s| * s ^ (2 : ℕ) := by
    rw [pow_succ, sq_abs, mul_comm]
  have hdivle :
      |reggeAction K hK (s • ξ) - (1 / 2) * (s ^ (2 : ℕ) * Q ξ)| / s ^ (2 : ℕ) ≤
        (C * ‖s • ξ‖ ^ (3 : ℕ)) / s ^ (2 : ℕ) := by
    gcongr
  refine le_trans hdivle (le_of_eq ?_)
  rw [hnorm3, habs3]
  field_simp
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 Δ)

What this page does not claim

The theorem does not prove that the Regge action itself is quadratic. The theorem does not identify which quadratic form is the correct one; that is a separate uniqueness result. The theorem does not assert the physical correctness of the discrete gravity model.

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