LocalFreeCornerInputs.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact remaining published premises for one local free-product application. Every field concerns the underlying tracial algebras or their standard Hilbert models; none is an estimate for the operator being tested. The generated algebras, frame, reflection and ordinary word density provide the geometric data.

structure OAI.KadisonSimilarity.TracialCornerGeometry.LocalFreeCornerPublishedInputs line 37
Source documentation
Published local ingredients, specialized to the chosen small corner and test symmetry. The applicability to the actual finite normal free product is kept explicit in the finite-factor assembly.
```
structure LocalFreeCornerPublishedInputs : Prop where
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_corner_from_local_published_inputs line 45

Source documentation

The local conclusion is derived from the published premises and the actual small frame, for every commuting operator with its concrete corner bound. No operator-estimate field occurs in the published bundle.

theorem free_corner_from_local_published_inputs
    (published : G.LocalFreeCornerPublishedInputs)
    (baseExpectation : Nonempty (TracialExpectation G.trace A))
    (hnormal : ∃ N : VonNeumannAlgebra H, G.left.range = N.toStarSubalgebra)
    (hgen : G.FactorsTraciallyGenerate A D)
    (S : RealTracialSequence (G.baseGeometry D).trace)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    (hf : ScalarFree G.trace D A)
    (hsstar : star s = s) (hs0 : G.trace (s : P) = 0)
    (T : H →L[ℂ] H)
    (hTD : ∀ x : D, T.comp (G.left (x : P)) = (G.left (x : P)).comp T)
    {ε : ℝ} (hε : 0 ≤ ε) (hcorner : G.TraceCornerBound D T Q.trace ε) :
…

Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.ScalarFree