Local rational definitions and their uses

Conservative local notation

Six capture-safe rational templates, with explicit nonzero denominators. No new kernel symbol or axiom; no global registry change. These are local expansions, not Alpha/Stable admissions. Arrows below are definition-expansion dependencies, not theorem proofs.

Reused signed-square notation

The signed norm bridge reuses the existing ND0157 — SignedDifferenceSquare, with the same reviewed expansion and identity. It is not a seventh new rational definition. Open the checked signed quadratic-norm zero criterion.

Quadratic-integer components

ND0388 — IQuadProductReal and ND0389 — IQuadProductRadical are two separate primitive balance equations, without hidden norm claims. The checked multiplicativity theorem uses both and the exact ND0157 square definition. These two aliases are local and unpromoted.

Finite convolution

Eight historical table, order, and summation definitions are reused with the same identities and argument order. CV001 proves a universal vanishing statement for the actual natural diagonal execution, not a rational exp-composition theorem.

Rational quadratic norms

RN001: norm independence from representatives and denominators and RN002: denominator-aware norm multiplication reuse IRatEq, IRatMul and the existing signed-square and coordinate definitions without adding a new alias or axiom. Real interpretation and analytic separation remain open.

Nonzero quadratic products

QN001: products of two nonzero signed quadratic integers are nonzero uses the actual norm and signed-integer proof bodies, with no canonical-representative restriction.

QF001: finite product traces preserve nonvanishing adds genuine induction over decoded tables. Four conservative trace definitions keep executed multiplication separate from the nonzero-factor assumption. Existence of traces and interpretation in the real numbers remain open.

Navigate the checked arithmetic DAG and its open planning parents. Proof dependencies and definition-use links are kept distinct.

Theorems using this notation

• RF001 — Reflexive
• RF002 — Symmetric
• RF003 — Transitive
• RF004 — Scale nonzero
• RF005 — Numerator shift
• RF006 — Negation compatible

Checked results · IR001 planning cone · Exact definition DAG data.

ND0382 — IRatValid

Parameters: p, m, d. No definition prerequisite.

¬d = 0

ND0383 — IRatEq

Parameters: p, m, d, P, M, D. IRatValid.

¬d = 0 ∧ (¬D = 0 ∧ p · D + M · d = m · D + P · d)

ND0384 — IRatAdd

Parameters: p, m, d, q, n, e, r, s, f. IRatValid · IRatEq.

¬d = 0 ∧ (¬e = 0 ∧ (¬f = 0 ∧ (¬d · e = 0 ∧ r · (d · e) + (m · e + n · d) · f = s · (d · e) + (p · e + q · d) · f)))

ND0385 — IRatMul

Parameters: p, m, d, q, n, e, r, s, f. IRatValid · IRatEq.

¬d = 0 ∧ (¬e = 0 ∧ (¬f = 0 ∧ (¬d · e = 0 ∧ r · (d · e) + (p · n + m · q) · f = s · (d · e) + (p · q + m · n) · f)))

ND0386 — IRatNeg

Parameters: p, m, d, r, s, f. IRatValid · IRatEq.

¬d = 0 ∧ (¬f = 0 ∧ (¬d = 0 ∧ r · d + p · f = s · d + m · f))

ND0387 — IRatLt

Parameters: p, m, d, P, M, D. IRatValid.

¬d = 0 ∧ (¬D = 0 ∧ (∃ x. p · D + M · d + S x = m · D + P · d))