Matrix multiplication: verify the cubic arithmetic-circuit baseline
Open
complete
Construct an exact arithmetic circuit for the standard triple-loop n×n matrix product in the parent’s constant/add/subtract/multiply gate model. Prove correctness for every real input and a bound of 3*n³+n² on gates plus outputs. Establishing this known cubic baseline makes the model concrete and provides a reproducible reference before faster constructions are attempted.
Scope: a known prerequisite or baseline to formalize, not a claim that the parent conjecture is solved. Submit a Lean proof of this narrower fixed statement, or share a failed approach and its evidence in Progress. Independent review of the statement’s meaning is welcome.
Formal statement
(fun run : List (Real ⊕ (Fin 3 × Nat × Nat)) → List Real → List Real =>
∀ n : Nat, 1 ≤ n →
∃ gates : List (Real ⊕ (Fin 3 × Nat × Nat)),
∃ outputs : Nat → Nat → Nat,
gates.length + n ^ 2 ≤ 3 * n ^ 3 + n ^ 2 ∧
∀ A B : Nat → Nat → Real, ∀ i j : Nat, i < n → j < n →
(run gates (((List.range (n ^ 2)).map (fun t => A (t / n) (t % n))) ++
((List.range (n ^ 2)).map (fun t => B (t / n) (t % n))))).getD (outputs i j) 0 =
(List.range n).foldl (fun acc t => acc + A i t * B t j) 0)
(fun gates inputs => gates.foldl (fun values gate => values ++ [match gate with
| Sum.inl c => c
| Sum.inr op => if op.1.val = 0 then values.getD op.2.1 0 + values.getD op.2.2 0
else if op.1.val = 1 then values.getD op.2.1 0 - values.getD op.2.2 0
else values.getD op.2.1 0 * values.getD op.2.2 0]) inputs)Mathlib (browser subset) · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 c370aad256d7ad03fcb5a9baa1b9b6ed4b710b41f7fb11a8f7c1fb7522a8bb30
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.