FreeCornerApplication.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Apply the proved free-corner theorem using the chosen matrix frame, its containing half projection, and the actual L²-generated test algebras. All ordinary generation and support identities are derived here.

def OAI.KadisonSimilarity.TracialCornerGeometry.smallFrameCompressionInput line 45
Source documentation
The elementary compression model on the actual half corner.
```
def smallFrameCompressionInput (hτ : G.trace 1 = 1) : Prop :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.smallFrameCompressionInput_proved line 57
Source documentation
The constructed reduced-word model supplies the half-corner input.
```
theorem smallFrameCompressionInput_proved (hτ : G.trace 1 = 1) :
    G.smallFrameCompressionInput A D Q s hτ := by
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_corner_from_smallFrame line 66

Source documentation

The free-corner estimate with the matrix frame and both generated algebras fixed by construction. The remaining premises are the local published word, spectral, comparison, and cyclic-implementation inputs.

theorem free_corner_from_smallFrame
    (hgen : G.FactorsTraciallyGenerate A D) (hfaithful : Function.Injective G.vector)
    (hext : ∀ j, G.MatrixConjugationExtensionInput D (M.embedding j) A)
    (S : RealTracialSequence (G.baseGeometry D).trace)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    (hτ : G.trace 1 = 1) (hf : ScalarFree G.trace D A)
    (words : RicardXuWordDecompositionInput G A D)
    (creation : RicardXuCreationInput G A D)
    (support : TracialRightSupportInput (fun a => (G.trace a).re)
      (Q.frame.corner : P) A)
    (comparison : FiniteFactorProjectionComparison (fun a => (G.trace a).re))
    (published : PublishedDerivationInputs.{u,v} (CStarCorner (Q.frame.corner : P)
…

Mentions: OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.RicardXuWordDecompositionInput, OAI.KadisonSimilarity.RicardXuCreationInput, OAI.KadisonSimilarity.TracialRightSupportInput, OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.CStarCorner