Five facts about EuclideanSpace the corpus kept re-proving

Category: 1-Mathlib (CSD-free; one upstream candidate, four specialisations). BACKLOG #146 cluster (D).

Each of these was proved independently in two or three layers, which is what check-duplicates reported. They are collected here because they cross layers: LF2 through Thermo and Empirical all need them, so no CSD layer is the right owner.

One upstream candidate

Matrix.norm_toEuclideanLin_of_isom — that Aᴴ A = 1 makes A's action norm-preserving. Mathlib has no norm or isometry lemma for toLpLin/toEuclideanLin at all (its API is toLpLin_apply, _one, _mul, _mul_same, _pow, _symm_comp, the determinant, and the adjoint bridge). This one arrived with that verdict already written twice: LF5/DilationFromFlow.lean called its copy a "generic helper (Mathlib upstream candidate)", and CV/ArenaBridge.lean carried a character-for-character identical second copy whose docstring explained why — "restated to keep CV free of an LF5 import". That is a request for this file, made twice.

Four convenience specialisations, which must not be offered upstream

• EuclideanSpace.single_one_ne_zero is PiLp.single_eq_zero_iff with one_ne_zero;
• EuclideanSpace.normSq_inner_single is EuclideanSpace.inner_single_left with map_one;
• Complex.inner_ofReal_ofReal is RCLike.inner_apply with Complex.conj_ofReal.
• Matrix.toEuclideanLin_mul_apply is @[simp] Matrix.toLpLin_mul_same applied to a vector. Upstream states composition as an equality of maps; the corpus always needs it applied, and had five copies of the applied form. A first draft of this file added a sixth with a docstring asserting Mathlib has no _mul lemma for toEuclideanLin — which is false, and looked true only because the upstream name is toLpLin, toEuclideanLin being toLpLin 2 2. The same mistake was live in Empirical/CSD/Algorithms/CircuitFlow.lean, whose toEuclideanLin_pow_apply re-derived @[simp] toLpLin_pow by induction; under #146 (D) it cites it instead.

They are here to be written once, not because upstream lacks them.

What this file deliberately does not hold, and why that matters

Two facts that looked like they belonged here turned out to have homes already, and #146 (D) retired their duplicates by citing rather than by moving them:

• nonzero image of a unitary — Matrix.UnitaryGroup.toEuclideanLin_unitary_ne_zero, in UnitaryTransitive.lean;
• the trace-of-outer-product bridge — LF2.trace_outer_mul_eq_inner, which is about LF2.outerProduct and so is not Cat-1 material at all.

A file like this earns its keep only while everything in it is genuinely homeless, so the exclusions are part of its content.

References: the consumers listed in specs/BACKLOG.md #146 (D); scripts/check-duplicates.sh; specs/BACKLOG.md #146, #145.

theorem Matrix.norm_toEuclideanLin_of_isom {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {A : Matrix κ ι ℂ} (hA : A.conjTranspose * A = 1) (ψ : EuclideanSpace ℂ ι) : ‖(toEuclideanLin A) ψ‖ = ‖ψ‖

An isometry of matrices induces a norm-preserving map. ‖Aψ‖² = re⟪Aψ, Aψ⟫ = re⟪ψ, Aᴴ A ψ⟫ = ‖ψ‖², through the matrix-operator adjoint bridge.

A need not be square: Aᴴ A = 1 on the source is all that is used, so this covers a dilation into a larger space, which is the use that first wanted it.

theorem Matrix.toEuclideanLin_mul_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A B : Matrix ι ι ℂ) (v : EuclideanSpace ℂ ι) : (toEuclideanLin (A * B)) v = (toEuclideanLin A) ((toEuclideanLin B) v)

toEuclideanLin turns matrix multiplication into composition, applied to a vector.

⚠️ A specialisation: @[simp] Matrix.toLpLin_mul_same is the same fact as an equality of maps, and this is it applied. Five layers wrote the applied form themselves.

theorem EuclideanSpace.single_one_ne_zero {ι : Type u_1} [DecidableEq ι] (i : ι) : single i 1 ≠ 0

A computational-basis vector is nonzero.

⚠️ A specialisation of PiLp.single_eq_zero_iff, not a new fact. It is here because three layers each wrote their own by three different proofs: LF5.single_one_ne_zero, LF4.cpBasisVec_ne_zero and RecordLayer.single_ne_zero'.

theorem EuclideanSpace.normSq_inner_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : EuclideanSpace ℂ ι) (i : ι) : ‖inner ℂ (single i 1) ψ‖ ^ 2 = ‖ψ.ofLp i‖ ^ 2

The inner product against a basis vector is that coordinate, over any index type.

⚠️ A specialisation of EuclideanSpace.inner_single_left. It had four copies — Fin 4 twice, Fin 8, and the dilated Fin N × ι of LF4/POVMVolume.lean — of which the duplicate scan could group only the two that shared a type.

theorem Complex.inner_ofReal_ofReal (a b : ℝ) : inner ℂ ↑a ↑b = ↑(a * b)

The inner product of two real scalars, inside ℂ.

⚠️ A specialisation of RCLike.inner_apply with Complex.conj_ofReal. Two contextuality files wrote it independently, as cplx_scalar_inner and mp_scalar_inner, with the same proof.