ManifoldMatching.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SmoothObstruction.ManifoldCoordinates.realize_array line 25
Source documentation
An exact finite coordinate solution lying in the original chart targets is a genuine manifold orbit, also in a half-space model.
```
theorem realize_array (S : Diffeomorph I I M M ∞) {n : ℕ}
    (a : Fin (n+1) → M) (u : Fin (n+1) → E (d:=d))
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.E
theorem OAI.SmoothObstruction.ManifoldCoordinates.realize_bilateral_array line 65
Source documentation
Matching the time-zero coordinate realizes the TWO-sided exact arrays as one actual orbit. In particular no pair of unrelated local branches is substituted for the smooth switch.
```
theorem realize_bilateral_array (S : Diffeomorph I I M M ∞) {n : ℕ}
    (a b : Fin (n+1) → M) (u v : Fin (n+1) → E (d:=d))
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.E
theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_join_unique line 106
Source documentation
The authentic local-coordinate nonlinear boundary construction gives ONE actual point of the manifold, with both orbit halves and the fixed terminal equations. The ball-domain conditions keep every inverse chart and every one-step expression inside the ORIGINAL manifold.
```
theorem actual_join_unique (S : Diffeomorph I I M M ∞) {n : ℕ}
    (a b : Fin (n+1) → M) (x y : M) (hab : a 0=b 0)
    (hx : ∀ t : Fin (n+1),S^[t.val] x∈(chartAt H (a t)).source)
    (hy : ∀ t : Fin (n+1),S.symm^[t.val] y∈(chartAt H (b t)).source)
    (A₁ A₂ : Evolution (E (d:=d))) (B₁ : Splitting A₁) (B₂ : Splitting A₂)
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.E
lemma OAI.SmoothObstruction.ShortBin.Gauge.evolution_step line 275
lemma OAI.SmoothObstruction.ShortBin.Gauge.unweighted line 282

theorem OAI.SmoothObstruction.ShortBin.gauge_boundary_control line 292

Source documentation

All the finite-interval linear boundary hypotheses are produced from raw common-bin gauge comparisons and fixed endpoint projections. The norm of the matching inverse is a middle-time cost, and the endpoint correction retains threshold cancellation, including a positive slow threshold.

theorem gauge_boundary_control (A₀ A Z : Gauge d n K) (S₀ S T : Finset (Fin d))
    (V W : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
    (hdV : Module.finrank ℝ ((A.splitting S).fast n).range=Module.finrank ℝ V)
    (hdW : Module.finrank ℝ ((Z.splitting T).fast n).range=Module.finrank ℝ W)
    (hcV : ‖((A.splitting S).fast n).range.starProjection-V.starProjection‖≤1/2)
    (hcW : ‖((Z.splitting T).fast n).range.starProjection-W.starProjection‖≤1/2)
    {ε γ g : ℝ} (hε : 0≤ε) (hεhalf : ε≤1/2)
    (hdS : S₀.card=S.card) (hdT : S₀ᶜ.card=T.card)
    (hcS : ‖(A₀.space S₀).starProjection-(A.space S).starProjection‖≤ε)
    (hcT : ‖(A₀.space S₀ᶜ).starProjection-(Z.space T).starProjection‖≤ε)
    (hsmall : Real.exp (2*K)*(2*ε)≤1/2)
    (hsA : ∀ j∈S,A.lam j≤γ-g) (hfA : ∀ j∈Sᶜ,γ+g≤A.lam j)
…

Mentions: OAI.SmoothObstruction.ShortBin.Gauge

def OAI.SmoothObstruction.ShortBin.bvpGrowth line 333
def OAI.SmoothObstruction.ShortBin.bvpInverseBound line 334
lemma OAI.SmoothObstruction.ShortBin.bvpGrowth_ge_two line 338
lemma OAI.SmoothObstruction.ManifoldCoordinates.interior_iterate line 351

lemma OAI.SmoothObstruction.ManifoldCoordinates.gauge_actual_step line 361

Source documentation

The long gauge equations identify every step of the evolution with an ACTUAL coordinate derivative.

lemma gauge_actual_step (S : Diffeomorph I I M M ∞) (a b x : M)
    {n : ℕ} {K : ℝ} (A : ShortBin.Gauge d n K) (t : ℕ)
    (hx : x∈(chartAt H a).source) (hSx : S x∈(chartAt H b).source)
    (hint : I.IsInteriorPoint x)
    (hEq : (Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm (coord I S a b x)*A.U t=
…

Mentions: OAI.SmoothObstruction.ShortBin.Gauge, OAI.SmoothObstruction.ManifoldCoordinates.coord

theorem OAI.SmoothObstruction.ManifoldCoordinates.gauged_join_unique line 374

Source documentation

Actual nonlinear joining, now with ALL linear matching/inverse/kernel hypotheses proved from the genuine gauges and the common-bin comparisons. No boundary inverse, complementary middle space or endpoint graph is assumed.

theorem gauged_join_unique (Smap : Diffeomorph I I M M ∞) {n : ℕ}
    (a b : Fin (n+1) → M) (x y : M) (hab : a 0=b 0)
    (hx : ∀ t : Fin (n+1),Smap^[t.val] x∈(chartAt H (a t)).source)
    (hy : ∀ t : Fin (n+1),Smap.symm^[t.val] y∈(chartAt H (b t)).source)
    (hintx : I.IsInteriorPoint x) (hinty : I.IsInteriorPoint y)
    {K ε γ g α : ℝ} (A₀ A Z : Gauge d n K) (S₀ S T : Finset (Fin d))
    (V W : Submodule ℝ (E (d:=d)))
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.E

theorem OAI.SmoothObstruction.FiniteGreen.Matching.genuine_initial_error line 506

Source documentation

A genuine nonlinear coordinate solution satisfies the exact boundary residual equation, hence the sharp ideal-exchange estimate.

theorem genuine_initial_error
    (L : (B₁.initialSpace×B₂.initialSpace) ≃L[ℝ] E)
    (hL : ∀ x,L x=(x.1:E)-(x.2:E))
    {K P ε κ Q C δ : ℝ} (hK : ‖L.symm.toContinuousLinearMap‖≤K)
    (hP : 0≤P) (hε : 0≤ε) (hκ : 0≤κ) (hC : 0≤C)
    (hsmall : ‖L.symm.toContinuousLinearMap.comp (correction C₁ C₂)‖≤1/2)
    (hc₁ : ‖B₁.initialSpace.starProjection-(B₀.slow 0).range.starProjection‖≤ε)
    (hc₂ : ‖B₂.initialSpace.starProjection-(B₀.fast 0).range.starProjection‖≤ε)
    (hk₁ : ‖C₁.kernel‖≤κ) (hk₂ : ‖C₂.kernel‖≤κ)
    (hs : ‖B₀.slow 0‖≤P) (hf : ‖B₀.fast 0‖≤P)
    (f₁ : Fin n₁ → E → E) (f₂ : Fin n₂ → E → E)
    (x₁ : Fin (n₁+1) → E) (x₂ : Fin (n₂+1) → E)
…

Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.correction

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_join_ideal line 579
Source documentation
The authentic local-coordinate nonlinear boundary construction gives ONE actual point of the manifold, with both orbit halves and the fixed terminal equations. The ball-domain conditions keep every inverse chart and every one-step expression inside the ORIGINAL manifold.
```
theorem actual_join_ideal (S : Diffeomorph I I M M ∞) {n : ℕ}
    (a b : Fin (n+1) → M) (x y : M) (hab : a 0=b 0)
    (hx : ∀ t : Fin (n+1),S^[t.val] x∈(chartAt H (a t)).source)
    (hy : ∀ t : Fin (n+1),S.symm^[t.val] y∈(chartAt H (b t)).source)
    (A₁ A₂ : Evolution (E (d:=d))) (B₁ : Splitting A₁) (B₂ : Splitting A₂)
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.E
theorem OAI.SmoothObstruction.ManifoldCoordinates.gauged_join_ideal line 781
lemma OAI.SmoothObstruction.ManifoldCoordinates.coord_refl_same line 933
def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.forward line 939
def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.backward line 944

theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_genuine_bin_splitting line 952

Source documentation

The common-bin spaces now belong to the ORIGINAL good bilateral gauges. All carried intermediate charts have disappeared from the conclusion. Only initial coarse-bin coordinates are used, so no orbit-code partition appears.

theorem uniform_genuine_bin_splitting (hclosed : IsClosed (range I))
    (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
    ∃ rF CF rB CB D : ℝ,0 < rF ∧ 1 ≤ CF ∧ 0 < rB ∧ 1 ≤ CB ∧ 1 ≤ D ∧
      ∀ (c : M → ι) (J : Type*) (x : J → M) (e : J)
        (n N : ℕ) (B R h g : ℝ) (A : ∀ i,BilateralGauge I S a c n B R (x i)),
        (∀ y,y∈K (c y)) → N ≤ n → (∀ i,c (x i)=c (x e)) →
        (∀ i,I.IsInteriorPoint (x i)) →
        (∀ i,‖(extChartAt I (a (c (x e)))) (x i)-
          (extChartAt I (a (c (x e)))) (x e)‖ ≤ h) →
        CF^N*h ≤ rF → CB^N*h ≤ rB → 0 < g →
        Real.exp (-2*g*N+4*(B+Real.log D)) ≤ 1/2 →
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.forwardSpace line 1027
Source documentation
Spaces of the genuine long-window gauge in its original endpoint chart.
```
noncomputable def BilateralGauge.forwardSpace (S : Diffeomorph I I M M ∞)
    (a : ι → M) (c : M → ι) {n : ℕ} {B R : ℝ} {x : M}
    (A : BilateralGauge I S a c n B R x) (t : ℕ) (T : Finset (Fin d)) :=
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge
def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.backwardSpace line 1032

theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_original_endpoint_fast_comparison line 1040

Source documentation

Endpoint-bin comparison with NO carried basis or extra threshold in the conclusion. The reference is chosen among original certificates reaching the same endpoint bin from a fixed starting bin.

theorem uniform_original_endpoint_fast_comparison (hclosed : IsClosed (range I))
    (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
    ∃ r C₁ D : ℝ,0<r ∧ 1≤C₁ ∧ 1≤D ∧
      ∀ (c : M → ι) (J : Type*) (x : J → M) (e : J)
        (n N : ℕ) (B R h γ g : ℝ) (T : J → Finset (Fin d))
        (A : ∀ i,BilateralGauge I S a c n B R (x i)),
        (∀ y,y∈K (c y)) → N≤n →
        (∀ i,c (S^[n] (x i))=c (S^[n] (x e))) →
        (∀ i,I.IsInteriorPoint (S^[n] (x i))) →
        (∀ i,‖(extChartAt I (a (c (S^[n] (x e))))) (S^[n] (x i))-
          (extChartAt I (a (c (S^[n] (x e))))) (S^[n] (x e))‖≤h) →
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge