SelectedOrdinaryOrbit.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.SelectedOrdinaryOrbit.first line 19
abbrev OAI.LittleFinitistic.SelectedOrdinaryOrbit.ordinary line 20
def OAI.LittleFinitistic.SelectedOrdinaryOrbit.firstIso line 23
Source documentation
The source's first-block localization is the actual selected exact inflation.
```
def firstIso : first ≅ SelectedFirstBlockFamily.derivedInflation :=
…
```
Mentions: OAI.LittleFinitistic.SelectedOrdinaryOrbit.first, OAI.LittleFinitistic.SelectedFirstBlockFamily.derivedInflation
def OAI.LittleFinitistic.SelectedOrdinaryOrbit.firstStalk line 26
def OAI.LittleFinitistic.SelectedOrdinaryOrbit.nativeIso line 35
Source documentation
Both tensor presentations use the identical Q_X and signed finite total.
```
def nativeIso : ordinary ≅ SelectedBarComparison.native :=
…
```
Mentions: OAI.LittleFinitistic.SelectedOrdinaryOrbit.ordinary, OAI.LittleFinitistic.SelectedBarComparison.native
def OAI.LittleFinitistic.SelectedOrdinaryOrbit.shiftedIso line 40
Source documentation
The source's shifted P[b] tensor is the concrete selecting shifted model.
```
def shiftedIso : OrdinarySimulation.shiftedDerivedTensor SelectedRectification.bimodule b length ≅
    SelectedShiftedRealization.G :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensor, OAI.LittleFinitistic.SelectedRectification.bimodule, OAI.LittleFinitistic.SelectedShiftedRealization.G
def OAI.LittleFinitistic.SelectedOrdinaryOrbit.barPower line 46
Source documentation
Every ordinary iterate on the selected first-block stalk is the original bar iterate.
```
def barPower (Y : FiniteSelectionFamily.S.{0}) (r : ℕ) :
    (ordinary.obj^[r]) (SelectedFirstBlockFamily.derived Y) ≅ SelectedBaseIterates.object Y r :=
…
```
Mentions: OAI.LittleFinitistic.SelectedFirstBlockFamily.derived, OAI.LittleFinitistic.SelectedBaseIterates.object
def OAI.LittleFinitistic.SelectedOrdinaryOrbit.evenIteration line 51
Source documentation
Exact Section 5 even-iteration formula, with both presentation distinctions discharged.
```
def evenIteration (Y : FiniteSelectionFamily.S.{0}) (j : ℕ) :
    SelectedBaseIterates.object Y (2*j) ≅
      first.obj ((SelectedShiftedRealization.G.obj^[j]) (FiniteSelectionFamily.derived Y)) :=
…
```
Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object, OAI.LittleFinitistic.FiniteSelectionFamily.derived
theorem OAI.LittleFinitistic.SelectedOrdinaryOrbit.isZero_iff line 60
Source documentation
Every even original-X iterate is zero exactly at the original selection stopping time.
```
theorem isZero_iff (Y : FiniteSelectionFamily.S.{0}) (j : ℕ) :
    IsZero (SelectedBaseIterates.object Y (2*j)) ↔ Subsingleton (selectionIterate Y.val j) :=
…
```
Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object, OAI.LittleFinitistic.selectionIterate
theorem OAI.LittleFinitistic.SelectedOrdinaryOrbit.extinction line 68
Source documentation
Actual extinction/survival pair required by the main theorem, on one fixed A.
```
theorem extinction (m : ℕ) [NeZero m] :
    IsZero (SelectedBaseIterates.object (FiniteSelectionFamily.test m) (2*m)) ∧
      ¬ IsZero (SelectedBaseIterates.object (FiniteSelectionFamily.test m) (2*m-2)) := by
…
```
Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object, OAI.LittleFinitistic.FiniteSelectionFamily.test