CStarMatrix ↔ Matrix transport bridge for the operator-convexity ladder

Matrix n n ℂ is not a CStarAlgebra at its default instances: the C⋆-algebra structure (norm, topology, spectral order) lives on the type synonym CStarMatrix m n A := Matrix m n A (CStarMatrix.instCStarAlgebra). Consequently the C⋆-generic continuous-functional-calculus order machinery — CFC.log (operator monotone), CFC.log_le_log, the rpow order lemmas, the rpow→log limit — is stated for [CStarAlgebra A] and does not fire directly on the bare Matrix type used by Matrix.OperatorConvexOn / Matrix.OperatorConcaveOn and the L.1/L.2 rungs.

This file builds the transport across the star-algebra equivalence e := CStarMatrix.ofMatrixStarAlgEquiv : Matrix n n ℂ ≃⋆ₐ[ℂ] CStarMatrix n n ℂ (which is the identity Equiv.refl on carriers, hence continuous), and uses it to pull the C⋆-generic facts back onto Matrix.

Main results

• Matrix.cstar_cfc (B.1, the crux): CFC naturality across the synonym equiv, e (cfc f A) = cfc f (e A). Note the two cfcs come from different functional-calculus instances — Matrix.IsHermitian.instContinuousFunctionalCalculus on the left and the C⋆-algebra CFC on the right — and they agree by CFC uniqueness, packaged by StarAlgHomClass.map_cfc.
• Matrix.cstar_le_iff (B.2): the Löwner order on Matrix and the spectral order on CStarMatrix agree across e, e A ≤ e B ↔ A ≤ B. Proved via StarRingEquivClass.instOrderIsoClass.map_le_map_iff (a star-ring equivalence is an order isomorphism between StarOrderedRings).
• Matrix.cstar_isStrictlyPositive: A.PosDef → IsStrictlyPositive (e A), the positivity hypothesis transport feeding the order lemmas.
• Matrix.matrix_log_le_log (B.3, log): operator monotonicity of log on positive-definite matrices in the Löwner order, A ≤ B → cfc Real.log A ≤ cfc Real.log B, transported from CFC.log_le_log. This is the genuine ladder enabler: the route-2 path to operator concavity of log (specs/operator-convexity-plan.md L.2) consumes CFC.log_monotoneOn and tendsto_cfc_rpow_sub_one_log on the C⋆ side, and this bridge is what makes the conclusion expressible on the Matrix carrier of the OperatorConcaveOn predicate.

Honest scope (rpow wall) SUPERSEDED 2026-08-22 (MG-3): the rpow rung is LANDED

The rpow wall recorded here previously is dissolved. The MG-3 probe (specs/mathlib-gaps-plan.md; scratch_mg3_probe.lean, five rounds) established that the obstruction was exactly two generic instances failing to fire through the discrimination tree — the ℝ-CFC over IsSelfAdjoint (the shim below, already present) and NonnegSpectrumClass ℝ (instCStarMatrixNonnegSpectrumClass, the second shim, added with B.4) — and that with both registered the entire upstream monotonicity tier fires on CStarMatrix n n ℂ, including CFC.monotone_nnrpow (operator monotonicity of x ^ p, p ∈ [0,1], which landed upstream in …/Rpow/Order.lean after the wall note was written). B.4 transports it to the Matrix carrier: matrix_nnrpow_le_nnrpow (the L.3 rung) and matrix_sqrt_le_sqrt, via the ℝ≥0-cfcₙ naturality cstar_cfcₙ_nnreal (the ℝ≥0 companion of B.1). The remaining C⋆-side absence for the DPI ladder is operator CONVEXITY (Lieb) — upstream's own TODO; see specs/operator-convexity-plan.md and MATHLIB-GAPS.md.

Category: 1-Mathlib (CSD-free). Natural Mathlib namespace Matrix.

The ℝ-CFC instance shim on CStarMatrix n n ℂ

The generic IsSelfAdjoint.instContinuousFunctionalCalculus does not fire on CStarMatrix n n ℂ through the discrimination tree (its predicate-output IsSelfAdjoint is not matched), so we register it explicitly as a local instance. It elaborates because CStarMatrix n n ℂ is a unital CStarAlgebra (CStarMatrix.instCStarAlgebra) with the ℂ-CFC over IsStarNormal.

instance Matrix.instCStarMatrixRealCFC {n : Type u_1} [Fintype n] [DecidableEq n] : ContinuousFunctionalCalculus ℝ (CStarMatrix n n ℂ) IsSelfAdjoint

The real continuous functional calculus on CStarMatrix n n ℂ over self-adjoint elements, registered explicitly (the generic instance does not fire on CStarMatrix via the discrimination tree).

Continuity of the synonym equivalence

theorem Matrix.ofMatrixStarAlgEquiv_continuous {n : Type u_1} [Fintype n] : Continuous ⇑CStarMatrix.ofMatrixStarAlgEquiv

The star-algebra equivalence Matrix n n ℂ ≃⋆ₐ[ℂ] CStarMatrix n n ℂ is continuous: on carriers it is the identity (Equiv.refl), and CStarMatrix.ofMatrixL is a continuous linear equivalence with continuous_id.

B.2 — order transport (Löwner ↔ spectral order across e)

theorem Matrix.cstar_le_iff {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : CStarMatrix.ofMatrixStarAlgEquiv A ≤ CStarMatrix.ofMatrixStarAlgEquiv B ↔ A ≤ B

B.2. The Löwner order on Matrix n n ℂ ((B - A).PosSemidef) and the spectral order on CStarMatrix n n ℂ agree across the star-algebra equivalence e: e A ≤ e B ↔ A ≤ B. Both Matrix and CStarMatrix are StarOrderedRings, and a star-ring equivalence is an OrderIso between StarOrderedRings (StarRingEquivClass.instOrderIsoClass), so this is map_le_map_iff.

B.1 — CFC transport (the crux)

theorem Matrix.cstar_cfc {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (f : ℝ → ℝ) (hA : A.IsHermitian) (hf : ContinuousOn f (spectrum ℝ A)) : CStarMatrix.ofMatrixStarAlgEquiv (cfc f A) = cfc f (CStarMatrix.ofMatrixStarAlgEquiv A)

B.1 (the crux). The continuous functional calculus commutes with the synonym equivalence e: for Hermitian A and f continuous on spectrum ℝ A, e (cfc f A) = cfc f (e A).

The left cfc is taken in Matrix's own functional-calculus instance (Matrix.IsHermitian.instContinuousFunctionalCalculus, the spectral triple product); the right cfc is taken in the C⋆-algebra instance on CStarMatrix. These are a priori different functional-calculus instances; they agree because e is a continuous star-algebra homomorphism and the CFC is unique (StarAlgHomClass.map_cfc, whose proof routes through ContinuousMap.UniqueHom). So no separate uniqueness argument is needed at this level.

Positivity transport

theorem Matrix.cstar_isStrictlyPositive {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) : IsStrictlyPositive (CStarMatrix.ofMatrixStarAlgEquiv A)

A positive-definite matrix maps to a strictly-positive element of CStarMatrix n n ℂ. IsStrictlyPositive a := 0 ≤ a ∧ IsUnit a: nonnegativity transports via cstar_le_iff (B.2) and map_zero e, and invertibility transports because e is a ring equivalence.

B.3 — operator monotonicity of log transported onto Matrix

theorem Matrix.logContinuousOn {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) : ContinuousOn Real.log (spectrum ℝ A)

Real.log is continuous on the (positive) spectrum of a positive-definite matrix.

theorem Matrix.matrix_log_le_log {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.PosDef) (hB : B.PosDef) (hAB : A ≤ B) : cfc Real.log A ≤ cfc Real.log B

B.3 (log). Operator monotonicity of log on positive-definite matrices, in the Löwner order: A ≤ B → cfc Real.log A ≤ cfc Real.log B (for positive-definite A, B).

Transported from CFC.log_le_log on CStarMatrix n n ℂ: the order transports (B.2), strict positivity transports (cstar_isStrictlyPositive), and CFC.log (e A) = e (cfc Real.log A) by B.1 (CFC.log a := cfc Real.log a definitionally). The statement is in terms of cfc Real.log on the Matrix side because CFC.log itself requires NormedRing (Matrix n n ℂ), which the default Matrix instances do not provide — this is exactly the carrier mismatch the bridge resolves.

The second shim + B.4 — rpow operator monotonicity on Matrix (2026-08-22, MG-3)

instance Matrix.instCStarMatrixNonnegSpectrumClass {n : Type u_1} [Fintype n] [DecidableEq n] : NonnegSpectrumClass ℝ (CStarMatrix n n ℂ)

The second non-firing generic instance found by the MG-3 probe: NonnegSpectrumClass ℝ on CStarMatrix n n ℂ, registered explicitly from its own generic provider (CStarAlgebra.instNonnegSpectrumClass — provable as a term, not found by synthesis through the repeated-index discrimination key). With this and the ℝ-CFC shim above, the upstream rpow/sqrt/log order tier fires on CStarMatrix.

theorem Matrix.cstar_cfcₙ_nnreal {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : 0 ≤ A) (f : NNReal → NNReal) (hf : ContinuousOn f (quasispectrum NNReal A)) (hf0 : f 0 = 0) : CStarMatrix.ofMatrixStarAlgEquiv (cfcₙ f A) = cfcₙ f (CStarMatrix.ofMatrixStarAlgEquiv A)

B.4a. ℝ≥0-cfcₙ naturality across the synonym equivalence, on nonnegative matrices: e (cfcₙ f A) = cfcₙ f (e A). The ℝ≥0 companion of B.1, by NonUnitalStarAlgHomClass.map_cfcₙ (the two cfcₙs come from the Matrix-side and CStarMatrix-side ℝ≥0 functional calculi respectively).

theorem Matrix.matrix_nnrpow_le_nnrpow {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} {p : NNReal} (hp : p ∈ Set.Icc 0 1) (hA : 0 ≤ A) (hAB : A ≤ B) : A ^ p ≤ B ^ p

B.4 (rpow, the L.3 rung). Operator monotonicity of the nonnegative power A ↦ A ^ p (p : ℝ≥0, p ≤ 1) on positive-semidefinite matrices in the Löwner order — CFC.monotone_nnrpow transported onto the Matrix carrier. The p = 0 exponent is junk-valued (A ^ 0 = 0 by the cfcₙ zero convention) and handled separately; for p ≠ 0 the pointwise function is zero-preserving and the naturality B.4a identifies the powers across e.

theorem Matrix.matrix_sqrt_le_sqrt {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : 0 ≤ A) (hAB : A ≤ B) : CFC.sqrt A ≤ CFC.sqrt B

B.4 corollary (sqrt). Operator monotonicity of the matrix square root on the Löwner order: 0 ≤ A ≤ B → √A ≤ √B.

B.5 / B.6 — operator CONCAVITY transported (the L.2 / L.3a-interior rungs)

Upstream proves operator concavity C⋆-generically (CFC.concaveOn_log, CFC.concaveOn_rpow); the same transport that carries monotonicity carries concavity, so both rungs are corollaries rather than builds. The convex combination is taken with real scalars coerced to ℂ, which is what smul_transport normalises.

theorem Matrix.smul_transport {n : Type u_1} [Fintype n] (t : ℝ) (A : Matrix n n ℂ) : CStarMatrix.ofMatrixStarAlgEquiv (↑t • A) = t • CStarMatrix.ofMatrixStarAlgEquiv A

Real-scalar smul commutes with the Matrix ≃ CStarMatrix transport. The convex combinations below are formed in ℂ, so this is the lemma that lets map_add/map_smul normalise them.

theorem Matrix.matrix_log_concave {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.PosDef) (hB : B.PosDef) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : ↑t • cfc Real.log A + (1 - ↑t) • cfc Real.log B ≤ cfc Real.log (↑t • A + (1 - ↑t) • B)

B.5. Operator concavity of log on positive-definite matrices, in Löwner order: t·log A + (1−t)·log B ≤ log (t·A + (1−t)·B). Transported from CFC.concaveOn_log.

theorem Matrix.operatorConcaveOn_log : OperatorConcaveOn (Set.Ioi 0) Real.log

★★ L.2 — log is operator concave on (0, ∞), in the corpus's all-dimensions OperatorConcaveOn predicate. The plan budgeted this as a multi-day build against a wall ("Matrix n n ℂ is not a CStarAlgebra"); the wall was a scope question and upstream has since proved the C⋆-generic statement, so it is a transport.

theorem Matrix.matrix_rpow_concave {n : Type u_1} [Fintype n] [DecidableEq n] {p : ℝ} (hp : p ∈ Set.Icc 0 1) {A B : Matrix n n ℂ} (hA : 0 ≤ A) (hB : 0 ≤ B) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : ↑t • A ^ p + (1 - ↑t) • B ^ p ≤ (↑t • A + (1 - ↑t) • B) ^ p

★ L.3a interior — x ^ p is operator concave for p ∈ [0,1], on the bare Matrix carrier in ^-notation and Löwner order. Transported from CFC.concaveOn_rpow; supersedes the endpoints-only operatorConcaveOn_rpow_zero / _one.

B.7 — x log x, the L.4 rung, transported

OperatorConvexCFC.convexOn_mul_log closes an upstream TODO C⋆-generically; this puts it on the Matrix carrier alongside matrix_log_concave. ⚠️ It is an input to the Effros/Lieb summit, not the summit: hDPI is untouched (specs/lieb-dpi-scoping.md).

theorem Matrix.matrix_mul_log_convex {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.PosDef) (hB : B.PosDef) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (↑t • A + (1 - ↑t) • B) * cfc Real.log (↑t • A + (1 - ↑t) • B) ≤ ↑t • (A * cfc Real.log A) + (1 - ↑t) • (B * cfc Real.log B)

L.4 on the matrix carrier. A ↦ A · log A is operator convex on positive-definite matrices, in Löwner order.

Non-vacuity witness

The bridge is non-vacuous: it applies to a concrete non-commuting positive-definite pair. A = diagonal !![2, 1]-style witnesses are positive definite; the transport lemmas relate the genuine carriers (the Matrix Löwner order and the CStarMatrix spectral order), not a degenerate or mismatched structure.