Positive real L² operators: equality from equal squares

Attributed ASTIS completion of positive REAL scalar-root uniqueness background for Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. This is not the printed joint ΓP transport/B.11 identity or a main theorem.

Complete source statement (Samplinglib restatement)

Let Ω be any measurable space, μ any measure, and A,B bounded positive real-linear operators on L²(μ;ℝ). Assume A²=B², where multiplication is composition. Then A=B. Positivity is symmetry plus nonnegative quadratic form on the complete real L² space. No finite/probability measure, finite-dimensional L², nontriviality, energy identity or real/complex CFC/extension certificate is assumed.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Positive real L² operators: equality from equal squares

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique.positive_square_roots_unique · theorem · Teaching coverage

Read this first

Mathematical statement

\[A\ge0,\quad B\ge0,\quad A^2=B^2\quad\Longrightarrow\quad A=B.\]

Lean statement · positive_square_roots_unique

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem positive_square_roots_unique
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (A B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ)
    (hA : A.IsPositive) (hB : B.IsPositive) (hSq : A*A=B*B) :
    A=B

Exact module and namespace context

Proof roadmap

1Lift both positive real operators canonically
Use the compiled shared positive complex lift twice over the SAME arbitrary measure. The actual quotient maps ι,R,Q are identical in both results. The internally produced positive complex Ac,Bc satisfy Acι=ιA, Bcι=ιB and the literal coordinate formula for every complex L² class. The same theorem proves ‖ιu‖=‖u‖.
2Transport equality of squares
Complex linearity and intertwining give Ac²g=ι(A²Rg)+iι(A²Qg), and the corresponding formula for Bc. The original equality A²=B² applies separately to Rg and Qg, giving Ac²=Bc² on every complex class. No multiplicativity or decomposition certificate is a public premise.
3Apply complex positive-root uniqueness internally
The fixed Mathlib complex operator algebra provides complex functional calculus and its restricted real selfadjoint instance internally. Both positive Ac and Bc equal the positive square root of their common square by CFC.sqrt_unique. Hence Ac=Bc. This requires no real functional-calculus instance on the original operator algebra.
4Recover equality of the real operators
Norm preservation constructs a real-linear isometry e=ι, so ι is injective. Evaluate Ac=Bc on ιu; intertwining gives ιAu=ιBu, then injectivity gives Au=Bu for every real L² class. Extensionality proves A=B, including zero/subsingleton spaces.

Full assumptions and notation

All objects and hypotheses

Let Ω be any measurable space, μ any measure, and A,B bounded positive real-linear operators on L²(μ;ℝ). Assume A²=B², where multiplication is composition. Then A=B. Positivity is symmetry plus nonnegative quadratic form on the complete real L² space. No finite/probability measure, finite-dimensional L², nontriviality, energy identity or real/complex CFC/extension certificate is assumed.
Arbitrary measure, including zero/subsingleton/infinite-dimensional L²; no energy, CFC, complex extension or norm-preserving embedding certificate supplied.

Mathematical proof

1. Lift both positive real operators canonically

Use the compiled shared positive complex lift twice over the SAME arbitrary measure. The actual quotient maps ι,R,Q are identical in both results. The internally produced positive complex Ac,Bc satisfy Acι=ιA, Bcι=ιB and the literal coordinate formula for every complex L² class. The same theorem proves ‖ιu‖=‖u‖.

\[A_{\mathbb C},B_{\mathbb C}\ge0,\quad A_{\mathbb C}\iota=\iota A,\quad B_{\mathbb C}\iota=\iota B,\quad\|\iota u\|=\|u\|.\]

Corresponding Lean step

L2RealComplexOperator.exists_positive_complex_lift; hNorm; hAf; hBf; hAi; hBi

2. Transport equality of squares

Complex linearity and intertwining give Ac²g=ι(A²Rg)+iι(A²Qg), and the corresponding formula for Bc. The original equality A²=B² applies separately to Rg and Qg, giving Ac²=Bc² on every complex class. No multiplicativity or decomposition certificate is a public premise.

\[A_{\mathbb C}^2g=\iota A^2Rg+i\iota A^2Qg=\iota B^2Rg+i\iota B^2Qg=B_{\mathbb C}^2g.\]

Corresponding Lean step

hReal; hComplexSquare; map_add; map_smul; ContinuousLinearMap.ext

3. Apply complex positive-root uniqueness internally

The fixed Mathlib complex operator algebra provides complex functional calculus and its restricted real selfadjoint instance internally. Both positive Ac and Bc equal the positive square root of their common square by CFC.sqrt_unique. Hence Ac=Bc. This requires no real functional-calculus instance on the original operator algebra.

\[A_{\mathbb C}=\sqrt{B_{\mathbb C}^2}=B_{\mathbb C}.\]

Corresponding Lean step

hAcNonneg; hBcNonneg; CFC.sqrt_unique; hSame

4. Recover equality of the real operators

Norm preservation constructs a real-linear isometry e=ι, so ι is injective. Evaluate Ac=Bc on ιu; intertwining gives ιAu=ιBu, then injectivity gives Au=Bu for every real L² class. Extensionality proves A=B, including zero/subsingleton spaces.

\[\iota Au=A_{\mathbb C}\iota u=B_{\mathbb C}\iota u=\iota Bu\quad\Longrightarrow\quad A=B.\]

Corresponding Lean step

e; LinearIsometry.injective; hAi; hBi; ContinuousLinearMap.ext

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · positive_square_roots_unique

Lift both positive real operators canonically; Transport equality of squares; Apply complex positive-root uniqueness internally; Recover equality of the real operators

Download module (.lean)

theorem positive_square_roots_unique
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (A B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ)
    (hA : A.IsPositive) (hB : B.IsPositive) (hSq : A*A=B*B) :
    A=B := by
  letI := IsStarNormal.instNonUnitalContinuousFunctionalCalculus
    (A := Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)
  letI : NonUnitalContinuousFunctionalCalculus ℂ
      (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) IsStarNormal :=
    NonUnitalClosedEmbeddingContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus
  letI : NonUnitalContinuousFunctionalCalculus ℝ
      (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) IsSelfAdjoint :=
    IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus
      (A := Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ)
  let ι : Lp ℝ 2 μ →L[ℝ] Lp ℂ 2 μ := Complex.ofRealCLM.compLpL 2 μ
  let R : Lp ℂ 2 μ →L[ℝ] Lp ℝ 2 μ := Complex.reCLM.compLpL 2 μ
  let Q : Lp ℂ 2 μ →L[ℝ] Lp ℝ 2 μ := Complex.imCLM.compLpL 2 μ
  obtain ⟨hNorm,_,Ac,hAc,hAf,hAi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ A hA
  obtain ⟨_,_,Bc,hBc,hBf,hBi,_⟩ :=
    L2RealComplexOperator.exists_positive_complex_lift μ B hB
  have hReal (u : Lp ℝ 2 μ) : A (A u) = B (B u) :=
    congrArg (fun D : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ => D u) hSq
  have hComplexSquare : Ac*Ac = Bc*Bc := by
    apply ContinuousLinearMap.ext
    intro g
    change Ac (Ac g) = Bc (Bc g)
    calc
      Ac (Ac g) = ι (A (A (R g))) + Complex.I • ι (A (A (Q g))) := by
        rw [hAf g, map_add, map_smul, hAi, hAi]
      _ = ι (B (B (R g))) + Complex.I • ι (B (B (Q g))) := by
        rw [hReal (R g),hReal (Q g)]
      _ = Bc (Bc g) := by rw [hBf g, map_add, map_smul, hBi, hBi]
  have hAcNonneg : 0 ≤ Ac := (ContinuousLinearMap.nonneg_iff_isPositive Ac).mpr hAc
  have hBcNonneg : 0 ≤ Bc := (ContinuousLinearMap.nonneg_iff_isPositive Bc).mpr hBc
  have hSame : Ac = Bc :=
    (CFC.sqrt_unique hComplexSquare hAcNonneg).symm.trans (CFC.sqrt_unique rfl hBcNonneg)
  let e : Lp ℝ 2 μ →ₗᵢ[ℝ] Lp ℂ 2 μ :=
    { toLinearMap := ι.toLinearMap
      norm_map' := hNorm }
  apply ContinuousLinearMap.ext
  intro u
  apply e.injective
  change ι (A u) = ι (B u)
  rw [← hAi u, ← hBi u, hSame]

end
end AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique

#print axioms AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique.positive_square_roots_unique

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
D1 standard unique positive square root background on a complete real Hilbert space.	Positive REAL A/B with equal squares over arbitrary-measure L² imply A=B.	generalization	Generic background completion is attributed; actual produced root fixes SAME ν/T/D, without extra energy assumptions.
Original finite Euclidean potential, curvature and step assumptions; literal reflection kernel and stationary conditional observable.	Arbitrary-measure REAL scalar background, internally supplied complex CFC.	generalization	Source assumptions unchanged; zero base dimension explicitly extended and L² may be infinite-dimensional.
Printed joint ΓP/B11 and centered root order/inverse/polar plus main algorithms and costs.	Exported real scalar uniqueness and genuine original-input same defect/root only. Printed joint GammaP/ontoM/typed B*B, centered order/inverse/polar/H1/dynamics/main/cost/composition remain separate.	unresolved	This supplies scalar real uniqueness and genuine actual input consumer only; no onto-M/joint operator transport, full-space inverse, main theorem or cost claim.

Exported real scalar uniqueness and genuine original-input same defect/root only. Printed joint GammaP/ontoM/typed B*B, centered order/inverse/polar/H1/dynamics/main/cost/composition remain separate.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

domains: D1 printed probability-L2 background is explicitly generalized to arbitrary-measure real L2. — Independent native generalization nonblocking classification retained in runs/20261007-companion-priority/pbps-real-root-unique62/source-review62/source.0.review.json
scopes: Scalar real positive uniqueness only. Printed jointGammaP/ontoM/typedB*B/centeredorder/inverse/polar/H1/dynamics/main/error/querycost/composition remain separate, not erased source edges. — Independent native unresolved nonblocking classification retained in runs/20261007-companion-priority/pbps-real-root-unique62/source-review62/source.0.review.json

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Exported real scalar uniqueness and genuine original-input same defect/root only. Printed joint GammaP/ontoM/typed B*B, centered order/inverse/polar/H1/dynamics/main/cost/composition remain separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator.exists_positive_complex_lift

Mathlib API called (external library)

ContinuousLinearMap.ext
map_add
map_smul
ContinuousLinearMap.nonneg_iff_isPositive
CFC.sqrt_unique
LinearIsometry.injective

Mathematical sources

arXiv2609.06905v1 D1 positive-root uniqueness background; scalar antecedent to printed B10 canonical joint root — Exported real scalar uniqueness and genuine original-input same defect/root only. Printed joint GammaP/ontoM/typed B*B, centered order/inverse/polar/H1/dynamics/main/cost/composition remain separate.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Positive real L² operators: equality from equal squares

Complete source statement (Samplinglib restatement)

Positive real L² operators: equality from equal squares

Read the formalized proofs

Positive real L² operators: equality from equal squares

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Lift both positive real operators canonically

2. Transport equality of squares

3. Apply complex positive-root uniqueness internally

4. Recover equality of the real operators

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?