doc: record the Array.ofFn call-site audit, and add ofFn' compatibility lemmas

HexBasic/OfFn.lean

@@ -49,6 +49,30 @@ namespace Hex
     Vector.ofFn' f = Vector.ofFn f := by
   simp [Vector.ofFn', _root_.Vector.ofFn]
 
+/-! ## Compatibility lemmas
+
+Core's lemmas (`Array.size_ofFn`, `Vector.getElem_ofFn`, …) are stated about
+`ofFn` and do not apply to `ofFn'`. `ofFn'_eq_ofFn` is `@[simp]`, so ordinary
+`simp` bridges the gap on its own; these exist so that `simp only` proofs and
+`rfl`-closing steps keep working after a definition is migrated, without having
+to thread the equality in by hand. -/
+
+@[simp] theorem Array.size_ofFn' {α : Type u} {n : Nat} (f : Fin n → α) :
+    (Array.ofFn' f).size = n := by
+  simp [Array.ofFn']
+
+@[simp] theorem Array.getElem_ofFn' {α : Type u} {n : Nat} (f : Fin n → α) (i : Nat)
+    (h : i < (Array.ofFn' f).size) :
+    (Array.ofFn' f)[i] = f ⟨i, by simpa using h⟩ := by
+  simp [Array.ofFn']
+
+@[simp] theorem Vector.toArray_ofFn' {n : Nat} {α : Type u} (f : Fin n → α) :
+    (Vector.ofFn' f).toArray = Array.ofFn' f := rfl
+
+@[simp] theorem Vector.getElem_ofFn' {n : Nat} {α : Type u} (f : Fin n → α) (i : Nat)
+    (h : i < n) : (Vector.ofFn' f)[i] = f ⟨i, h⟩ := by
+  simp [Vector.ofFn']
+
 /-- Compiled code uses the core `Array.ofFn`, which fills an array of known
 capacity instead of building a `List` first. The `List` route exists only so
 that the kernel can reduce it. -/

progress/lean4-array-decidableeq-module-repro.md

@@ -107,6 +107,81 @@ All three are fixed by
   through the fully exposed `List.ofFn` and do reduce. They are proved equal to
   the core versions (`ofFn'_eq_ofFn`), so the swap back is a rewrite.
 
+## Audit: existing `Array.ofFn` / `Vector.ofFn` call sites
+
+Done 2026-07-28 against `cf303a47`, to decide whether the tree should migrate
+to `ofFn'` ahead of the upstream fix. **Conclusion: no, but because a
+consumer-side remedy is cheaper, not because migration is expensive.**
+
+**The defect is real.** `Vector.unit` in `HexMatrix.Basic` is exposed, is built
+with core `Vector.ofFn`, and does not reduce from a downstream module.
+`hex-matrix` is released, so this ships:
+
+```lean
+module
+public import HexMatrix.Basic
+public import HexBasic.ArrayDecEq
+open scoped Hex
+example : (Vector.unit Nat (n := 3) 1) = #v[0, 1, 0] := by decide +kernel
+-- stuck
+```
+
+**The cheapest fix is in the consumer, not the definition.** Adding
+
+```lean
+import all Init.Data.Array.Basic
+```
+
+to the *consuming* module makes the example above pass with no change to
+`Vector.unit` or to anything else in the tree. Equivalently, a proof can bridge
+locally with `rw [Vector.unit, ← Hex.Vector.ofFn'_eq_ofFn]` before
+`decide +kernel`. Both are one line, per-consumer, and cost nothing anywhere
+else. This is the recommended remedy.
+
+**Counts**, from stripping comments and matching the exact core identifiers
+(a plain grep over-counts badly: it picks up prose and the primed shim names):
+
+- 255 references in code;
+- **66** inside `def` / `abbrev` / `instance` bodies, which is the only
+  position where kernel reduction is affected. The remainder are in theorem
+  statements and proof bodies, where they do not matter;
+- of those 66, **9** are inside `*Impl` definitions, which are runtime
+  implementations behind `@[csimp]` where core `ofFn` is correct and must stay;
+- by library: HexGramSchmidt 19, HexMatrix 10, HexDeterminant 9,
+  HexNumberFieldTower 7, HexLLL 4, HexBerlekamp 3, HexPoly 3 (all three
+  `*Impl`), then single figures elsewhere.
+
+**A blanket migration was attempted and rejected**, but the experiment was
+weaker than it first appeared and should not be cited as proof that migration
+is costly. It rewrote 62 sites indiscriminately, including `*Impl` definitions
+that the recommendation says to leave alone, non-exposed definitions where
+reduction already stops earlier, and `HexGF2Mathlib/Basic.lean`, which is not a
+module file at all so the exposure question does not arise there. It produced
+15 primary diagnostics (the rest of the build output was cascading bad imports).
+The genuinely interesting population, the exposed non-`*Impl` sites, was never
+tested on its own.
+
+**Most of the observed churn was a missing shim API, since fixed.** The failures
+in `HexMatrix` and `HexRealRootsMathlib` came from core lemmas
+(`Vector.getElem_ofFn`, `Array.size_ofFn`) not applying to `ofFn'`.
+`HexBasic.OfFn` now provides `Array.size_ofFn'`, `Array.getElem_ofFn'`,
+`Vector.getElem_ofFn'`, and `Vector.toArray_ofFn'`. Note also that
+`ofFn'_eq_ofFn` is `@[simp]`, so ordinary `simp` already bridges; only
+`simp only` and `rfl`-closing steps needed the extra lemmas.
+
+**What cannot be done.** `@[expose]` cannot be applied retrospectively, so
+core `Array.ofFn` cannot be fixed from here. A shim defined as core `ofFn`
+would be definitionally equal but would inherit its non-reduction, so
+"defeq and reducing" is not available. Scoped simp sets affect proof
+elaboration, not kernel reduction.
+
+**Recommendation.** Use the consumer-side `import all` when a downstream module
+needs one of these definitions to reduce. Migrate an individual definition only
+if that is impossible for its consumer; the compatibility lemmas make it cheap
+when needed. Never migrate `*Impl` definitions. If #14270 stalls long enough
+that consumers accumulate, revisit migrating the exposed non-`*Impl` sites as a
+batch, which remains untested.
+
 ## Cleanup once #14270 lands
 
 After the toolchain is bumped past the fix: