CartanTiledOffsetRates.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Matching the actual source partition count to the target exponent

theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.count_le_offset_rate line 37

Source documentation

The stored tile count has exactly the source-minus-target exponent, including when the transformed cone has a different ideal dimension.

theorem PolarTiledSamplerData.count_le_offset_rate
    (ExpI : M.coneWordIdeal C → I) (ι : I →* F.N.carrier)
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
    {ε : ℝ} (hε : 0 < ε) (β : M.ConeIdealBases C)
    (hβ : M.IsMaximizingConeIdealBasis C bI (M.polarProbeWidths T hunimod eW K) β)
    (R : ℝ) (scale : ℕ → ℝ) (φ : ℕ → I ≃ₜ* I)
    (D : M.PolarTiledSamplerData T F hunimod eW K ExpI ι bN ε β R scale φ)
    (A : templateSymmetryGroup (M.supportIn T hunimod eW))
    (bI' : Basis (Fin (finrank ℝ
      (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A.val)))))
      ℝ (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A.val))))
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage, OAI.PolycyclicRecognition.transformedPolarCone