Gravity Cubic Regge Convergence Uv Cutoff Pos

The ultraviolet cutoff

The declaration uv_cutoff_pos is a small, machine-checked theorem in the framework's library of formal theorems. It states that the ultraviolet cutoff wavenumber, defined as π/4, is greater than zero. In plain language, this means the shortest wavelength that the framework's cubic lattice can resolve is a positive, finite number, not zero and not negative. It is a basic sanity condition: a resolution limit that is zero would be no limit at all, and a negative one would be meaningless.

The context for this statement is the framework's model of gravity on a cubic lattice, a discrete grid of points with a fixed spacing. The framework identifies a natural periodicity of eight ticks, and from that periodicity derives a minimum resolvable wavelength of eight times the fundamental voxel length. The wavenumber corresponding to that wavelength is π divided by four times the voxel length, and the theorem uv_cutoff_pos establishes that this number is positive. The proof is immediate: it unfolds the definition and applies the positivity tactic, which is a standard automated step.

The theorem is a component of a larger certificate that combines several structural advantages of the cubic lattice for proving convergence of a discrete action to a continuum one. The certificate records that the shape quality is perfect, that the ultraviolet cutoff is positive, that the golden ratio is greater than one, and that a weak-field error estimate holds. The positive cutoff is one of the four conditions, and it is the one that addresses the problem of ultraviolet divergences, which are infinite results that plague continuum quantum gravity.

The theorem does not claim that the cutoff is derived from first principles within the framework. The value π/4 is introduced as a definition, not proved. The theorem only proves a property of that definition: its positivity. It also does not claim that the cutoff prevents all divergences in all models; it is a statement about a single constant, not a proof of finiteness for any physical quantity. The theorem is a necessary condition, not a sufficient one, for a well-behaved lattice theory.

What the theorem does establish is that the framework's lattice has a built-in, positive resolution limit. This is the kind of fact that must be true for any discrete model of spacetime that aims to be physically sensible. It is a small but load-bearing piece of the framework's claim that its lattice provides a natural, physical cutoff rather than an artificial one. The reader can now see that the framework takes the problem of infinities seriously enough to state and prove even the most basic positivity condition.

/-- The cutoff is positive. -/
theorem uv_cutoff_pos : 0 < uv_cutoff := by
  unfold uv_cutoff
  positivity

theorem cubic_convergence_cert : CubicConvergenceCert where
  shape_quality_free := rs_cubic_shape_quality
  uv_cutoff_exists := uv_cutoff_pos
  phi_growth := phi_exponential_growth
  weak_field_unconditional := weak_field_error_estimate

What this page does not claim

The theorem does not derive the value π/4 from more fundamental principles; it is a definitional choice. The theorem does not prove that the cutoff prevents all ultraviolet divergences in the framework's gravity model. The theorem does not establish that the lattice model is physically correct, only that one of its constants is positive.

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/CubicReggeConvergence.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: