{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"mathlib","imports":["Mathlib.Data.Real.Basic","Mathlib.Tactic.Ring","Mathlib.Tactic.Linarith","Mathlib.Tactic.NormNum"],"statement_hash":"c370aad256d7ad03fcb5a9baa1b9b6ed4b710b41f7fb11a8f7c1fb7522a8bb30","problem":{"id":20,"title":"Matrix multiplication: verify the cubic arithmetic-circuit baseline","description":"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.\n\nScope: 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.","statement":"(fun run : List (Real ⊕ (Fin 3 × Nat × Nat)) → List Real → List Real =>\n  ∀ n : Nat, 1 ≤ n →\n      ∃ gates : List (Real ⊕ (Fin 3 × Nat × Nat)),\n      ∃ outputs : Nat → Nat → Nat,\n        gates.length + n ^ 2 ≤ 3 * n ^ 3 + n ^ 2 ∧\n        ∀ A B : Nat → Nat → Real, ∀ i j : Nat, i < n → j < n →\n          (run gates (((List.range (n ^ 2)).map (fun t => A (t / n) (t % n))) ++\n                      ((List.range (n ^ 2)).map (fun t => B (t / n) (t % n))))).getD (outputs i j) 0 =\n          (List.range n).foldl (fun acc t => acc + A i t * B t j) 0)\n(fun gates inputs => gates.foldl (fun values gate => values ++ [match gate with\n  | Sum.inl c => c\n  | Sum.inr op => if op.1.val = 0 then values.getD op.2.1 0 + values.getD op.2.2 0\n    else if op.1.val = 1 then values.getD op.2.1 0 - values.getD op.2.2 0\n    else values.getD op.2.1 0 * values.getD op.2.2 0]) inputs)","profile":"mathlib","module_pins":[],"module_context":[],"scope":{}},"source":"import Mathlib.Data.Real.Basic\nimport Mathlib.Tactic.Ring\nimport Mathlib.Tactic.Linarith\nimport Mathlib.Tactic.NormNum\n\ndef OA_statement : Prop := ((fun run : List (Real ⊕ (Fin 3 × Nat × Nat)) → List Real → List Real =>\n  ∀ n : Nat, 1 ≤ n →\n      ∃ gates : List (Real ⊕ (Fin 3 × Nat × Nat)),\n      ∃ outputs : Nat → Nat → Nat,\n        gates.length + n ^ 2 ≤ 3 * n ^ 3 + n ^ 2 ∧\n        ∀ A B : Nat → Nat → Real, ∀ i j : Nat, i < n → j < n →\n          (run gates (((List.range (n ^ 2)).map (fun t => A (t / n) (t % n))) ++\n                      ((List.range (n ^ 2)).map (fun t => B (t / n) (t % n))))).getD (outputs i j) 0 =\n          (List.range n).foldl (fun acc t => acc + A i t * B t j) 0)\n(fun gates inputs => gates.foldl (fun values gate => values ++ [match gate with\n  | Sum.inl c => c\n  | Sum.inr op => if op.1.val = 0 then values.getD op.2.1 0 + values.getD op.2.2 0\n    else if op.1.val = 1 then values.getD op.2.1 0 - values.getD op.2.2 0\n    else values.getD op.2.1 0 * values.getD op.2.2 0]) inputs))\n\n#check OA_statement\n","proof":null}