ProbeSectionRestrictions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The two probe restrictions in the same section coordinates

The first path controls the quotient orbit point in the base frame. The absorbed bridge controls the ideal residual in the tile-anchor frame. These restrictions apply simultaneously to each point of the right cell.

def OAI.PolycyclicRecognition.exponentialIdealKernelRegion line 20
theorem OAI.PolycyclicRecognition.exponential_section_residual_mem line 40
Source documentation
An actual ideal-times-section factorization places its residual in the intrinsic kernel region. This is the ideal restriction used in packing.
```
theorem exponential_section_residual_mem
    (hzeroQ : chartQ (eQ 0) = 1) (I : Set U) {n : N}
    (hn : ∃ i ∈ I, ∃ q : V ⧸ U.toSubmodule,
      n = chartN (eN (i : V)) * chartN (eN (quotientLinearSection U bQ lift q))) :
    quotientSectionResidual π
      (exponentialQuotientSection U bQ lift eN eQ chartN chartQ)
      (exponentialQuotientSection_rightInverse U bQ lift hlift eN eQ chartN chartQ π hπ) n ∈
        exponentialIdealKernelRegion U π (chartN ∘ eN) I := by
…
```
Mentions: OAI.PolycyclicRecognition.quotientLinearSection, OAI.PolycyclicRecognition.quotientSectionResidual, OAI.PolycyclicRecognition.exponentialQuotientSection, OAI.PolycyclicRecognition.exponentialQuotientSection_rightInverse, OAI.PolycyclicRecognition.exponentialIdealKernelRegion

theorem OAI.PolycyclicRecognition.thickened_probe_section_restriction line 55

Source documentation

The containing product region is valid for the actual thickened endpoints and their fixed lifts, with arbitrary quotient translation.

theorem thickened_probe_section_restriction
    (hzeroQ : chartQ (eQ 0) = 1)
    (φ : D →* MulAut N) (ι : N →* G) (κ : D →* G)
    (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ n d q, act (ι n * κ d) q = π n * α d q)
    (base anchor endpoint : G) (p : N × D) (n₀ : N) (d₀ : D)
    (hp : anchor⁻¹ * endpoint = ι p.1 * κ p.2)
    (hframe : anchor⁻¹ * base = ι n₀ * κ d₀)
    (cell : Set (N × D)) (T : Set Q) (I : Set U) (B : Set D)
    (hfirst : ∀ z ∈ cell, act (base⁻¹ * (endpoint * (ι z.1 * κ z.2))) 1 ∈ T)
    (hideal : ∀ z ∈ cell, ∃ i ∈ I, ∃ q : V ⧸ U.toSubmodule,
…