Encyclopedia Gravity Gravity Track1 Bcorrected Quadratic Periodic Edge Stencil Dirichlet Action Smul

ARTICLE 4 claims 4 theorems

Gravity Track1 Bcorrected Quadratic Periodic Edge Stencil Dirichlet Action Smul

A small algebraic fact about a gravity calculation: scaling the input scales the output by the square, a property that pins down a unique quadratic form.

Verify this page

Scaling law for a stencil

In numerical analysis, a stencil is a fixed pattern of neighboring points used to approximate a derivative or an action. The declaration periodicEdgeStencilDirichletAction_smul establishes a scaling property for one such stencil on a periodic three-dimensional grid. It states that if you multiply every value in the potential field by a constant a, the stencil's output is multiplied by a squared. This is the signature of a quadratic form: a homogeneous degree-two function.

The proof is a direct computation in the framework's machine-checked library of formal theorems. It applies to the canonical periodic Freudenthal torus, a specific triangulation of a three-torus, and to any real scaling factor. The statement is unconditional, with no hidden assumptions beyond the grid being larger than two cells in each direction. The same scaling law is proved for the corrected axis stencil, and the two are shown to be the only possible quadratic endpoints under a local correspondence condition.

This scaling law is not just a technical curiosity. It is the algebraic backbone of a rigidity result: any two homogeneous quadratics that satisfy the same local correspondence must be pointwise equal. That uniqueness is what allows the framework to argue that the corrected axis stencil, not the legacy one, is the true Taylor coefficient of the Regge action. The scaling property is the first step in that argument, and it is what makes the quadratic structure usable in the damped-schedule closure.

In Recognition Science, this fact is part of a larger chain that derives gravity from a discrete ledger of recognition events. The stencil is a local approximation to the Regge action, which is a discretization of general relativity. The scaling law ensures that the approximation behaves correctly under rescalings, a necessary condition for the correspondence to be meaningful. The framework proves this algebra unconditionally, but it does not claim that the stencil is the only possible discretization, nor that the physical bridge from recognition to gravity is complete.

What the declaration does not claim is equally important. It does not assert that the legacy stencil is wrong in all contexts; it only shows that the two stencils cannot both satisfy the same local correspondence unless they are identical. It does not claim that the corrected gate is closed for all grid sizes; that remains an open target. And it does not claim that the stencil itself is a physical observable, only that it is the correct quadratic approximation under the framework's assumptions.

THEOREM periodicEdgeStencilDirichletAction_smul · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
periodicEdgeStencilDirichletAction_smul · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:150 
/-- Quadratic homogeneity transfers to the legacy edge stencil through the
proved identification with the canonical Dirichlet energy. -/
theorem periodicEdgeStencilDirichletAction_smul
    (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
    (a : ℝ)
    (ξ : VertexPotential
      (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K) :
    periodicEdgeStencilDirichletAction
        (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz) (a • ξ) =
      a ^ (2 : ℕ) *
        periodicEdgeStencilDirichletAction
          (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz) ξ := by
  rw [← canonicalPeriodicEdgeStencilTarget Nx Ny Nz hx hy hz (a • ξ),
    ← canonicalPeriodicEdgeStencilTarget Nx Ny Nz hx hy hz ξ]
  exact canonicalDirichletEnergy_smul
    (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K
    (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).hK a ξ
THEOREM canonicalPeriodicMixedAxisStencilAction_smul · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean
canonicalPeriodicMixedAxisStencilAction_smul · IndisputableMonolith/Gravity/Track1BCorrectedQuadratic.lean:132 
/-- The axis stencil is exactly quadratically homogeneous. -/
theorem canonicalPeriodicMixedAxisStencilAction_smul
    (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
    (a : ℝ)
    (ξ : VertexPotential
      (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K) :
    canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz (a • ξ) =
      a ^ (2 : ℕ) * canonicalPeriodicMixedAxisStencilAction Nx Ny Nz hx hy hz ξ := by
  unfold canonicalPeriodicMixedAxisStencilAction
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun base _ => ?_
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun d _ => ?_
  dsimp only
  simp only [Pi.smul_apply, smul_eq_mul]
  ring
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 legacy stencil is wrong in all contexts. The corrected gate is closed for all grid sizes. The stencil itself is a physical observable.

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