CellTowers.lean`

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

CellRestriction

theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.ext line 18
theorem OAI.PartitionConsistency.ConservativeMonoids.Probe.exists_preimage line 29
Source documentation
No closure-of-path assertion is presumed: divisibility is reflected by conservation, and the actual countably many nodes are pulled back.
```
theorem exists_preimage (d : Probe N) (f : M ⟶ N)
    (h : d.parameters ⊆ Set.range f) : ∃ c : Probe M, c.map f = d := by
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Probe
theorem OAI.PartitionConsistency.ConservativeMonoids.Merger.exists_preimage line 56
Source documentation
The finite presentation uses only the displayed starts. Every validity clause is reflected along the conservative inclusion, not added as a new hypothesis on the selected prescription.
```
theorem exists_preimage (d : Merger N) (f : M ⟶ N)
    (h : d.parameters ⊆ Set.range f) : ∃ c : Merger M, c.map f = d := by
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Merger
theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.exists_preimage line 96
theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.exists_restriction line 108
Source documentation
In particular, every parameter-containing conservative subobject admits the same actual operation.
```
theorem exists_restriction (d : Cell M) (S : Subobject M)
    (h : d.parameters ⊆ S.submonoid) :
    ∃ c : Cell S.object, c.map S.inclusion = d :=
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Cell, OAI.PartitionConsistency.ConservativeMonoids.Subobject
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.of_mulEquiv line 129
Source documentation
A monoid isomorphism preserves all four conservation conditions.
```
theorem of_mulEquiv (e : M ≃* N) : Conservative e.toMonoidHom where
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.Conservative
def OAI.PartitionConsistency.ConservativeMonoids.ofMulEquiv line 148
theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.ext line 154
def OAI.PartitionConsistency.ConservativeMonoids.Subobject.top line 157
def OAI.PartitionConsistency.ConservativeMonoids.Subobject.hom line 162
theorem OAI.PartitionConsistency.ConservativeMonoids.Subobject.hom_apply line 167
structure OAI.PartitionConsistency.ConservativeMonoids.Attachment line 173
Source documentation
An actual presentation cell, identified with a subobject of the very same terminal monoid. The identification fixes every old element.
```
structure Attachment {T : Object.{u}} (S R : Subobject T) where
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject
def OAI.PartitionConsistency.ConservativeMonoids.Attachment.embedding line 181
def OAI.PartitionConsistency.ConservativeMonoids.Attachment.generator line 183
def OAI.PartitionConsistency.ConservativeMonoids.Attachment.parameters line 185
theorem OAI.PartitionConsistency.ConservativeMonoids.Attachment.embedding_old line 187
theorem OAI.PartitionConsistency.ConservativeMonoids.Attachment.parameters_countable line 190
theorem OAI.PartitionConsistency.ConservativeMonoids.Attachment.old_le line 194
theorem OAI.PartitionConsistency.ConservativeMonoids.Attachment.finite_coefficients line 203
Source documentation
A retained word has a finite list of old coefficients, even in a countably presented cell.
```
theorem finite_coefficients (x : R.object) :
    ∃ s : Finset S.object, x.val ∈ Submonoid.closure
      (S.inclusion '' (s : Set S.object) ∪ Set.range d.generator) := by
…
```
structure OAI.PartitionConsistency.ConservativeMonoids.CellTower line 229
Source documentation
The original construction as a continuous tower of literal cells. Identity steps are allowed, so a selected or an omitted subconstruction can keep the same index order without compressing its limit cuts.
```
structure CellTower where
…
```
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.NewAt line 242
Source documentation
The unique original successor where an element first appears.
```
def NewAt (i : J) (x : T) : Prop :=
…
```
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.NewAt.not_isMax line 246
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.NewAt.neq line 251
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.NewAt.unique line 257
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.exists_newAt line 266
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.newIndex line 287
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.newIndex_eq line 289
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.stepCell line 295
Source documentation
The chosen cell at an active stage is independent of the queried word.
```
def stepCell (i : J) (h : (D.stage i).submonoid ≠ (D.stage (Order.succ i)).submonoid) :
    Attachment (D.stage i) (D.stage (Order.succ i)) := ((D.step i).resolve_left h).some
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Attachment
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.coefficients line 298
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.dependencies line 302
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.dependencies_countable line 310
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.dependencies_at line 318
def OAI.PartitionConsistency.ConservativeMonoids.CellTower.hull line 329
Source documentation
Close under dependencies as well as factors and actual conditional joins. This is a submonoid of the terminal monoid, not a substitute monoid.
```
def hull (s : Set T) : Subobject T where
…
```
Mentions: OAI.PartitionConsistency.ConservativeMonoids.Subobject
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.hull_countable line 336
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.subset_hull line 341
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.bottom_le_hull line 344
theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.hull_closed line 347