PrimeWordCellGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.primeLogIndex_eq_iff line 11
theorem OAI.Ostmann.primeLogIndex_filter_shell line 30
Source documentation
Intersecting a whole shell with an integer cell clips its endpoints; no boundary prime is removed or added. Prescribed exclusions remain intact.
```
theorem primeLogIndex_filter_shell (a b : ℝ) (D : Finset ℕ) (h : ℕ) :
    ((primeLogCellSet 1 0 a b \ D).filter (fun p => primeLogIndex p = h)) =
      primeLogCellSet 1 0 (max a (h : ℝ)) (min b ((h : ℝ) + 1)) \ D := by
…
```
Mentions: OAI.Ostmann.primeLogCellSet, OAI.Ostmann.primeLogIndex
theorem OAI.Ostmann.primeCellWordPrior_lift line 45
Source documentation
Passing a selected cell to the common prime sample space preserves its original harmonic normalizer exactly.
```
theorem primeCellWordPrior_lift (P Q : Finset ℕ) (hQP : Q ⊆ P) (h : ℕ) (p : Q) :
    primeSubsetPrior P (Q.filter (fun q => primeLogIndex q = h)) ⟨p, hQP p.property⟩ =
      primeCellWordPrior Q h p := by
…
```
Mentions: OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.primeLogIndex, OAI.Ostmann.primeCellWordPrior