Rigidity.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Two-chart proof of precisely the holomorphic-conic rigidity step. The analytic construction of the comparison from DN equality is NOT assumed in the main target and is still missing.

def OAI.ElasticityAugmented.diagonalGauge line 12
lemma OAI.ElasticityAugmented.diagonalGauge_mul line 15
lemma OAI.ElasticityAugmented.diagonalGauge_sub line 24
lemma OAI.ElasticityAugmented.diagonalGauge_one line 29
lemma OAI.ElasticityAugmented.matrixD_diagonalGauge line 37
lemma OAI.ElasticityAugmented.matrixD_direction_smul line 42
lemma OAI.ElasticityAugmented.diagonalGauge_smul line 48
lemma OAI.ElasticityAugmented.diagonalGauge_equation line 54
lemma OAI.ElasticityAugmented.diagonalGauge_supported line 61
lemma OAI.ElasticityAugmented.direction_theta_smul line 86
lemma OAI.ElasticityAugmented.thetaGamma_smul line 89
lemma OAI.ElasticityAugmented.transportT_smul line 92
lemma OAI.ElasticityAugmented.transportQ_smul line 96
def OAI.ElasticityConic.chartDiagonal line 110
lemma OAI.ElasticityConic.chartDiagonal_ne_zero line 111
lemma OAI.ElasticityConic.chartTheta_transition line 114
lemma OAI.ElasticityConic.chartMatrix_transition line 118
lemma OAI.ElasticityConic.physical_chart_transition line 126

theorem OAI.ElasticityConic.supported_chart_glue line 137

Source documentation

The projective conic transition law is forced by supported uniqueness; comparisons constructed using unrelated weak subsequences glue exactly.

theorem supported_chart_glue (k r : Fin 2 → Smooth)
    (hr : ∀ q x,(r q : X → ℂ) x≠0) (hk : ∀ q x,(k q : X → ℂ) x≠0)
    (hl : ∀ q x,((k q+r q*r q : Smooth) : X → ℂ) x≠0)
    {K : Set X} (hK : IsCompact K) (G : Bool → ℂ → Matrix (Fin 3) (Fin 3) Smooth)
    (hs : ∀ b z i j,tsupport ((G b z i j-(1 : Matrix (Fin 3) (Fin 3) Smooth) i j : Smooth) : X → ℂ)⊆K)
    (he : ∀ b z,matrixD (chartTheta b z) (G b z)=
      chartMatrix b z (transportT (chartTheta b z) (k 1) (r 1) (hk 1) (hl 1))
        (transportQ (chartTheta b z) (k 1) (r 1) (hr 1) (hk 1) (hl 1))*G b z-
      G b z*chartMatrix b z (transportT (chartTheta b z) (k 0) (r 0) (hk 0) (hl 0))
        (transportQ (chartTheta b z) (k 0) (r 0) (hr 0) (hk 0) (hl 0)))
    (z : ℂ) (hz : z≠0) : G false z=diagonalGauge (chartDiagonal z) (G true z⁻¹) := by
…

Mentions: OAI.ElasticityConic.chartTheta, OAI.ElasticityConic.chartMatrix, OAI.ElasticityConic.chartDiagonal

abbrev OAI.ElasticityRigidity.X line 181
abbrev OAI.ElasticityRigidity.Mat line 182
def OAI.ElasticityRigidity.θ line 184
def OAI.ElasticityRigidity.e line 186
def OAI.ElasticityRigidity.D line 188

lemma OAI.ElasticityRigidity.sphere_function_constant line 192

Source documentation

Two-chart Liouville argument for degree-zero entries.

lemma sphere_function_constant {f g : ℂ → ℂ} (hf : Differentiable ℂ f)
    (hg : ContinuousAt g 0) (hglue : ∀ z : ℂ, z ≠ 0 → f z = g z⁻¹) :
    ∀ z, f z = f 0 := by
…

lemma OAI.ElasticityRigidity.negative_section_zero line 207

Source documentation

The negative-degree transition forces every holomorphic section to vanish.

lemma negative_section_zero {f g : ℂ → ℂ} (hf : Differentiable ℂ f)
    (hg : ContinuousAt g 0) (hglue : ∀ z : ℂ, z ≠ 0 → f z = z⁻¹ * g z⁻¹) :
    ∀ z, f z = 0 := by
…

def OAI.ElasticityRigidity.HolomorphicComparison line 223
Source documentation
The exact chart transition for End(O(-1)² ⊕ O). The two spatial coefficients are expressed in h₁(1,z),h₂(1,z) and h₁(w,1),h₂(w,1).
```
def HolomorphicComparison (G₀ Ginf : X → ℂ → Mat) : Prop :=
…
```
Mentions: OAI.ElasticityRigidity.X, OAI.ElasticityRigidity.Mat
lemma OAI.ElasticityRigidity.diagonal_degree_zero line 231
lemma OAI.ElasticityRigidity.upperright_zero line 243
def OAI.ElasticityRigidity.M line 252
Source documentation
Normal-form connection matrix on the finite chart; q is the bottom-left row in this frame and T the original scalar coefficient.
```
def M (q : X → ℂ → Fin 2 → ℂ) (T : X → ℂ → ℂ) (x : X) (z : ℂ) : Mat :=
…
```
Mentions: OAI.ElasticityRigidity.X, OAI.ElasticityRigidity.Mat
def OAI.ElasticityRigidity.Transport line 255
lemma OAI.ElasticityRigidity.D_zero line 260
lemma OAI.ElasticityRigidity.top_blocks_scalar line 263
lemma OAI.ElasticityRigidity.comparison_scalar_and_dir_zero line 307
lemma OAI.ElasticityRigidity.fderiv_zero_of_chart_dirs line 352

theorem OAI.ElasticityRigidity.comparison_identity line 370

Source documentation

Exact comparison rigidity in the two charts of the projective null conic. The exterior identity assumption is used only at a single exterior point.

theorem comparison_identity {G₀ Ginf : X → ℂ → Mat}
    {q₁ q₂ : X → ℂ → Fin 2 → ℂ} {T₁ T₂ : X → ℂ → ℂ}
    (hG : HolomorphicComparison G₀ Ginf) (hT : Transport G₀ q₁ q₂ T₁ T₂)
    (hs : ∀ z i j, Differentiable ℝ (fun x => G₀ x z i j))
    {x₀ : X} (hext : G₀ x₀ 0 = 1) :
    (∀ x z, G₀ x z = 1) ∧ (∀ x w, Ginf x w = 1) := by
…

Mentions: OAI.ElasticityRigidity.X, OAI.ElasticityRigidity.Mat, OAI.ElasticityRigidity.HolomorphicComparison, OAI.ElasticityRigidity.Transport

theorem OAI.ElasticityRigidity.connections_equal line 416

Source documentation

The comparison equation now yields the equality of connection matrices, without any residual scalar gauge or assumed transport equality.

theorem connections_equal {G₀ Ginf : X → ℂ → Mat}
    {q₁ q₂ : X → ℂ → Fin 2 → ℂ} {T₁ T₂ : X → ℂ → ℂ}
    (hG : HolomorphicComparison G₀ Ginf) (hT : Transport G₀ q₁ q₂ T₁ T₂)
    (hs : ∀ z i j, Differentiable ℝ (fun x => G₀ x z i j))
    {x₀ : X} (hext : G₀ x₀ 0 = 1) :
    ∀ x z, M q₁ T₁ x z = M q₂ T₂ x z := by
…

Mentions: OAI.ElasticityRigidity.X, OAI.ElasticityRigidity.Mat, OAI.ElasticityRigidity.HolomorphicComparison, OAI.ElasticityRigidity.Transport, OAI.ElasticityRigidity.M

def OAI.ElasticityConic.physicalChartMatrix line 445
lemma OAI.ElasticityConic.physicalChartMatrix_regular line 451
lemma OAI.ElasticityConic.physicalChartMatrix_eqOn line 460
lemma OAI.ElasticityConic.chart_transition_scalar line 475
lemma OAI.ElasticityConic.chartTheta_smooth line 481
lemma OAI.ElasticityConic.chartTheta_false line 485

theorem OAI.ElasticityConic.chart_comparison_trivial line 492

Source documentation

The abstract conic rigidity calculation, separated from the lengthy physical coefficient formulas. All analytic matching properties are supplied below by proved supported uniqueness and regularity, not by inverse hypotheses.

theorem chart_comparison_trivial (T : Bool → ℂ → Fin 2 → Smooth)
    (Q : Bool → ℂ → Fin 2 → Fin 3 → Smooth)
    (G : Bool → ℂ → Matrix (Fin 3) (Fin 3) Smooth)
    (hG : ∀ b i j,JointHolomorphic (fun y : X × ℂ => (G b y.2 i j : X → ℂ) y.1))
    (hglue : ∀ z : ℂ,z≠0 → G false z=diagonalGauge (chartDiagonal z) (G true z⁻¹))
    (he : ∀ b z,matrixD (chartTheta b z) (G b z)=
      chartMatrix b z (T b z 1) (Q b z 1)*G b z-G b z*chartMatrix b z (T b z 0) (Q b z 0))
    (x₀ : X) (hbase : matrixEval x₀ (G false 0)=1) : ∀ b z,G b z=1 := by
…

Mentions: OAI.ElasticityConic.JointHolomorphic, OAI.ElasticityConic.chartDiagonal, OAI.ElasticityConic.chartTheta, OAI.ElasticityConic.chartMatrix

theorem OAI.ElasticityConic.supported_physical_holomorphic line 538

Source documentation

Rigidity of the genuine two-chart physical connection. The entire analytic matching input is only separately smooth supported transport; joint smoothness, holomorphy and transition compatibility are conclusions of the transport equations, never additional properties imposed upon CGO weak limits.

theorem supported_physical_holomorphic (k r : Fin 2 → Smooth)
    (hr : ∀ q x,(r q : X → ℂ) x≠0) (hk : ∀ q x,(k q : X → ℂ) x≠0)
    (hl : ∀ q x,((k q+r q*r q : Smooth) : X → ℂ) x≠0)
    {K : Set X} (hK : IsCompact K) (χ : Smooth) (hχ : HasCompactSupport (χ : X → ℂ))
    (hχ1 : ∀ x∈K,(χ : X → ℂ) x=1)
    (hexk : EqOn (k 0 : X → ℂ) (k 1) Kᶜ) (hexr : EqOn (r 0 : X → ℂ) (r 1) Kᶜ)
    (G : Bool → ℂ → Matrix (Fin 3) (Fin 3) Smooth)
    (hs : ∀ b z i j,tsupport ((G b z i j-(1 : Matrix (Fin 3) (Fin 3) Smooth) i j : Smooth) : X → ℂ)⊆K)
    (he : ∀ b z,matrixD (chartTheta b z) (G b z)=
      physicalChartMatrix b z (k 1) (r 1) (hr 1) (hk 1) (hl 1)*G b z-
      G b z*physicalChartMatrix b z (k 0) (r 0) (hr 0) (hk 0) (hl 0)) :
    ∀ b i j,JointHolomorphic (fun y : X × ℂ => (G b y.2 i j : X → ℂ) y.1) := by
…

Mentions: OAI.ElasticityConic.chartTheta, OAI.ElasticityConic.physicalChartMatrix, OAI.ElasticityConic.JointHolomorphic

theorem OAI.ElasticityConic.physical_conic_connections_equal line 564
lemma OAI.ElasticityConic.chart_covers_null line 598
Source documentation
The two affine charts exhaust every nonzero complex characteristic direction, up to its nonzero scalar. No arbitrary choice of a square root is needed.
```
lemma chart_covers_null (v : C3) (hv : v≠0) (hn : null v) :
    ∃ (b : Bool) (z c : ℂ), c≠0 ∧ v=c • chartTheta b z := by
…
```
Mentions: OAI.ElasticityConic.C3, OAI.ElasticityConic.null, OAI.ElasticityConic.chartTheta
lemma OAI.ElasticityConic.chart_bottom_equal line 646
lemma OAI.ElasticityRecovery.T_smul line 670
lemma OAI.ElasticityRecovery.Q_smul line 673

theorem OAI.ElasticityAugmented.restricted_transports_of_chart_equal line 681

Source documentation

Equality of the actual conic connections is precisely sufficient for the restricted physical transports used by Lamé coefficient recovery.

theorem restricted_transports_of_chart_equal (m k : Fin 2 → X → ℝ)
    (hm : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (m q)) (hk : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (k q))
    (hmp : ∀ q x,0 < m q x) (hkp : ∀ q x,0 < k q x)
    (he : ∀ b z,
      chartMatrix b z
        (transportT (chartTheta b z) (smoothOfReal (k 0) (hk 0)) (positiveRoot (m 0) (hm 0) (hmp 0))
          (fun x => Complex.ofReal_ne_zero.mpr (hkp 0 x).ne') (real_sum_nonzero (m 0) (k 0) (hm 0) (hk 0) (hmp 0) (hkp 0)))
        (transportQ (chartTheta b z) (smoothOfReal (k 0) (hk 0)) (positiveRoot (m 0) (hm 0) (hmp 0))
          (positiveRoot_nonzero (m 0) (hm 0) (hmp 0)) (fun x => Complex.ofReal_ne_zero.mpr (hkp 0 x).ne')
          (real_sum_nonzero (m 0) (k 0) (hm 0) (hk 0) (hmp 0) (hkp 0)))=
      chartMatrix b z
        (transportT (chartTheta b z) (smoothOfReal (k 1) (hk 1)) (positiveRoot (m 1) (hm 1) (hmp 1))
…

Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.transportT, OAI.ElasticityAugmented.smoothOfReal, OAI.ElasticityAugmented.positiveRoot, OAI.ElasticityAugmented.real_sum_nonzero, OAI.ElasticityAugmented.transportQ, OAI.ElasticityAugmented.positiveRoot_nonzero

lemma OAI.Elasticity.physicalChartMatrix_congr_k line 733

theorem OAI.Elasticity.dn_global_coefficients_equal line 744

Source documentation

The global transport-matching implication for a genuine common exterior. Its only inverse-data hypothesis is equality of the physical DN maps.

theorem dn_global_coefficients_equal {Ω : Set X} (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω)
    (lam m : Fin 2 → X → ℝ)
    (hl : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (lam q)) (hm : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (m q))
    (hp : ∀ q x,0 < m q x ∧ 0<3*lam q x+2*m q x)
    (hcll : ∀ q,ExteriorConstant (smoothOfReal (lam q) (hl q)))
    (hclm : ∀ q,ExteriorConstant (smoothOfReal (m q) (hm q)))
    (he : ∀ x∉Ω,lam 0 x=lam 1 x ∧ m 0 x=m 1 x)
    (hDN : DN Ω (lam 0) (m 0)=DN Ω (lam 1) (m 1)) :
    lam 0=lam 1 ∧ m 0=m 1 := by
…

Mentions: OAI.Elasticity.X, OAI.Elasticity.DN