IdealTransport.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

Ideal transport through the extended trace cone

Additive idempotents recover closed ideals. The scalar limits at zero and infinity recover the finite and zero ideals of an extended lower semicontinuous trace. These constructions give the ideal transport in Section 2 of The trace cone classifies Razak–Jacelon stabilizations (OpenAI, 2026).

theorem OAI.TraceConeClassification.ExtendedTrace.ext line 25
def OAI.TraceConeClassification.ExtendedTrace.add line 32
Source documentation
Pointwise addition of the actual extended weights, including infinite values.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:105 (same declaration text).
```
def add (τ σ : ExtendedTrace A) : ExtendedTrace A where
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
theorem OAI.TraceConeClassification.ExtendedTrace.add_apply line 40
def OAI.TraceConeClassification.ExtendedTrace.zero line 44
Source documentation
The zero weight, not the weight of the zero ideal.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:113 (same declaration text).
```
def zero : ExtendedTrace A where
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
theorem OAI.TraceConeClassification.ExtendedTrace.zero_apply line 52
theorem OAI.TraceConeClassification.ExtendedTrace.idempotent_values line 55
Source documentation
Additive idempotence cannot hide any finite nonzero values.
```
theorem idempotent_values {τ : ExtendedTrace A} (hτ : τ.add τ = τ) (a : Positive A) :
    τ a = 0 ∨ τ a = ∞ := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive
def OAI.TraceConeClassification.ClosedIdeal line 66
Source documentation
A literal closed two-sided star ideal of the coefficient algebra.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:123 (same declaration text).
```
def ClosedIdeal (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A]
    [StarOrderedRing A] :=
…
```
instance OAI.TraceConeClassification.ClosedIdeal.(instance at line 73) line 73
def OAI.TraceConeClassification.ClosedIdeal.weight line 76
Source documentation
The extended trace taking zero on an ideal and infinity outside it.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:155 (same declaration text).
```
def weight (I : ClosedIdeal A) : ExtendedTrace A :=
…
```
Mentions: OAI.TraceConeClassification.ClosedIdeal, OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.ClosedIdeal.weight_apply line 79
theorem OAI.TraceConeClassification.ClosedIdeal.weight_idempotent line 83
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:157 (different declaration text). Qualify references as OAI.TraceConeClassification.ClosedIdeal.weight_idempotent@path.
theorem OAI.TraceConeClassification.ClosedIdeal.finiteIdeal_weight line 89
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:158 (different declaration text). Qualify references as OAI.TraceConeClassification.ClosedIdeal.finiteIdeal_weight@path.
lemma OAI.TraceConeClassification.ClosedIdeal.weight_injective line 102
theorem OAI.TraceConeClassification.ClosedIdeal.le_iff_add_weight line 108
Source documentation
The reversed order on ideal weights can be read using only addition.
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:159 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ClosedIdeal.le_iff_add_weight@path.
```
theorem le_iff_add_weight (I J : ClosedIdeal A) :
    I ≤ J ↔ I.weight.add J.weight = I.weight := by
…
```
Mentions: OAI.TraceConeClassification.ClosedIdeal
def OAI.TraceConeClassification.ExtendedTrace.finIdeal line 134
Source documentation
The closed finite-domain ideal, with the absorption and closedness already proved.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:130 (same declaration text).
```
def finIdeal (τ : ExtendedTrace A) : ClosedIdeal A :=
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.ClosedIdeal
theorem OAI.TraceConeClassification.ExtendedTrace.idempotent_zero_on_finIdeal line 140
Source documentation
For an additive idempotent, every positive in its finite ideal has value zero. Lower semicontinuity is essential here: the finite ideal is a norm closure.
```
theorem idempotent_zero_on_finIdeal {τ : ExtendedTrace A} (hτ : τ.add τ = τ)
    (a : Positive A) (ha : a.1 ∈ τ.finiteIdeal) : τ a = 0 := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive
theorem OAI.TraceConeClassification.ExtendedTrace.idempotent_eq_weight line 151
Source documentation
Every additive idempotent is the literal weight of a closed two-sided ideal.
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:164 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.idempotent_eq_weight@path.
```
theorem idempotent_eq_weight {τ : ExtendedTrace A} (hτ : τ.add τ = τ) :
    τ.finIdeal.weight = τ := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
def OAI.TraceConeClassification.IdempotentTrace line 166
Source documentation
Precisely the additive idempotents, not a chosen subclass of traces.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:168 (same declaration text).
```
def IdempotentTrace (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A]
    [StarOrderedRing A] := {τ : ExtendedTrace A // τ.add τ = τ}
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
def OAI.TraceConeClassification.closedIdealEquivIdempotent line 170
Source documentation
The bijection in the first paragraph of the proof of st:ideals.
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:171 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.closedIdealEquivIdempotent@path.
```
def closedIdealEquivIdempotent : ClosedIdeal A ≃ IdempotentTrace A where
…
```
Mentions: OAI.TraceConeClassification.ClosedIdeal, OAI.TraceConeClassification.IdempotentTrace

theorem OAI.TraceConeClassification.canonicalConvergence_unique line 177

Source documentation

Uniqueness of limits for canonical cut limsup/liminf convergence.

theorem canonicalConvergence_unique {ι : Type*} (l : Filter ι) [l.NeBot]
    (f : ι → ExtendedTrace A) {τ σ : ExtendedTrace A}
    (hτ : CanonicalConvergence A l f τ) (hσ : CanonicalConvergence A l f σ) : τ = σ := by
…

Mentions: OAI.TraceConeClassification.ExtendedTrace

def OAI.TraceConeClassification.idempotentTraceEquiv line 195
Source documentation
An additive bijection of extended trace cones identifies their additive idempotents.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:179 (same declaration text).
```
def idempotentTraceEquiv (e : ExtendedTrace A ≃ ExtendedTrace B)
    (he : ∀ τ σ, e (τ.add σ) = (e τ).add (e σ)) : IdempotentTrace A ≃ IdempotentTrace B where
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.IdempotentTrace
def OAI.TraceConeClassification.closedIdealEquivOfAdditive line 205
Source documentation
Recovering the closed ideals from their idempotent trace weights.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:188 (same declaration text).
```
def closedIdealEquivOfAdditive (e : ExtendedTrace A ≃ ExtendedTrace B)
    (he : ∀ τ σ, e (τ.add σ) = (e τ).add (e σ)) : ClosedIdeal A ≃ ClosedIdeal B :=
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.ClosedIdeal
lemma OAI.TraceConeClassification.closedIdealEquivOfAdditive_weight line 210
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:193 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.closedIdealEquivOfAdditive_weight@path.
def OAI.TraceConeClassification.closedIdealOrderEquivOfAdditive line 217
Source documentation
The order isomorphism of closed ideals induced by an additive trace-cone bijection.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:197 (same declaration text).
```
def closedIdealOrderEquivOfAdditive (e : ExtendedTrace A ≃ ExtendedTrace B)
    (he : ∀ τ σ, e (τ.add σ) = (e τ).add (e σ)) : ClosedIdeal A ≃o ClosedIdeal B where
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.ClosedIdeal
theorem OAI.TraceConeClassification.canonicalConvergence_of_pointwise line 229
Source documentation
Pointwise convergence implies the specified convergence, but is not used as its definition (the converse is false in general).
```
theorem canonicalConvergence_of_pointwise {ι : Type*} (l : Filter ι) [l.NeBot]
    (f : ι → ExtendedTrace A) (σ : ExtendedTrace A)
    (h : ∀ a, Tendsto (fun i => f i a) l (𝓝 (σ a))) :
    CanonicalConvergence A l f σ := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace

lemma OAI.TraceConeClassification.canonicalConvergence_map_iff line 238

Source documentation

Reindexing a net by its image filter does not change the cut inequalities.

lemma canonicalConvergence_map_iff {ι κ : Type*} (l : Filter ι) (g : ι → κ)
    (f : κ → ExtendedTrace A) (σ : ExtendedTrace A) :
    CanonicalConvergence A (map g l) f σ ↔ CanonicalConvergence A l (f ∘ g) σ := by
…

Mentions: OAI.TraceConeClassification.ExtendedTrace

def OAI.TraceConeClassification.PreservesCanonicalConvergence line 245
Source documentation
Preservation of canonical convergence for filters on the trace cone. The image-filter identity extends this property to nets in every index type.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:206 (same declaration text).
```
def PreservesCanonicalConvergence (f : ExtendedTrace A → ExtendedTrace B) : Prop :=
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.PreservesCanonicalConvergence.net line 249
theorem OAI.TraceConeClassification.ExtendedTrace.scale_zero_limit line 262
Source documentation
Positive scalar multiples converge to the finite-ideal weight as the scalar tends to zero.
```
theorem scale_zero_limit (τ : ExtendedTrace A) :
    CanonicalConvergence A (𝓝[>] (0 : ℝ≥0)) (fun r => τ.scale r) τ.finIdeal.weight := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.ExtendedTrace.lowerSemicontinuous_supportWeight line 280
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:134 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.ExtendedTrace.lowerSemicontinuous_supportWeight@path.
def OAI.TraceConeClassification.ExtendedTrace.supportWeight line 296
Source documentation
The pointwise support weight of a trace. It will be identified with the weight of the literal zero ideal, rather than an arbitrary ideal label.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:137 (same declaration text).
```
def supportWeight (τ : ExtendedTrace A) : ExtendedTrace A where
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.ExtendedTrace.supportWeight_apply line 308
lemma OAI.TraceConeClassification.ExtendedTrace.supportWeight_idempotent line 311
def OAI.TraceConeClassification.ExtendedTrace.zeroIdeal line 320
Source documentation
The zero ideal, as an actual closed two-sided ideal in the algebra. Its positive elements are characterized by mem_zeroIdeal_iff below.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:149 (same declaration text).
```
def zeroIdeal (τ : ExtendedTrace A) : ClosedIdeal A := τ.supportWeight.finIdeal
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.ClosedIdeal
lemma OAI.TraceConeClassification.ExtendedTrace.mem_zeroIdeal_iff line 322
lemma OAI.TraceConeClassification.ExtendedTrace.zeroIdeal_weight line 336
theorem OAI.TraceConeClassification.ExtendedTrace.scale_infty_limit line 341
Source documentation
The second scalar limit from st:scalar-limits, including all infinite traces and the possibility that the zero ideal is the whole algebra or zero.
```
theorem scale_infty_limit (τ : ExtendedTrace A) :
    CanonicalConvergence A atTop (fun r : ℝ≥0 => τ.scale r) τ.zeroIdeal.weight := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.ExtendedTrace.scale_zero line 359
structure OAI.TraceConeClassification.TraceConeEquiv line 369
Source documentation
An equivalence of extended trace cones preserving addition, zero, positive scalar multiplication, and canonical convergence in both directions.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:210 (same declaration text).
```
structure TraceConeEquiv (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A]
    [StarOrderedRing A] (B : Type v) [NonUnitalCStarAlgebra B] [PartialOrder B]
    [StarOrderedRing B] where
…
```
lemma OAI.TraceConeClassification.TraceConeEquiv.map_scale_all line 383
def OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso line 391
Source documentation
The actual ideal-poset isomorphism induced by a cone equivalence.
Also declared: ComparatorChallenges/TraceIdealTransportSupport.lean:222 (same declaration text).
```
def idealOrderIso : ClosedIdeal A ≃o ClosedIdeal B :=
…
```
Mentions: OAI.TraceConeClassification.ClosedIdeal
lemma OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_weight line 394
theorem OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_finIdeal line 400
Source documentation
The scalar-zero limit identifies the finite-domain ideals under the induced ideal correspondence, including weights whose finite ideal is proper or zero.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalCStarAlgebra, PartialOrder, StarOrderedRing, OAI.TraceConeClassification.TraceConeEquiv, OAI.TraceConeClassification.ExtendedTrace, Eq, OAI.TraceConeClassification.ClosedIdeal, OrderIso, OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso, OAI.TraceConeClassification.ExtendedTrace.finIdeal, Equiv, OAI.TraceConeClassification.TraceConeEquiv.toEquiv
Proof uses: OAI.TraceConeClassification.ClosedIdeal.weight_injective, Eq.mpr, OAI.TraceConeClassification.ClosedIdeal.weight, id, congrArg, OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_weight, OAI.TraceConeClassification.CanonicalConvergence, NNReal, nhdsWithin, OfNat.ofNat, Set.Ioi, Function.comp, OAI.TraceConeClassification.ExtendedTrace.scale, OAI.TraceConeClassification.PreservesCanonicalConvergence.net, OAI.TraceConeClassification.TraceConeEquiv.continuous_toFun, OAI.TraceConeClassification.ExtendedTrace.scale_zero_limit, OAI.TraceConeClassification.canonicalConvergence_unique, Eq.mp, congrFun', funext and 1 more
33 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:225 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_finIdeal@path.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem idealOrderIso_finIdeal (τ : ExtendedTrace A) :
    F.idealOrderIso τ.finIdeal = (F.toEquiv τ).finIdeal := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
theorem OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_zeroIdeal line 411
Source documentation
The scalar-infinity limit identifies the literal zero ideals under the same ideal correspondence. No finiteness restriction on the trace is introduced.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalCStarAlgebra, PartialOrder, StarOrderedRing, OAI.TraceConeClassification.TraceConeEquiv, OAI.TraceConeClassification.ExtendedTrace, Eq, OAI.TraceConeClassification.ClosedIdeal, OrderIso, OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso, OAI.TraceConeClassification.ExtendedTrace.zeroIdeal, Equiv, OAI.TraceConeClassification.TraceConeEquiv.toEquiv
Proof uses: OAI.TraceConeClassification.ClosedIdeal.weight_injective, Eq.mpr, OAI.TraceConeClassification.ClosedIdeal.weight, id, congrArg, OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_weight, OAI.TraceConeClassification.CanonicalConvergence, NNReal, Filter.atTop, Function.comp, OAI.TraceConeClassification.ExtendedTrace.scale, OAI.TraceConeClassification.PreservesCanonicalConvergence.net, OAI.TraceConeClassification.TraceConeEquiv.continuous_toFun, OAI.TraceConeClassification.ExtendedTrace.scale_infty_limit, OAI.TraceConeClassification.canonicalConvergence_unique, Eq.mp, congrFun', funext, OAI.TraceConeClassification.TraceConeEquiv.map_scale_all
30 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/TraceIdealTransportSupport.lean:229 (same statement text; different proof or body). Qualify references as OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_zeroIdeal@path.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem idealOrderIso_zeroIdeal (τ : ExtendedTrace A) :
    F.idealOrderIso τ.zeroIdeal = (F.toEquiv τ).zeroIdeal := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace