Encyclopedia Gravity Gravity Track1 Bcorrected Quadratic

ARTICLE 4 claims 4 theorems

Gravity Track1 Bcorrected Quadratic

A machine-checked audit found the old formula for a gravity term was wrong, and the correction is now a proved theorem.

Verify this page

The corrected quadratic

In the Recognition Science framework, gravity is built from a discrete ledger of recognition events on a triangulated space. The relevant quantity is the Regge action, a sum over the space's hinges that measures how curvature accumulates. The framework's library, a machine-checked collection of formal theorems, now contains a corrected quadratic formula for this action, and the correction is not a stylistic choice but a forced result.

The old identification used a seven-class square-root edge stencil. A stencil is a fixed pattern of weights assigned to nearby points. The new audit, at a single-vertex bump with five neighbors, found the old stencil evaluates to 6 + 6√2 + 2√3, while the mixed quadratic evaluates to 12. These scalars differ, so the old identification was wrong-weighted. The corrected endpoint, the axis stencil, is a different pattern of weights that the audit selects.

The module proves a rigidity theorem: two homogeneous quadratics satisfying the local correspondence on the same complex must be pointwise equal. This means the legacy and corrected endpoints cannot both be correct unless the two stencils are identical, which they are not. The audit therefore forces the axis stencil as the true Taylor coefficient of the Regge action.

The module also proves the corrected gate at the N = 5 certificate scale is closed. This gate is a finite coefficient identity, and its closure means the correction is not merely plausible but established. What remains open is only the generalization to all cardinalities, a single explicit-fiber coefficient identity for arbitrary N.

The practical consequence is a damped-schedule closure for the D2 pipeline. The module proves a per-tetrahedron normalized residual bound parametrically in the quadratic, so the entire damped D2 pipeline transfers to the corrected quadratic the day the all-cardinality gate closes. The correction is not an aesthetic preference; it is what the audit forces.

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
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

What this page does not claim

The all-cardinality generalization of the gate is not proved. The physical recognition-to-linking bridge for gravity is not established. The module does not derive the value of any physical constant.

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