Encyclopedia Gravity Gravity Track1 Bcorrected Quadratic Axis Normalized Regge Bound Of Correspondenc
ARTICLE 4 claims 4 theorems
Gravity Track1 Bcorrected Quadratic Axis Normalized Regge Bound Of Correspondenc
A machine-checked theorem pins down the exact quadratic that describes gravity's local behavior on a discrete spacetime grid, and shows why the older candidate cannot be right.
The corrected bound
In numerical relativity, a stencil is a fixed pattern of points used to approximate a derivative or an action. The declaration axis_normalized_regge_bound_of_correspondence is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that if a particular quadratic form, called the axis stencil, correctly describes the local behavior of the Regge action (a discrete version of gravity's action) on a periodic three-dimensional grid, then a specific bound follows: the difference between the normalized Regge action and half the axis stencil action is controlled by a term that shrinks like the cube of the potential's size.
The theorem is conditional. It does not assert that the axis stencil is the correct one; it takes that as a hypothesis. What it proves is the consequence: given that correspondence, the bound holds. This bound is the hook that lets a larger, damped-schedule closure argument transfer to the corrected quadratic. The theorem is proved parametrically, meaning it works for any quadratic satisfying the correspondence, not just the axis stencil. This generality is what makes the damped pipeline transferable the day the corrected gate closes.
The theorem also carries the weight of a correction. An earlier identification used a different quadratic, the edge stencil. A separate finite audit showed the two stencils disagree at a single-vertex bump on a five-point grid: the mixed quadratic evaluates to 12, while the edge stencil evaluates to 6 + 6√2 + 2√3. Because of this mismatch, at most one of the two quadratics can be the true Taylor coefficient. The rigidity theorem proves that two homogeneous quadratics satisfying the correspondence on the same complex must be pointwise equal. Therefore, if they differ, they cannot both be correct. The audit selects the axis stencil.
In Recognition Science, the framework's library proves the corrected endpoint, the algebra of the axis stencil, the rigidity, and the exclusivity with the legacy stencil. The all-cardinality generalization, a single coefficient identity for arbitrary grid size N, remains open. The theorem does not claim that the axis stencil is the unique correct quadratic for all grids, nor does it assert that the correspondence itself holds; it only establishes the bound that follows from it.
THEOREM axis_normalized_regge_bound_of_correspondence · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- The corrected endpoint feeds the damped D2 pipeline: under the axis
correspondence, the normalized nonlinear Regge action converges to one half
of the axis stencil with the same constructive damping bound used by the
damped-schedule closure. -/
theorem axis_normalized_regge_bound_of_correspondence
(Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
(hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
(hCorr : CanonicalPeriodicAxisStencilLocalCorrespondence Nx Ny Nz hx hy hz) :
∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
∀ (s : ℝ), s ≠ 0 →
∀ ξ : VertexPotential
(canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K,
‖s • ξ‖ < r →
|reggeAction
(canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
(canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
(s • ξ) / s ^ (2 : ℕ) -
(1 / 2) *
canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ| ≤
C * |s| * ‖ξ‖ ^ (3 : ℕ) := by
obtain ⟨r, C, hr, hC, hb⟩ := hCorr
refine ⟨r, C, hr, hC, fun s hs ξ hsmall => ?_⟩
exact normalized_regge_sub_half_quadratic_abs_le
(canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
(canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK
(canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz)
(canonicalPeriodicMixedAxisStencilAction_smul Nx Ny Nz hx hy hz)
(canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatConfiguration
Nx Ny Nz hx hy hz
(canonicalPeriodicFlatConfiguration Nx Ny Nz hx hy hz))
r C hb s hs ξ hsmall
THEOREM normalized_regge_sub_half_quadratic_abs_le · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- 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 not_both_correspondences_of_quadratics_differ · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- **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 reggeLocalQuadraticCorrespondence_quadratic_unique · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- **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 axis stencil is the correct quadratic; it only proves the bound that follows from that hypothesis. The theorem does not establish the correspondence itself for any grid size. The all-cardinality generalization for arbitrary N remains open, not proved.
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:
- What physical interpretation does the axis stencil have in the continuum limit?
- How does the corrected quadratic change the predicted value of a physical observable?
- What is the explicit-fiber coefficient identity that would close the all-cardinality generalization?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM axis_normalized_regge_bound_of_correspondence · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- The corrected endpoint feeds the damped D2 pipeline: under the axis correspondence, the normalized nonlinear Regge action converges to one half of the axis stencil with the same constructive damping bound used by the damped-schedule closure. -/ theorem axis_normalized_regge_bound_of_correspondence (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) (hCorr : CanonicalPeriodicAxisStencilLocalCorrespondence Nx Ny Nz hx hy hz) : ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧ ∀ (s : ℝ), s ≠ 0 → ∀ ξ : VertexPotential (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K, ‖s • ξ‖ < r → |reggeAction (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK (s • ξ) / s ^ (2 : ℕ) - (1 / 2) * canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ| ≤ C * |s| * ‖ξ‖ ^ (3 : ℕ) := by obtain ⟨r, C, hr, hC, hb⟩ := hCorr refine ⟨r, C, hr, hC, fun s hs ξ hsmall => ?_⟩ exact normalized_regge_sub_half_quadratic_abs_le (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK (canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz) (canonicalPeriodicMixedAxisStencilAction_smul Nx Ny Nz hx hy hz) (canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatConfiguration Nx Ny Nz hx hy hz (canonicalPeriodicFlatConfiguration Nx Ny Nz hx hy hz)) r C hb s hs ξ hsmallThe theorem states that if the axis stencil correctly describes the local behavior of the Regge action, then a specific bound follows, controlling the difference between the normalized Regge action and half the axis stencil action. axis_normalized_regge_bound_of_correspondence · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.leanTHEOREM normalized_regge_sub_half_quadratic_abs_le · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- 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_simpThe theorem is proved parametrically, meaning it works for any quadratic satisfying the correspondence. normalized_regge_sub_half_quadratic_abs_le · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.leanTHEOREM not_both_correspondences_of_quadratics_differ · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- **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 ξ)A finite audit showed the mixed quadratic and the edge stencil differ at a single-vertex bump on a five-point grid. not_both_correspondences_of_quadratics_differ · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.leanTHEOREM reggeLocalQuadraticCorrespondence_quadratic_unique · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
/-- **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 Δ)Two homogeneous quadratics satisfying the correspondence on the same complex must be pointwise equal. reggeLocalQuadraticCorrespondence_quadratic_unique · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean