PersistentProfiles.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Persistence of the full probe profile at successor stages

structure OAI.PartitionConsistency.DiagramOrder.ProbeProfile line 14
Source documentation
The full profile of a probe, with downsets taken in the entire monoid rather than only in the base over which the probe was adjoined.
```
structure ProbeProfile {M : Type u} [Monoid M]
    (a b e m : M) (n : ℕ → M) : Prop where
…
```
structure OAI.PartitionConsistency.DiagramOrder.OldGate line 25
Source documentation
An old gate controls both old right multiples and intersections with old cones not containing the new element. In probe normal forms this is exactly the first-letter exit rule.
```
structure OldGate {M : Type u} {N : Type v} [Monoid M] [Monoid N]
    (f : M →* N) (w : N) (g : M) : Prop where
…
```
def OAI.PartitionConsistency.DiagramOrder.HasOldGates line 34
Source documentation
Only elements with an old right multiple need a gate. For mergers all such elements are already old, so the second alternative is unused.
```
def HasOldGates {M : Type u} {N : Type v} [Monoid M] [Monoid N]
    (f : M →* N) : Prop :=
…
```
theorem OAI.PartitionConsistency.DiagramOrder.ProbeProfile.map line 49
Source documentation
Source lem:mono-profile-persistence, successor step. The new full downward closure of the original path, not its old set of divisors, is the profile in the extension.
```
theorem map : ProbeProfile (f a) (f b) (f e) (f m) (f ∘ n) where
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.ProbeProfile
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.hasOldGates line 86
Source documentation
The gate hypothesis of profile persistence is supplied by the actual probe extension, including all new words, not just the adjoined generators.
```
theorem hasOldGates (hM : HasConditionalJoins (LeftDivOrder M)) :
    HasOldGates (Word.oldHom (P.alphabet he) b) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.oldHom

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probeProfile line 108

Source documentation

The profile initially holds with all downsets in the new monoid.

theorem probeProfile (hM : HasConditionalJoins (LeftDivOrder M)) (hb : b ≠ 1) :
    ProbeProfile (Word.old (P.alphabet he) b a) (Word.old (P.alphabet he) b b)
      (Word.old (P.alphabet he) b e) (P.probe he b hb 0)
      (fun i => Word.old (P.alphabet he) b (P.node i)) where
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.preserve_profile line 119

Source documentation

The same profile survives a later probe operation, whose parameters need have no relation to the parameters of the original probe.

theorem preserve_profile (hM : HasConditionalJoins (LeftDivOrder M))
    {a₀ b₀ e₀ m₀ : M} {n₀ : ℕ → M} (h : ProbeProfile a₀ b₀ e₀ m₀ n₀) :
    ProbeProfile (Word.old (P.alphabet he) b a₀) (Word.old (P.alphabet he) b b₀)
      (Word.old (P.alphabet he) b e₀) (Word.old (P.alphabet he) b m₀)
      (fun i => Word.old (P.alphabet he) b (n₀ i)) :=
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.MergerAlgebra.Word.hasOldGates line 134
Source documentation
A merger introduces no new divisor of any old element.
```
theorem hasOldGates : HasOldGates (oldHom : M →* Word M D) := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word.oldHom, OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.preserve_profile line 140
Source documentation
Source profile persistence for a merger successor.
```
theorem preserve_profile {a b e m : M} {n : ℕ → M} (h : ProbeProfile a b e m n) :
    ProbeProfile (old a : Word M D) (old b) (old e) (old m) (fun i => old (n i)) :=
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word