CLASS.EQUATION

Navigation:

On this page:

  • Artifacts #
  • Interactive demo #
Summary

BOUNDED CUBIC UNIVERSAL DIOPHANTINES

We present two concrete cubic Diophantine equations (degree-3 polynomials over $\mathbb{N}$) whose satisfiability effectively recovers constructive theoremhood.

Key materials:

  • Main Paper arXiv
  • Repository T002 (Proof System & Reduction in Rocq) GitHub
  • Repository T003 (Universal Cubic in Rocq) GitHub
  • Repository T004 (Bridge in Rocq) GitHub
  • Carryless Pairing .html

Secondary literature and prerequisites:

  • Jones: Universal Diophantine Equation (1982) DOI
  • Matiyasevich: Hilbert's Tenth Problem (Book) DOI
  • Gasarch: Hilbert's Tenth Problem (2021) arXiv
  • Boolos, Burgess, Jeffrey: Computability and Logic (Book) DOI

We recall the MRDP Theorem, the Universal Diophantine Equation of Jones, and the degree hierarchy of Diophantine equations over $\mathbb{N}$, as codified in the study of Hilbert's Tenth Problem.

Operational summary: each artifact below is a published degree-3 polynomial whose bounded satisfiability can be checked directly from its coefficient table.

  • Degree 2. Certain structured quadratic forms are decidable via classical number-theoretic methods (Hasse–Minkowski, Lagrange). Degree-2 constraints lack the expressive power to encode arbitrary proof checking.
  • Degree 4. Every recursively enumerable set is the solution set of a degree-4 Diophantine equation in 58 variables. Undecidability follows classically from MRDP.
  • Degree 3. The open case, identified by Jones (1980), cf. “Secondary Literature” on this page.

The artifacts shown here are computable witnesses rather than classic existence claims. Their coefficients are published, their degrees can be directly examined, and their bounded satisfaction predicates are decidable by finite search. The constructions are strictly more informative: where tradition asserts that some polynomial encodes all recursively enumerable sets, the effective construction demonstrates this.

We start with simple resource parameters signifying the number of lines, the digit width, and the base:

$$\mathtt{k,digit\_width,base}$$

A generator in $\mathsf{Python}$ emits one concrete cubic coefficient table $U_{k,w}$ and establishes bounded proof-check satisfiability:

$$\mathsf{BoundedThm}_{k,w}(u) \;\Longleftrightarrow\; \exists\, \vec{x} \in \mathbb{N}^{m(k,w)}\; U_{k,w}(\vec{x}) = 0.$$

Analogy. We imagine a polynomial as a command-line interface (without a monitor). We can define a query and feed it into its variables. The equation evaluates to 'zero' if the encoded statement is true, and to a nonzero value otherwise. The polynomial itself is fixed; only the input changes.

Realization proceeds in layers.

Given a weak arithmetic we define as Register Arithmetic or $\mathsf{RA}$, situating its comprehension (with extensional multiplication) between Robinson Arithmetic ($\mathsf{Q}$) and Peano Arithmetic $(\mathsf{PA})$:

$$\mathsf{Q} \;\leq_{\mathrm{int}}\; \mathsf{RA}+\mathtt{Mult} \;\leq_{\mathrm{int}}\; \mathsf{EFA} \;<\; \mathsf{PA} \lor \mathsf{HA}.$$

(ii) Compilation. A primitive recursive map

$$\varphi \longmapsto \mathcal{S}_\varphi$$

takes sentence codes to finite systems of degree-3 Diophantine equations, such that

$$\mathrm{Prov}_{\mathsf{RA}}(\ulcorner\varphi\urcorner) \;\Longleftrightarrow\; \mathsf{CubicSat}(\ulcorner \mathcal{S}_\varphi \urcorner).$$

(iii) Constraining. Syntactic and inference checks compile to quadratic constraints (degree-2). Cubic terms arise only when a degree-1 selector variable activates a quadratic obligation. The resulting system is collapsed to a single cubic equation by mixed-radix aggregation, avoiding the sum-of-squares degree doubling that would otherwise raise degree to 6.

(iv) Metatheory. Each fixed bounded slice is decidable, yet no total correct uniform decider for the compiled family exists. By the Diagonal Lemma, such a decider would compose with the compiler to decide theoremhood: contradiction. If $\mathsf{RA}$ could internally certify such a decider, it would witness its own $\Sigma_1$-reflection, contradicting Gödel's Second Incompleteness Theorem, hence ad absurdum.

Download

Both Diophantine polynomials are generated by the same compiler with different parameter choices and have total degree exactly 3. They differ by resource bounds and aggregation scale. Each is decidable, recursively enumerable, and able to validate bounded proofs according to its pinned parameters. We introduce two flavors:

Effective ($\mathsf{imp},\bot,\mathsf{EFQ}$)

  • Bounded universal, single proof line (k = 1), digit width 36
  • Radix base 6,000,001 | 13,545 variables | 4,842 channels | 15,417 monomials | max coefficient 10^1234 |
  • JSON: .json

Minimal ($\mathsf{RE}$)

  • $\mathsf{Rocq}$-formalized, three proof lines (k = 3), digit width 16
  • Radix base 5 | 18 712 variables | 6,675 channels | 21,471 monomials | max coefficient ≈ 10^198 |
  • JSON: .json
  • Rendered equation: .htm
Demo

This demo performs in-browser verification of the published cubic artifact. The coefficient table is loaded locally, structural bounds are checked, and a fixed suite of two provable and two unprovable sentence encodings is validated against the loaded polynomial.

Worker idle.

Step 1. Load a coefficient table. Download one of the JSON artifacts above, or fetch directly.


Step 2. Run structural audits: degree bounds, coefficient digit counts, variable index bounds.

No artifact loaded.

Step 3. Validate four fixed sentence cases (two provable, two unprovable) against the loaded polynomial. The witness environments are sparse encodings drawn from the bounded regime.

$$ \begin{aligned} \mathtt{true\_efq\_bot\_bot} &: \bot \to \bot,\\ \mathtt{true\_k\_bot} &: \bot \to (\bot \to \bot),\\ \mathtt{false\_bot\_goal} &: \bot,\\ \mathtt{false\_trace\_mismatch\_k\_bot} &: u \leftarrow u+1. \end{aligned} $$

The suite is explicit: two theorem witnesses are checked as positive cases (expected zero), and two negative controls are checked as expected nonzero. One negative case sets the target to $\bot$ (bottom/false); the other keeps theorem data fixed and mutates the public trace code by +1.

Sentence suite not run yet.

Note. We restrict ourselves to equations no more sophisticated than those above, but in principle, we should see no obstructions.

Legend
1Navigation
3Materials and References
2Introduction and Construction
4Equation Artifact
5JS Check (Audit + Sentence Suite)