CartanSamplingParameters.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Concrete parameters for the neighboring-sheet sampling argument

def OAI.PolycyclicRecognition.CartanWordModel.samplingPolytope line 22
Source documentation
The actual normalized halfspaces used to sample the root ideal.
```
def samplingPolytope : Set W :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.sampling_weight_ne_zero line 25
theorem OAI.PolycyclicRecognition.CartanWordModel.isCompact_samplingPolytope line 35
theorem OAI.PolycyclicRecognition.CartanWordModel.sampling_weightSupport_eq line 38
theorem OAI.PolycyclicRecognition.CartanWordModel.sampling_weightSupport_pos line 44

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sampling_gap line 52

Source documentation

The finite word list supplies positive lower and upper widths and a strict concentration gap. These constants are chosen from the actual sampling polytope rather than assumed as geometric inputs.

theorem exists_sampling_gap [Nonempty (Fin M.letterCount)] :
    ∃ lo hi c : ℝ, 0 < lo ∧ 0 < hi ∧ 0 < c ∧
      (∀ w : M.wordList, lo ≤ M.boxCost T hunimod eW
        (M.samplingPolytope T hunimod eW) w ∧
        M.boxCost T hunimod eW (M.samplingPolytope T hunimod eW) w ≤ hi) ∧
      (M.bound : ℝ) * hi < c * lo := by
…

def OAI.PolycyclicRecognition.threePolarRadii line 91
Source documentation
Source, reverse anchor, and within-tile radii, in that order.
```
def threePolarRadii (ε : ℝ) : Fin 3 → ℝ := ![2 * ε / 3, ε, ε / 3]
```

def OAI.PolycyclicRecognition.polarSamplingTemplates line 94

Source documentation

The exact translated templates used by the three probe chains.

def polarSamplingTemplates {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (K : ProperCone ℝ (W →L[ℝ] ℝ)) (ε : ℝ) (w : W) (k : Fin 3) : Set W :=
…

def OAI.PolycyclicRecognition.samplingHeightDomain line 99

Source documentation

The open profile-height domain retains the strict facet inequalities.

def samplingHeightDomain {W I : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (α : I → W →L[ℝ] ℝ) (a : ℝ) : Set W := {w | ∀ i, α i w < a * ‖α i‖}

theorem OAI.PolycyclicRecognition.exists_three_polar_sampling_templates line 104

Source documentation

All three radii and the contact point can be fixed before choosing the chart enlargement. Every translated template has strict facet slack.

theorem exists_three_polar_sampling_templates
    {W I : Type*} [NormedAddCommGroup W] [InnerProductSpace ℝ W]
    [FiniteDimensional ℝ W] [Fintype I]
    (α : I → W →L[ℝ] ℝ) (hne : ∀ i, α i ≠ 0)
    (i₀ : I) (K : ProperCone ℝ (W →L[ℝ] ℝ)) (hK : α i₀ ∈ K)
    {c : ℝ} (hc : 0 ≤ c) :
    ∃ (p : W) (ε δ₀ : ℝ), α i₀ p = ‖α i₀‖ ∧ 0 < ε ∧ 0 < δ₀ ∧
      0 < threePolarRadii ε 2 ∧ threePolarRadii ε 2 < threePolarRadii ε 0 ∧
      threePolarRadii ε 0 < threePolarRadii ε 1 ∧
      ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
        0 < 1 - (c + 1) * δ ∧
        ∀ k : Fin 3, ∀ z ∈ conePolarTemplate K, ∀ i,
…

Mentions: OAI.PolycyclicRecognition.threePolarRadii, OAI.PolycyclicRecognition.conePolarTemplate

theorem OAI.PolycyclicRecognition.polar_sampling_template_geometry line 137

Source documentation

The facet inequalities give precisely the compact, convex templates inside one open convex profile domain required by both path construction and raw concentration. The domain is also inside the original sampling polytope, which supplies the common coordinate bound.

theorem polar_sampling_template_geometry
    {W I : Type*} [NormedAddCommGroup W] [InnerProductSpace ℝ W]
    [FiniteDimensional ℝ W] [Fintype I]
    (α : I → W →L[ℝ] ℝ) (K : ProperCone ℝ (W →L[ℝ] ℝ))
    (p : W) (ε δ c : ℝ) (hc : 0 ≤ c) (hδ : 0 < δ)
    (hfactor : 0 < 1 - (c + 1) * δ)
    (hfacet : ∀ k : Fin 3, ∀ z ∈ conePolarTemplate K, ∀ i,
      α i ((1 - (c + 1) * δ) • p + threePolarRadii ε k • z) <
        (1 - c * δ) * ‖α i‖) :
    let w := (1 - (c + 1) * δ) • p
…

Mentions: OAI.PolycyclicRecognition.conePolarTemplate, OAI.PolycyclicRecognition.threePolarRadii