ProbePresentations.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PartitionConsistency.ProbeAlgebra.Path.map line 13
Source documentation
The same countable probe presentation over the larger base.
```
def map : Path M (f a) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Path
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.map_node line 19
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.map_factor line 21
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.map_terminal line 29
def OAI.PartitionConsistency.ProbeAlgebra.Path.lettersMap line 38
Source documentation
Map the actual, potentially non-injective direct limits.
```
noncomputable def lettersMap : P.Letters → (P.map f).Letters :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Path.Letters
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.lettersMap_letter line 42
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.lettersMap_injective line 48
Source documentation
Reflection is tested at a common finite stage, not by cancellation of the (possibly non-injective) transition maps.
```
theorem lettersMap_injective (hf : Function.Injective f) :
    Function.Injective (P.lettersMap f) := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.lettersMap_act line 58
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.lettersMap_exit line 65
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.lettersMap_inCone_iff line 74
Source documentation
Smaller-letter divisibility is reflected with its exact quotient: a larger-stage witness can be pulled back by old-factor conservation.
```
theorem lettersMap_inCone_iff (hf : Conservative f) (x : B) (s : P.Letters) :
    (P.map f).InCone (f x) (P.lettersMap f s) ↔ P.InCone x s := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Path.InCone
structure OAI.PartitionConsistency.ProbeAlgebra.AlphabetSimulation line 90
Source documentation
A map of probe alphabets whose old divisibility tests are unchanged. All these laws will be proved for the path direct limits; no assumptions about joins between new words or their gates enter this definition.
```
structure AlphabetSimulation {B : Type u} {M : Type v} {S : Type w} {T : Type z}
    [LeftCancelMonoid B] [LeftCancelMonoid M]
    (A : Alphabet B S) (C : Alphabet M T) (f : B →* M) (g : S → T) : Prop where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Alphabet
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.alphabetSimulation line 105
Source documentation
A conservative map of bases supplies an alphabet simulation for the same generators and terminal parameter.
```
theorem alphabetSimulation : AlphabetSimulation (P.alphabet he)
    ((P.map f).alphabet (fun h => he (hf.injective (h.trans f.map_one.symm)))) f
    (P.lettersMap f) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.AlphabetSimulation, OAI.PartitionConsistency.ProbeAlgebra.Path.alphabet
def OAI.PartitionConsistency.ProbeAlgebra.Raw.transport line 120
Source documentation
Simulation on literal strings. Reducedness will be proved, not postulated or hidden in a quotient of these words.
```
def transport (f : B → M) (g : S → T) : Raw B S → Raw M T
  | old x => old (f x)
  | cons s w => cons (g s) (transport f g w)
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Raw
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.transport_old line 124
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.transport_cons line 126
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.transport_injective line 129
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.headDiv_transport line 152
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.reduced_transport line 159
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.transport_oldAct line 169
def OAI.PartitionConsistency.ProbeAlgebra.Word.transport line 184
Source documentation
Smaller irreducible words remain irreducible in the larger presentation.
```
def transport (y : Word A b) : Word C (f b) :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_old line 187
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_cons line 190
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_transport line 195
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv_transport line 200
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_injective line 204
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_oldAct line 208
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_quotient line 212
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_letterAct line 219
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_mul line 231
def OAI.PartitionConsistency.ProbeAlgebra.Word.transportHom line 243
Source documentation
The literal normal-form embedding respects the defining reductions.
```
def transportHom : Word A b →* Word C (f b) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transportHom_apply line 248
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_dvd_transport_iff line 251

theorem OAI.PartitionConsistency.ProbeAlgebra.Word.simulated_old_intersection line 271

Source documentation

The old intersection used in the gate recursion is the same on both sides, including its original right quotients.

theorem simulated_old_intersection (x y : B) (q : Word C (f b))
    (hx : old C (f b) (f x) ∣ q) (hy : old C (f b) (f y) ∣ q) :
    ∃ j : B, (∀ v : Word A b, old A b x ∣ v ∧ old A b y ∣ v ↔ old A b j ∣ v) ∧
      ∀ v : Word C (f b), old C (f b) (f x) ∣ v ∧ old C (f b) (f y) ∣ v ↔
        old C (f b) (f j) ∣ v := by
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.ProbeAlgebra.Word.exists_simulated_gate_of_exit line 284
Source documentation
An exit in the larger presentation determines exactly the same old gate in both presentations. Induction computes gates using the transported old joins; the existence/nonexistence of a gate is not an assumption.
```
theorem exists_simulated_gate_of_exit (x : Word A b) {s : S}
    (hx : head A b x = some s) {q : Word C (f b)}
    (hxq : transport hf hg b x ∣ q) (hq : head C (f b) q ≠ some (g s)) :
    ∃ j : B, Gate A b x s j ∧ Gate C (f b) (transport hf hg b x) (g s) (f j) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.transport, OAI.PartitionConsistency.ProbeAlgebra.Word.Gate
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_transport_eq_some line 361
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_factor_of_dvd line 371
Source documentation
Once a comparison reflects, cancellation reflects its particular factor, not just the existence of some factor.
```
theorem transport_factor_of_dvd (x y : Word A b) (q : Word C (f b))
    (h : transport hf hg b x * q = transport hf hg b y) (hxy : x ∣ y) :
    ∃ r : Word A b, transport hf hg b r = q := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.transport
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_factors line 389
Source documentation
Source lem:mono-simulation, separate division argument for probes. Old heads use letter-cone reflection; equal new heads cancel; an exit factors through the shared old gate furnished by the gate recursion.
```
theorem transport_factors (x y : Word A b) (q : Word C (f b))
    (h : transport hf hg b x * q = transport hf hg b y) :
    ∃ r : Word A b, transport hf hg b r = q := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.transport
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_dvd_iff line 423
Source documentation
Comparisons between transported probe normal forms reflect.
```
theorem transport_dvd_iff (x y : Word A b) :
    transport hf hg b x ∣ transport hf hg b y ↔ x ∣ y := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.transport
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_generator line 441
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_old_common_below line 456
Source documentation
An old/new common upper bound in the larger extension lies above a smaller common upper bound. The latter is the new word itself, or is old and obtained by joining its shared gate with the old divisor.
```
theorem transport_old_common_below (x : B) (y : Word A b) (q : Word C (f b))
    (hx : old C (f b) (f x) ∣ q) (hy : transport hf hg b y ∣ q) :
    ∃ j : Word A b, old A b x ∣ j ∧ y ∣ j ∧ transport hf hg b j ∣ q := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.transport
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_dvd_of_different_head line 485
Source documentation
A larger common multiple in one smaller first-letter block puts the other, differently headed smaller divisor below the entire smaller block.
```
theorem transport_dvd_of_different_head {x y : Word A b} {s t : S}
    (hx : head A b x = some s) (hy : head A b y = some t) (hst : s ≠ t)
    {q : Word C (f b)} (hyq : transport hf hg b y ∣ q)
    (hq : head C (f b) q = some (g s)) : y ∣ x := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.transport
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_common_below line 503
Source documentation
Every larger common upper bound of two simulated words lies above a smaller common upper bound. This simultaneously conserves joins and the absence of joins, rather than just comparisons between simulated words.
```
theorem transport_common_below (x y : Word A b) (q : Word C (f b))
    (hxq : transport hf hg b x ∣ q) (hyq : transport hf hg b y ∣ q) :
    ∃ j : Word A b, x ∣ j ∧ y ∣ j ∧ transport hf hg b j ∣ q := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.transport
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.transport_conservative line 572
Source documentation
Probe normal-form simulation conserves factors, all old cone intersections, and old nonjoins.
```
theorem transport_conservative : Conservative (transportHom hf hg b) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.transportHom
def OAI.PartitionConsistency.ProbeAlgebra.Path.simulation line 600
Source documentation
Simulate the identical countable probe presentation over the larger base; this is a homomorphism of the actual reduced-word extensions.
```
noncomputable def simulation : P.Extension he b →*
    (P.map f).Extension (fun h => he (hf.injective (h.trans f.map_one.symm))) (f b) :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Path.Extension
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.simulation_conservative line 606
Source documentation
Probe case of source lem:mono-simulation. It conserves right factors, whole cone intersections, and the lack of a common right multiple.
```
theorem simulation_conservative
    (hB : HasConditionalJoins (LeftDivOrder B)) (hb : b ≠ 1) :
    Conservative (P.simulation he hf b) :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.simulation_old line 614
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.simulation_probe line 619