changed name

1 files changed, 0 insertions, 513 deletions

diff --git a/proof.norg b/proof.norg
deleted file mode 100644
index 7bd9e25..0000000
--- a/proof.norg
+++ /dev/null
@@ -1,513 +0,0 @@
-@document.meta
-title: proof
-description: 
-authors: ericmarin
-categories: research
-created: 2026-03-16T11:34:52
-updated: 2026-03-28T17:37:48
-version: 1.1.1
-@end
-
-* Soundness Proof
-** Mathematical Definitions
-	 - $Linear(x, q, r) ~ out => out = q*x + r$
-	 - $Concrete(k) ~ out => out = k$
-	 - $Add(out, b) ~ a => out = a + b$
-	 - $AddCheckLinear(out, x, q, r) ~ b => out = q*x + (r + b)$
-	 - $AddCheckConcrete(out, k) ~ b => out = k + b$
-	 - $Mul(out, b) ~ a => out = a * b$
-	 - $MulCheckLinear(out, x, q, r) ~ b => out = q*b*x + r*b$
-	 - $MulCheckConcrete(out, k) ~ b => out = k*b$
-	 - $ReLU(out) ~ x => out = IF (x > 0) THEN x ELSE 0$
-	 - $Materialize(out) ~ x => out = x$
-
-** Soundness of Translation
-*** ReLU
-		ONNX ReLU node is defined as:
-		$Y = X if X > 0 else 0$
-
-		The translation defines the interactions:
-		$x_i ~ ReLU(y_i)$
-
-		By definition this interaction is equal to:
-		$y_i = IF (x_i > 0) THEN x_i ELSE 0$
-
-*** Gemm
-		ONNX Gemm node is defined as:
-		$Y = alpha * A * B + beta * C$
-
-		The translation defines the interactions:
-		$a_i ~ Mul(v_i, Concrete(alpha * b_i))$
-		$Add(...(Add(y_i, v_1), ...), v_n) ~ Concrete(beta * c_i)$
-
-		By definition this interaction is equal to:
-		$v_i = alpha * a_i * b_i$
-		$y_i = v_1 + v_2 + ... + v_n + beta * c_i$
-
-		By grouping the operations we get:
-		$Y = alpha * A * B + beta * C$
-
-*** Flatten
-		Just identity mapping because the wires are always Flatten.
-		$o_i ~ i_i$
-
-*** MatMul
-		Equal to Gemm with $alpha=1$, $beta=0$ and $C=0$.
-
-*** Reshape
-		Just identity mapping because the wires always Flatten.
-		$o_i ~ i_i$
-
-*** Add
-		ONNX Add node is defined as:
-		$C = A + B$
-
-		The translation defines the interactions:
-		$Add(c_i, b_i) ~ a_i$
-
-		By definition this interaction is equal to:
-		$c_i = a_i + b_i$
-
-		By grouping the operations we get:
-		$C = A + B$
-
-*** Sub
-		ONNX Sub node is defined as:
-		$C = A - B$
-
-		The translation defines the interactions:
-		$Add(c_i, neg_b_i) ~ a_i$
-		$Mul(neg_b_i, Concrete(-1)) ~ b_i$
-
-		By definition this interaction is equal to:
-		$c_i = a_i + neg_b_i$
-		$neg_b_i = -1 * b_i$
-
-		By grouping the operations we get:
-		$C = A - B$
-
-** Soundness of Interaction Rules
-*** Materialize
-		The Materialize agent transforms a Linear agent into a tree of explicit mathematical operations
-		that are used as final representation for the solver.
-		In the Python module the terms are defined as:
-		@code python
-		def TermAdd(a, b):
-			return a + b  
-		def TermMul(a, b):
-			return a * b
-		def TermReLU(x):
-			return z3.If(x > 0, x, 0)
-	@end
-**** $Linear(x, q, r) >< Materialize(out) => (1), (2), (3), (4), (5)$
-		 LHS:
-		 $Linear(x, q, r) ~ wire$
-		 $Materialize(out) ~ wire$
-		 $q*x + r = wire$
-		 $out = wire$
-		 $out = q*x + r$
-
-		 $$ Case 1: $q = 0 => out ~ Concrete(r), x ~ Eraser$
-		 RHS:
-		 $out = r$
-
-		 EQUIVALENCE:
-		 $0*x + r = r => r = r$
-		 $$
-
-		 $$ Case 2: $q = 1, r = 0 => out ~ x$
-		 RHS:
-		 $x = out$
-		 $out = x$
-
-		 EQUIVALENCE:
-		 $1*x + 0 = x => x = x$
-		 $$
-
-		 $$ Case 3: $q = 1 => out ~ TermAdd(x, Concrete(r))$
-		 RHS:
-		 $out = x + r$
-
-		 EQUIVALENCE:
-		 $1*x + r = x + r => x + r = x + r$
-		 $$
-
-		 $$ Case 4: $r = 0 => out ~ TermMul(Concrete(q), x)$
-		 RHS:
-		 $out = q*x$
-
-		 EQUIVALENCE:
-		 $q*x + 0 = q*x => q*x = q*x$
-		 $$
-
-		 $$ Case 5: $otherwise => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r))$
-		 RHS:
-		 $out = q*x + r$
-
-		 EQUIVALENCE:
-		 $q*x + r = q*x + r$
-		 $$
-
-**** $Concrete(k) >< Materialize(out) => out ~ Concrete(k)$
-		 LHS:
-		 $Concrete(k) ~ wire$
-		 $Materialize(out) ~ wire$
-		 $k = wire$
-		 $out = wire$
-		 $out = k$
-
-		 RHS:
-		 $out = k$
-
-		 EQUIVALENCE:
-		 $k = k$
-
-*** Add
-**** $Linear(x, q, r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r)$
-		 LHS:
-		 $Linear(x, q, r) ~ wire$
-		 $Add(out, b) ~ wire$
-		 $q*x + r = wire$
-		 $out = wire + b$
-		 $out = q*x + r + b$
-
-		 RHS:
-		 $out = q*x + (r + b)$
-
-		 EQUIVALENCE:
-		 $q*x + r + b = q*x + (r + b) => q*x + (r + b) = q*x + (r + b)$
-
-**** $Concrete(k) >< Add(out, b) => (1), (2)$
-		 LHS:
-		 $Concrete(k) ~ wire$
-		 $Add(out, b) ~ wire$
-		 $k = wire$
-		 $out = wire + b$
-		 $out = k + b$
-
-		 $$ Case 1: $k = 0 => out ~ b$
-		 RHS:
-		 $out = b$
-
-		 EQUIVALENCE:
-		 $0 + b = b => b = b$
-		 $$
-
-		 $$ Case 2: $otherwise => b ~ AddCheckConcrete(out, k)$
-		 RHS:
-		 $out = k + b$
-
-		 EQUIVALENCE:
-		 $k + b = k + b$
-		 $$
-
-**** $Linear(y, s, t) >< AddCheckLinear(out, x, q, r) => (1), (2), (3), (4)$
-		 LHS:
-		 $Linear(y, s, t) ~ wire$
-		 $AddCheckLinear(out, x, q, r) ~ wire$
-		 $s*y + t = wire$
-		 $out = q*x + (r + wire)$
-		 $out = q*x + (r + s*y + t)$
-
-		 $$ Case 1: $q,r,s,t = 0 => out ~ Concrete(0), x ~ Eraser, y ~ Eraser$
-		 RHS:
-		 $out = 0$
-
-		 EQUIVALENCE:
-		 $0*x + (0 + 0*y + 0) = 0 => 0 = 0$
-		 $$
-
-		 $$ Case 2: $s,t = 0 => out ~ Linear(x, q, r), y ~ Eraser$
-		 RHS:
-		 $out = q*x + r$
-
-		 EQUIVALENCE:
-		 $q*x + (r + 0*y + 0) = q*x + r => q*x + r = q*x + r$
-		 $$
-
-		 $$ Case 3: $q, r = 0 => out ~ Linear(y, s, t), x ~ Eraser$
-		 RHS:
-		 $out = s*y + t$
-
-		 EQUIVALENCE:
-		 $0*x + (0 + s*y + t) = s*y + t => s*y + t = s*y + t$
-		 $$
-
-		 $$ Case 4: $otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0)$
-		 RHS:
-		 $Linear(x, q, r) ~ wire1$
-		 $Materialize(out_x) ~ wire1$
-		 $q*x + r = wire1$
-		 $out_x = wire1$
-		 $Linear(y, s, t) ~ wire2$
-		 $Materialize(out_y) ~ wire2$
-		 $s*y + t = wire2$
-		 $out_y = wire2$
-		 $out = 1*TermAdd(out_x, out_y) + 0$
-		 Because $TermAdd(a, b)$ is defined as "a+b$:
-		 $out = 1*(q*x + r + s*y + t) + 0$
-
-		 EQUIVALENCE:
-		 $q*x + (r + s*y + t) = 1*(q*x + r + s*y + t) + 0 => q*x + r + s*y + t = q*x + r + s*y + t
-		 $$
-
-**** $Concrete(j) >< AddCheckLinear(out, x, q, r) => out ~ Linear(x, q, r + j)$
-		 LHS:
-		 $Concrete(j) ~ wire$
-		 $AddCheckLinear(out, x, q, r) ~ wire$
-		 $j = wire$
-		 $out = q*x + (r + wire)$
-		 $out = q*x + (r + j)$
-
-		 RHS:
-		 $out = q*x + (r + j)$
-
-		 EQUIVALENCE:
-		 $q*x + (r + j) = q*x + (r + j)$
-
-**** $Linear(y, s, t) >< AddCheckConcrete(out, k) => out ~ Linear(y, s, t + k)$
-		 LHS:
-		 $Linear(y, s, t) ~ wire$
-		 $AddCheckConcrete(out, k) ~ wire$
-		 $s*y + t = wire$
-		 $out = k + wire$
-		 $out = k + s*y + t$
-
-		 RHS:
-		 $out = s*y + (t + k)$
-
-		 EQUIVALENCE:
-		 $k + s*y + t = s*y + (t + k) => s*y + (t + k) = s*y + (t + k)$
-
-**** $Concrete(j) >< AddCheckConcrete(out, k) => (1), (2)$
-		 LHS:
-		 $Concrete(j) ~ wire$
-		 $AddCheckConcrete(out, k) ~ wire$
-		 $j = wire$
-		 $out = k + wire$
-		 $out = k + j$
-
-		 $$ Case 1: $j = 0 => out ~ Concrete(k)$
-		 RHS:
-		 $out = k$
-
-		 EQUIVALENCE:
-		 $k + 0 = k => k = k$
-		 $$
-
-		 $$ Case 2: $otherwise => out ~ Concrete(k + j)$
-		 RHS:
-		 $out = k + j$
-
-		 EQUIVALENCE:
-		 $k + j = k + j$
-		 $$
-
-*** Mul
-**** $Linear(x, q, r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r)$
-		 LHS:
-		 $Linear(x, q, r) ~ wire$
-		 $Mul(out, b) ~ wire$
-		 $q*x + r = wire$
-		 $out = wire * b$
-		 $out = (q*x + r) * b$
-
-		 RHS:
-		 $out = q*b*x + r*b$
-
-		 EQUIVALENCE:
-		 $(q*x + r) * b = q*b*x + r*b => q*b*x + r*b = q*b*x + r*b$
-
-**** $Concrete(k) >< Mul(out, b) => (1), (2), (3)$
-		 LHS:
-		 $Concrete(k) ~ wire$
-		 $Mul(out, b) ~ wire$
-		 $k = wire$
-		 $out = wire * b$
-		 $out = k * b$
-
-		 $$ Case 1: $k = 0 => out ~ Concrete(0), b ~ Eraser$
-		 RHS:
-		 $out = 0$
-
-		 EQUIVALENCE:
-		 $0 * b = 0 => 0 = 0$
-		 $$
-
-		 $$ Case 2: $k = 1 => out ~ b$
-		 RHS:
-		 $out = b$
-
-		 EQUIVALENCE:
-		 $1 * b = b => b = b$
-		 $$
-
-		 $$ Case 3: $otherwise => b ~ MulCheckConcrete(out, k)$
-		 RHS:
-		 $out = k * b$
-
-		 EQUIVALENCE:
-		 $k * b = k * b$
-		 $$
-
-**** $Linear(y, s, t) >< MulCheckLinear(out, x, q, r) => (1), (2)$
-		 LHS:
-		 $Linear(y, s, t) ~ wire$
-		 $MulCheckLinear(out, x, q, r) ~ wire$
-		 $s*y + t = wire$
-		 $out = q*wire*x + r*wire$
-		 $out = q*(s*y + t)*x + r*(s*y + t)$
-
-		 $$ Case 1: $(q,r = 0) or (s,t = 0) => x ~ Eraser, y ~ Eraser, out ~ Concrete(0)$
-		 RHS:
-		 $out = 0$
-
-		 EQUIVALENCE:
-		 $0*(s*y + t)*x + 0*(s*y + t) = 0 => 0 = 0$
-		 or
-		 $q*(0*y + 0)*x + r*(0*y + 0) = 0 => 0 = 0$
-		 $$
-
-		 $$ Case 2: $otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0)$
-		 RHS:
-		 $Linear(x, q, r) ~ wire1$
-		 $Materialize(out_x) ~ wire1$
-		 $q*x + r = wire1$
-		 $out_x = wire1$
-		 $Linear(y, s, t) ~ wire2$
-		 $Materialize(out_y) ~ wire2$
-		 $s*y + t = wire2$
-		 $out_y = wire2$
-		 $out = 1*TermMul(out_x, out_y) + 0$
-		 Because $TermMul(a, b)$ is defined as $a*b$:
-		 $out = 1*(q*x + r)*(s*y + t) + 0$
-
-		 EQUIVALENCE:
-		 $q*(s*y + t)*x + r*(s*y + t) = 1*(q*x + r)*(s*y + t) => 
-		 q*(s*y + t)*x + r*(s*y + t) = (q*x + r)*(s*y + t) => 
-		 q*(s*y + t)*x + r*(s*y + t) = q*(s*y + t)*x + r*(s*y + t)$
-		 $$
-
-**** $Concrete(j) >< MulCheckLinear(out, x, q, r) => out ~ Linear(x, q * j, r * j)$
-		 LHS:
-		 $Concrete(j) ~ wire$
-		 $MulCheckLinear(out, x, q, r) ~ wire$
-		 $j = wire$
-		 $out = q*wire*x + r*wire$
-		 $out = q*j*x + r*j$
-
-		 RHS:
-		 $out = q*j*x + r*j$
-
-		 EQUIVALENCE:
-		 $q*j*x + r*j = q*j*x + r*j$
-
-**** $Linear(y, s, t) >< MulCheckConcrete(out, k) => out ~ Linear(y, s * k, t * k)$
-		 LHS:
-		 $Linear(y, s, t) ~ wire$
-		 $MulCheckConcrete(out, k) ~ wire$
-		 $s*y + t = wire$
-		 $out = k * wire$
-		 $out = k * (s*y + t)$
-
-		 RHS:
-		 $out = s*k*y + t*k$
-
-		 EQUIVALENCE:
-		 $k * (s*y + t) = s*k*y + t*k => s*k*y + t*k = s*k*y + t*k$
-
-**** $Concrete(j) >< MulCheckConcrete(out, k) => (1), (2), (3)$
-		 LHS:
-		 $Concrete(j) ~ wire$
-		 $MulCheckConcrete(out, k) ~ wire$
-		 $j = wire$
-		 $out = k * wire$
-		 $out = k * j$
-
-		 $$ Case 1: $j = 0 => out ~ Concrete(0)$
-		 RHS:
-		 $out = 0$
-
-		 EQUIVALENCE:
-		 $k * 0 = 0 => 0 = 0$
-		 $$
-
-		 $$ Case 2: $j = 1 => out ~ Concrete(k)$
-		 RHS:
-		 $out = k$
-
-		 EQUIVALENCE:
-		 $k * 1 = k => k = k$
-		 $$
-
-		 $$ Case 3: $otherwise => out ~ Concrete(k * j)$
-		 RHS:
-		 $out = k * j$
-
-		 EQUIVALENCE:
-		 $k * j = k * j$
-
-*** ReLU
-**** $Linear(x, q, r) >< ReLU(out) => Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0)$
-		 LHS:
-		 $Linear(x, q, r) ~ wire$
-		 $ReLU(out) ~ wire$
-		 $q*x + r = wire$
-		 $out = IF wire > 0 THEN wire ELSE 0$
-		 $out = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0$
-
-		 RHS:
-		 $Linear(x, q, r) ~ wire$
-		 $Materialize(out_x) ~ wire$
-		 $q*x + r = wire$
-		 $out_x = wire$
-		 $out = 1*TermReLU(out_x) + 0$
-		 Because $TermReLU(x)$ is defined as $z3.If(x > 0, x, 0)$:
-		 $out = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0$
-
-		 EQUIVALENCE:
-		 $IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0 =>
-		 IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0$
-
-**** $Concrete(k) >< ReLU(out) => (1), (2)$
-		 LHS:
-		 $Concrete(k) ~ wire$
-		 $ReLU(out) ~ wire$
-		 $k = wire$
-		 $out = IF wire > 0 THEN wire ELSE 0$
-		 $out = IF k > 0 THEN k ELSE 0$
-
-		 $$ Case 1: $k > 0 => out ~ Concrete(k)$
-		 RHS:
-		 $out = k$
-
-		 EQUIVALENCE:
-		 $IF true THEN k ELSE 0 = k => k = k$
-		 $$
-
-		 $$ Case 2: $k <= 0 => out ~ Concrete(0)$
-		 RHS:
-		 $out = 0$
-
-		 EQUIVALENCE:
-		 $IF false THEN k ELSE 0 = 0 => 0 = 0$
-		 $$
-
-** Soundness of Reduction
-	 Let $IN_0$ be the Interaction Net translated from a Neural Network $NN$. Let $IN_n$ be the state of the net
-	 after $n$ reduction steps. Then $\forall n \in N$, $[IN_n] = [NN]$.
-
-*** Proof by Induction
-		- Base Case ($n = 0$): By the {* Soundness of Translation}, the initial net $IN_0$ is constructed such that
-			its semantics $[IN_0]$ exactly match the mathematical definition of the ONNX nodes in $NN$.
-		- Induction Step ($n -> n + 1$): Assume $[IN_n] = [NN]$. If $IN_n$ is in normal form, the proof is complete.
-			Otherwise, there exists an active pair $A$ that reduces $IN_n$ to $IN_{n+1}$.
-			By the {* Soundness of Interaction Rules}, the mathematical definition is preserved after any reduction step,
-		it follows that $[IN_{n+1}] = [IN_n]$. By the inductive hypothesis, $[IN_{n+1}] = [NN]$.
-		---
-
-	 By the principle of mathematical induction, the Interaction Net remains semantically equivalent to the original 
-	 Neural Network at every step of the reduction process.
-
-	 Since Interaction Nets are confluent, the reduced mathematical expression is unique regardless
-	 of order in which rules are applied.