Finite execution · Conservative definition DAG

Quadratic product trace definitions

Execution and mathematical hypotheses stay separate

Four new local aliases describe decoded coordinates, actual multiplication steps, a trace starting at one, and its separate nonzero-factor hypothesis. The trace does not assume that its outputs are nonzero. Every finite step includes actual decoding witnesses; no table-existence theorem is silently assumed.

Exact checked induction theorem · Definition network · Checked arithmetic DAG · Typed expansion DAG.

Conservative expansion DAG

Arrows run from an unchanged prerequisite to the definition using it. They are notation dependencies, not proof certificates.

BetaAt is used by IQuadAtIQuadAt is used by IQuadProductStepIQuadProductReal is used by IQuadProductStepIQuadProductRadical is used by IQuadProductStepIQuadAt is used by IQuadProductTraceLt is used by IQuadProductTraceIQuadProductStep is used by IQuadProductTraceLt is used by IQuadNonzeroFactorsIQuadAt is used by IQuadNonzeroFactorsPD0002LtPD0013BetaAtND0388IQuadProductRealND0389IQuadProductRadicalND0390IQuadAtND0391IQuadProductStepND0392IQuadProductTraceND0393IQuadNonzeroFactors

PD0002 — Lt

Existing definition, unchanged. Parameters: a, b.

Witness-defined strict order on natural numbers.

No definition prerequisite

exists h. h + S a = b
Exact expanded HA definition
exists h. h + S a = b

PD0013 — BetaAt

Existing definition, unchanged. Parameters: b, c, i, x.

x is the bounded beta-decoded value at index i.

No definition prerequisite

((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\
  exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))
Exact expanded HA definition
((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))

ND0388 — IQuadProductReal

Existing definition, unchanged. Parameters: ap, an, bp, bn, cp, cn, dp, dn, rp, rn.

The signed pair rp,rn represents the real component AC+2BD of (A+B sqrt(2))(C+D sqrt(2)).

No definition prerequisite

rp + (ap · cn + an · cp + 2 · (bp · dn + bn · dp)) = ap · cp + an · cn + 2 · (bp · dp + bn · dn) + rn
Exact expanded HA definition
rp + (ap · cn + an · cp + 2 · (bp · dn + bn · dp)) = ap · cp + an · cn + 2 · (bp · dp + bn · dn) + rn

ND0389 — IQuadProductRadical

Existing definition, unchanged. Parameters: ap, an, bp, bn, cp, cn, dp, dn, sp, sn.

The signed pair sp,sn represents the radical component AD+BC of (A+B sqrt(2))(C+D sqrt(2)).

No definition prerequisite

sp + (ap · dn + an · dp + (bp · cn + bn · cp)) = ap · dp + an · dn + (bp · cp + bn · cn) + sn
Exact expanded HA definition
sp + (ap · dn + an · dp + (bp · cn + bn · cp)) = ap · dp + an · dn + (bp · cp + bn · cn) + sn

ND0390 — IQuadAt

New local conservative alias. Parameters: ab, ac, bb, bc, cb, cc, db, dc, i, ap, an, bp, bn.

Four actual beta-decoded natural components represent one signed quadratic integer.

BetaAt

BetaAt(ab,ac,i,ap) /\
  (BetaAt(bb,bc,i,an) /\
  (BetaAt(cb,cc,i,bp) /\
  BetaAt(db,dc,i,bn)))
Exact expanded HA definition
S ap ≤ S (S i · ac) ∧ (∃ x. ab = x · S (S i · ac) + ap) ∧ (S an ≤ S (S i · bc) ∧ (∃ x. bb = x · S (S i · bc) + an) ∧ (S bp ≤ S (S i · cc) ∧ (∃ x. cb = x · S (S i · cc) + bp) ∧ (S bn ≤ S (S i · dc) ∧ (∃ x. db = x · S (S i · dc) + bn))))

ND0391 — IQuadProductStep

New local conservative alias. Parameters: ab, ac, bb, bc, cb, cc, db, dc, ub, uc, vb, vc, wb, wc, xb, xc, i.

One actual factor/current/successor decoding and both multiplication balances; no nonzero assumption.

IQuadAt · IQuadProductReal · IQuadProductRadical

exists ap an bp bn cp cn dp dn rp rn sp sn. IQuadAt(ab,ac,bb,bc,cb,cc,db,dc,i,cp,cn,dp,dn) /\
  (IQuadAt(ub,uc,vb,vc,wb,wc,xb,xc,i,ap,an,bp,bn) /\
  (IQuadAt(ub,uc,vb,vc,wb,wc,xb,xc,S i,rp,rn,sp,sn) /\
  (IQuadProductReal(ap,an,bp,bn,cp,cn,dp,dn,rp,rn) /\
  IQuadProductRadical(ap,an,bp,bn,cp,cn,dp,dn,sp,sn))))
Exact expanded HA definition
∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ j. ∃ u. ∃ v. ∃ w. ∃ x0. ∃ x1. S m ≤ S (S i · ac) ∧ (∃ x2. ab = x2 · S (S i · ac) + m) ∧ (S k ≤ S (S i · bc) ∧ (∃ x2. bb = x2 · S (S i · bc) + k) ∧ (S j ≤ S (S i · cc) ∧ (∃ x2. cb = x2 · S (S i · cc) + j) ∧ (S u ≤ S (S i · dc) ∧ (∃ x2. db = x2 · S (S i · dc) + u)))) ∧ (S x ≤ S (S i · uc) ∧ (∃ x2. ub = x2 · S (S i · uc) + x) ∧ (S y ≤ S (S i · vc) ∧ (∃ x2. vb = x2 · S (S i · vc) + y) ∧ (S z ≤ S (S i · wc) ∧ (∃ x2. wb = x2 · S (S i · wc) + z) ∧ (S n ≤ S (S i · xc) ∧ (∃ x2. xb = x2 · S (S i · xc) + n)))) ∧ (S v ≤ S (S S i · uc) ∧ (∃ x2. ub = x2 · S (S S i · uc) + v) ∧ (S w ≤ S (S S i · vc) ∧ (∃ x2. vb = x2 · S (S S i · vc) + w) ∧ (S x0 ≤ S (S S i · wc) ∧ (∃ x2. wb = x2 · S (S S i · wc) + x0) ∧ (S x1 ≤ S (S S i · xc) ∧ (∃ x2. xb = x2 · S (S S i · xc) + x1)))) ∧ (v + (x · k + y · m + 2 · (z · u + n · j)) = x · m + y · k + 2 · (z · j + n · u) + w ∧ x0 + (x · u + y · j + (z · k + n · m)) = x · j + y · u + (z · m + n · k) + x1)))

ND0392 — IQuadProductTrace

New local conservative alias. Parameters: ab, ac, bb, bc, cb, cc, db, dc, ub, uc, vb, vc, wb, wc, xb, xc, L.

A supplied length-L multiplication trace starts at one and executes every factor; existence is not assumed.

IQuadAt · Lt · IQuadProductStep

IQuadAt(ub,uc,vb,vc,wb,wc,xb,xc,0,1,0,0,0) /\
  (forall i. Lt(i,L) -> IQuadProductStep(ab,ac,bb,bc,cb,cc,db,dc,ub,uc,vb,vc,wb,wc,xb,xc,i))
Exact expanded HA definition
2 ≤ S (1 · uc) ∧ (∃ x. ub = x · S (1 · uc) + 1) ∧ (1 ≤ S (1 · vc) ∧ (∃ x. vb = x · S (1 · vc) + 0) ∧ (1 ≤ S (1 · wc) ∧ (∃ x. wb = x · S (1 · wc) + 0) ∧ (1 ≤ S (1 · xc) ∧ (∃ x. xb = x · S (1 · xc) + 0)))) ∧ (∀ x. S x ≤ L → ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. ∃ v. ∃ w. ∃ x0. ∃ x1. S k ≤ S (S x · ac) ∧ (∃ x2. ab = x2 · S (S x · ac) + k) ∧ (S i ≤ S (S x · bc) ∧ (∃ x2. bb = x2 · S (S x · bc) + i) ∧ (S j ≤ S (S x · cc) ∧ (∃ x2. cb = x2 · S (S x · cc) + j) ∧ (S u ≤ S (S x · dc) ∧ (∃ x2. db = x2 · S (S x · dc) + u)))) ∧ (S y ≤ S (S x · uc) ∧ (∃ x2. ub = x2 · S (S x · uc) + y) ∧ (S z ≤ S (S x · vc) ∧ (∃ x2. vb = x2 · S (S x · vc) + z) ∧ (S n ≤ S (S x · wc) ∧ (∃ x2. wb = x2 · S (S x · wc) + n) ∧ (S m ≤ S (S x · xc) ∧ (∃ x2. xb = x2 · S (S x · xc) + m)))) ∧ (S v ≤ S (S S x · uc) ∧ (∃ x2. ub = x2 · S (S S x · uc) + v) ∧ (S w ≤ S (S S x · vc) ∧ (∃ x2. vb = x2 · S (S S x · vc) + w) ∧ (S x0 ≤ S (S S x · wc) ∧ (∃ x2. wb = x2 · S (S S x · wc) + x0) ∧ (S x1 ≤ S (S S x · xc) ∧ (∃ x2. xb = x2 · S (S S x · xc) + x1)))) ∧ (v + (y · i + z · k + 2 · (n · u + m · j)) = y · k + z · i + 2 · (n · j + m · u) + w ∧ x0 + (y · u + z · j + (n · i + m · k)) = y · j + z · u + (n · k + m · i) + x1))))

ND0393 — IQuadNonzeroFactors

New local conservative alias. Parameters: ab, ac, bb, bc, cb, cc, db, dc, L.

Every decoded factor below L is represented nonzero; this is a separate premise, not part of the trace.

Lt · IQuadAt

forall i ap an bp bn. Lt(i,L) -> IQuadAt(ab,ac,bb,bc,cb,cc,db,dc,i,ap,an,bp,bn) -> ~(ap=an /\
  bp=bn)
Exact expanded HA definition
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. S x ≤ L → S y ≤ S (S x · ac) ∧ (∃ k. ab = k · S (S x · ac) + y) ∧ (S z ≤ S (S x · bc) ∧ (∃ k. bb = k · S (S x · bc) + z) ∧ (S n ≤ S (S x · cc) ∧ (∃ k. cb = k · S (S x · cc) + n) ∧ (S m ≤ S (S x · dc) ∧ (∃ k. db = k · S (S x · dc) + m)))) → ¬(y = z ∧ n = m)