perf(hex-matrix): Submatrix views for the mulStrassen recursion

[kim-em]

This PR add the Submatrix view type — named after Lean's Subarray/Substring: a base matrix plus row/column offsets and block dimensions, whose entry reads are pure offset arithmetic into the shared flat buffer — and rewire mulStrassen's internal recursion over views, so quadrants stop being materialized copies (the generated C shows zero quadrant-copy allocations; allocation remains only for the operand sums, the seven recursive products, padding, and leaf materialization for the unchanged baseMul signature). mulStrassen_eq_mul is re-proved through view-to-Matrix abstraction lemmas with the algorithm, its statement, and the three named correctness lemmas untouched; the colAdd/colAddRight/colSwap family moves from the materializing mapRows pass to flat per-entry column engines with unchanged public lemma statements; and the SPEC's BlockView mentions are renamed. The re-measured cost model is honestly neutral: the cutoff sweep and scaling series on the view recursion are within noise of the committed flat baseline (0.99–1.01× everywhere — the removed copies are O(n²) per level against O(n^2.81) multiply work, so they never dominated at benched sizes), so strassenDefault.cutoff stays at the measured 96, with the committed exports and overlay figure recording the outcome. Whole-graph and root-invalidated builds green (4160 jobs), conformance green, no sorry/axiom/native_decide. Closes #8652.

🤖 Prepared with Claude Code