TubeProjection.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.FiniteBins.Active line 19
Source documentation
Only bins meeting the original good set require a reference.
```
def Active := {c : C // ∃ x∈G,P x=c}
```
def OAI.SmoothObstruction.FiniteBins.Fiber line 20
def OAI.SmoothObstruction.FiniteBins.reference line 22
instance OAI.SmoothObstruction.FiniteBins.(instance at line 28) line 28

theorem OAI.SmoothObstruction.ManifoldCoordinates.finite_starting_references line 43

Source documentation

The original genuine finite-window estimates produce all starting-bin thresholds simultaneously. Only finite bin reference choices survive: no measurable choice of frame, exponent, or orbit chart code is used.

theorem finite_starting_references (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 → ι) (P : M → C) (G : Set M)
        (n N : ℕ) (B R h g : ℝ) (A : ∀ x:G,BilateralGauge I S a c n B R x),
        (∀ y,y∈K (c y)) → N≤n →
        (∀ x y,P x=P y → c x=c y) →
        (∀ x∈G,I.IsInteriorPoint x) →
        (∀ x y,P x=P y → ‖(extChartAt I (a (c y))) x-(extChartAt I (a (c y))) y‖≤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

theorem OAI.SmoothObstruction.ManifoldCoordinates.finite_endpoint_references line 102

Source documentation

The endpoint reference is indexed only by starting and endpoint coarse bins. The common starting rank and threshold are retained unchanged. Inactive endpoint keys are not part of the construction or the partition count.

theorem finite_endpoint_references (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 → ι) (P : M → C) (G : Set M) (n N : ℕ) (B R h g : ℝ)
        (γ : C → ℝ) (T : G → Finset (Fin d))
        (A : ∀ x:G,BilateralGauge I S a c n B R x),
        (∀ y,y∈K (c y)) → N≤n →
        (∀ x y,P x=P y → c x=c y) →
        (∀ x∈G,I.IsInteriorPoint (S^[n] x)) →
        (∀ x y,P x=P y → ‖(extChartAt I (a (c y))) x-(extChartAt I (a (c y))) y‖≤h) →
        C₁^N*h≤r → 0≤h →
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.reverse line 165
Source documentation
Time reversal keeps the original gauge and negates its rates; it is not an independently selected certificate.
```
noncomputable def BilateralGauge.reverse (A : BilateralGauge I S a c n B R x) :
    BilateralGauge I S.symm a c n B R x where
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge
lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.reverse_forwardSpace line 184
lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.backwardSpace_zero line 189
Source documentation
The two true middle subspaces agree exactly.
```
lemma BilateralGauge.backwardSpace_zero (A : BilateralGauge I S a c n B R x)
    (T : Finset (Fin d)) :
    A.backwardSpace I S a c 0 T=A.forwardSpace I S a c 0 T := by
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge
def OAI.SmoothObstruction.FiniteBins.key line 198
def OAI.SmoothObstruction.FiniteBins.extend line 199
lemma OAI.SmoothObstruction.FiniteBins.extend_active line 202
lemma OAI.SmoothObstruction.FiniteBins.extend_key line 207

theorem OAI.SmoothObstruction.ManifoldCoordinates.bilateral_endpoint_references line 223

Source documentation

All future and past reference projectors are selected from the same original good inputs. Their labels are exactly (starting bin, endpoint bin). Time reversal is the original bilateral gauge, so its endpoint rank is the complementary original rank, not a new threshold or a separately chosen frame.

theorem bilateral_endpoint_references (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 DF rB CB DB : ℝ,0<rF ∧ 1≤CF ∧ 1≤DF ∧ 0<rB ∧ 1≤CB ∧ 1≤DB ∧
      ∀ (c : M → ι) (P : M → C) (G : Set M) (n N : ℕ) (B R h g : ℝ)
        (γ : C → ℝ) (T : G → Finset (Fin d))
        (A : ∀ x:G,BilateralGauge I S a c n B R x),
        (∀ y,y∈K (c y)) → N≤n →
        (∀ x y,P x=P y → c x=c y) →
        (∀ x∈G,I.IsInteriorPoint (S^[n] x) ∧ I.IsInteriorPoint (S.symm^[n] x)) →
        (∀ x y,P x=P y → ‖(extChartAt I (a (c y))) x-(extChartAt I (a (c y))) y‖≤h) →
        CF^N*h≤rF → CB^N*h≤rB → 0≤h →
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

def OAI.SmoothObstruction.ManifoldCoordinates.fastSet line 294
def OAI.SmoothObstruction.ManifoldCoordinates.slowSet line 297
lemma OAI.SmoothObstruction.ManifoldCoordinates.slowSet_eq_compl line 300

theorem OAI.SmoothObstruction.ManifoldCoordinates.finite_references line 308

Source documentation

Simultaneous starting and two endpoint references derived from the ORIGINAL bilateral good gauges. All choices are finite bin choices: the pointwise frames and rate lists are never made into a measurable refinement.

theorem finite_references (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₁ r₂ C₂ D r₃ C₃ D₃ r₄ C₄ D₄ : ℝ,
      0<r₁ ∧ 1≤C₁ ∧ 0<r₂ ∧ 1≤C₂ ∧ 1≤D ∧
      0<r₃ ∧ 1≤C₃ ∧ 1≤D₃ ∧ 0<r₄ ∧ 1≤C₄ ∧ 1≤D₄ ∧
      ∀ (c : M → ι) (P : M → C) (G : Set M) (n N : ℕ) (B R h g : ℝ)
        (A : ∀ x:G,BilateralGauge I S a c n B R x),
        (∀ y,y∈K (c y)) → N≤n →
        (∀ x y,P x=P y → c x=c y) →
        (∀ x∈G,I.IsInteriorPoint x) →
        (∀ x y,P x=P y → ‖(extChartAt I (a (c y))) x-(extChartAt I (a (c y))) y‖≤h) →
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

theorem OAI.SmoothObstruction.ManifoldCoordinates.finite_starting_references_uniform line 418
theorem OAI.SmoothObstruction.ManifoldCoordinates.finite_endpoint_references_uniform line 473
theorem OAI.SmoothObstruction.ManifoldCoordinates.bilateral_endpoint_references_uniform line 533
theorem OAI.SmoothObstruction.ManifoldCoordinates.finite_references_uniform line 603

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_tube_data line 717

Source documentation

All the one-step tube/Taylor hypotheses used by the boundary-value solver follow from actual one-step smoothness on the finite compact atlas. The only variable-domain input is the literal avoidance of the boundary.

theorem actual_tube_data (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 : ℝ,0<r ∧ 1≤C ∧ ∀ (i j : ι) (x : M) (δ : ℝ),
      x∈K i → S x∈K j → 0≤δ → δ≤r →
      closedBall ((extChartAt I (a i)) x) δ⊆interior (range I) →
      closedBall ((extChartAt I (a i)) x) δ⊆(extChartAt I (a i)).target ∧
      closedBall ((extChartAt I (a i)) x) δ⊆domainU I S (a i) (a j) ∧
      ∀ y∈closedBall ((extChartAt I (a i)) x) δ,
        ContDiffAt ℝ ∞ (localMap I S (a i) (a j)) y ∧
        ‖fderiv ℝ (localMap I S (a i) (a j)) y‖≤C ∧
        ‖fderiv ℝ (localMap I S (a i) (a j)) y-
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domainU, OAI.SmoothObstruction.ManifoldCoordinates.localMap

lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.forward_space line 761
lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.backward_space line 767
lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.forward_fast line 773
lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.backward_fast line 780
def OAI.SmoothObstruction.ManifoldCoordinates.originalTube line 789
Source documentation
An old tube tests the candidate in the original input's selected charts. The candidate is not required to belong to the good set.
```
def originalTube (δ : ℝ) (x z : M) : Prop :=
…
```
def OAI.SmoothObstruction.ManifoldCoordinates.originalEndpoint line 795
Source documentation
Fixed endpoint projection, still based on the old input's endpoint chart.
```
def originalEndpoint (V : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (x z : M) : Prop :=
…
```
lemma OAI.SmoothObstruction.ManifoldCoordinates.projection_diff_iff line 809

theorem OAI.SmoothObstruction.ManifoldCoordinates.original_gauged_join line 826

Source documentation

An actual two-sided joining. The uniform geometry is chosen BEFORE the window, good gauges, cells, thresholds, or endpoint ranks. Every tube and Taylor hypothesis is derived here from the source finite atlas; the only tube-domain condition retained is the literal avoidance of the manifold boundary.

theorem original_gauged_join (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 : ℝ,0<r₀ ∧ 1≤C ∧
      ∀ (c : M → ι) (n : ℕ) (B R ε γ g α r δ : ℝ) (q x y : M)
        (A₀ : BilateralGauge I S a c n B R q)
        (Ax : BilateralGauge I S a c n B R x)
        (Ay : BilateralGauge I S a c n B R y)
        (T₀ Tx Ty : Finset (Fin d))
        (V W : Submodule ℝ (EuclideanSpace ℝ (Fin d))),
        (∀ v,v∈K (c v)) → c x=c y → I.IsInteriorPoint x → I.IsInteriorPoint y →
        Module.finrank ℝ (Ax.forwardSpace I S a c n Tx)=Module.finrank ℝ V →
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge