CartanSourceSectionCoordinates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed section in the actual source-cell coordinates

theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceSection_sourceCoordinates line 61
Source documentation
The quotient coordinate used by the compact source cell evaluates the same fixed pure-word section used by the metric bridge.
```
theorem TiledProbeChainData.sourceSection_sourceCoordinates
    (hchartN : ∀ v, chartN v = F.ExpN v) (n : ℕ) (y : Y n) :
    σ y.val.1 = F.ExpN (F.N.equiv
      (quotientLinearSection (M.coneWordIdeal C) D.bQ D.lift
        (D.bQ.equivFun.symm (ψ n y).1.val))) := by
…
```
Mentions: OAI.PolycyclicRecognition.quotientLinearSection

theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceSection_eq_fixed_coordinates line 82

Source documentation

Retaining the linear section before selecting the tiling keeps the contact-bridge constants independent of that later selection.

theorem TiledProbeChainData.sourceSection_eq_fixed_coordinates
    (hchartN : ∀ v, chartN v = F.ExpN v)
    (τ : (Fin (finrank ℝ (cartanRootIdeal H ⧸ (M.coneWordIdeal C).toSubmodule)) → ℝ)
      →ₗ[ℝ] cartanRootIdeal H)
    (hτ : (quotientLinearSection (M.coneWordIdeal C) D.bQ D.lift).comp
      D.bQ.equivFun.symm.toLinearMap = τ)
    (n : ℕ) (y : Y n) :
    σ y.val.1 = F.ExpN (F.N.equiv (τ (ψ n y).1.val)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.quotientLinearSection