ConservativeExtensions.lean`

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PartitionConsistency.DiagramOrder.Conservative line 13
Source documentation
Conservation of a submonoid means more than an injective homomorphism: right factors of old comparisons, entire old intersections, and absence of old common right multiples are preserved.
```
structure Conservative {M : Type u} {N : Type v} [Monoid M] [Monoid N]
    (f : M →* N) : Prop where
…
```
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.factor_eq line 30
Source documentation
Division is reflected together with its particular unique factor, not by an unrelated witness to the existence of a comparison.
```
theorem factor_eq {x y : M} {z : N} (h : f x * z = f y) :
    ∃ t : M, f t = z ∧ x * t = y := by
…
```
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.dvd_iff line 35
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.common_iff line 42
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.intersection_iff line 49
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.comp line 59
Source documentation
The composition law is what makes comparisons testable in the final monoid, independently of the birth step at which a factor was computed.
```
theorem comp {g : N →* R} (hg : Conservative g) : Conservative (g.comp f) where
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.Conservative
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.id line 70
Source documentation
Identity inclusions are conservative.
```
theorem id (M : Type u) [Monoid M] : Conservative (MonoidHom.id M) where
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.Conservative
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.oldHom_conservative line 86
Source documentation
All four conservation requirements for the actual probe extension.
```
theorem oldHom_conservative : Conservative (Word.oldHom (P.alphabet he) b) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.oldHom
theorem OAI.PartitionConsistency.MergerAlgebra.Word.oldHom_conservative line 104
Source documentation
All four conservation requirements for merger normal forms.
```
theorem oldHom_conservative : Conservative (oldHom : M →* Word M D) where
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word.oldHom, OAI.PartitionConsistency.MergerAlgebra.Word
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.map line 121
Source documentation
Transport the actual overlap starts along a base homomorphism. The pair relation remains the given one-step relation, not its transitive closure.
```
def map (P : OverlapPrescription B n) (f : B →* M) : OverlapPrescription M n where
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.map_start line 124
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.rel_map line 128
Source documentation
Each prescribed identification is valid after transporting its factors.
```
theorem rel_map (P : OverlapPrescription B n) (f : B →* M)
    {i j : Fin n} {x y : B} (h : P.Rel (i,x) (j,y)) :
    (P.map f).Rel (i, f x) (j, f y) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription, OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Rel
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.rel_map_iff line 148
Source documentation
Factor conservation reflects each one-step identification, without assuming that the prescription is valid in either monoid.
```
theorem rel_map_iff (P : OverlapPrescription B n) {f : B →* M} (hf : Conservative f)
    (i j : Fin n) (x y : B) :
    (P.map f).Rel (i, f x) (j, f y) ↔ P.Rel (i,x) (j,y) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription, OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Rel
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.valid_of_map line 169
Source documentation
Validity of a transported prescription reflects to the old monoid.
```
theorem valid_of_map (P : OverlapPrescription B n) {f : B →* M} (hf : Conservative f)
    (h : (P.map f).Valid) : P.Valid where
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription, OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Valid
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.rel_start line 183
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.exists_starts_of_rel_map line 188
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.valid_map line 210
Source documentation
Cone intersections, with their original right quotients, suffice to transport a valid finite prescription. The transitivity check is at the old join of the two middle-copy starts; it is not a transitive closure of the transported prescription. Source lem:mono-simulation, final assertion.
```
theorem valid_map (P : OverlapPrescription B n) (hP : P.Valid)
    (hB : HasConditionalJoins (LeftDivOrder B)) {f : B →* M} (hf : Conservative f) :
    (P.map f).Valid where
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription, OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Valid
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.valid_map_iff line 253
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.common_below line 269
Source documentation
An upper bound in the larger monoid admits an old joint lower bound of any two specified old divisors.
```
theorem common_below (hB : HasConditionalJoins (LeftDivOrder B))
    {x y : B} {m : M} (hx : f x ∣ m) (hy : f y ∣ m) :
    ∃ j : B, x ∣ j ∧ y ∣ j ∧ f j ∣ m := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
theorem OAI.PartitionConsistency.DiagramOrder.Conservative.cone_residual line 279
Source documentation
Residual cones of old elements are computed using the same old join and right quotient even when queried at a new factor.
```
theorem cone_residual (hB : HasConditionalJoins (LeftDivOrder B))
    (x a : B) {t : M} (ht : f x ∣ f a * t) :
    ∃ r : B, (∀ z : B, x ∣ a * z ↔ r ∣ z) ∧
      ∀ z : M, f x ∣ f a * z ↔ f r ∣ z := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesMap line 304
Source documentation
The genuine copy quotient embeds under conservative base simulation.
```
def copiesMap : P.Copies hP → (P.map f).Copies (P.valid_map hP hB hf) :=
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Copies
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesMap_copy line 308
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesMap_injective line 312
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesMap_act line 318
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesMap_factors line 328
Source documentation
A right factor between smaller-copy elements stays in the old base; validity alone would not give this assertion.
```
theorem copiesMap_factors (z w : P.Copies hP) (m : M)
    (h : act (P.copiesMap hP hB hf z) m = P.copiesMap hP hB hf w) :
    ∃ a : B, f a = m := by
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesMap_common_below line 347
Source documentation
The finite-overlap cone calculation lifts an old common lower bound below each larger common upper bound. This proves preservation both of all old joins and of nonjoins, not just injectivity of the quotient map.
```
theorem copiesMap_common_below (z w : P.Copies hP)
    (c : (P.map f).Copies (P.valid_map hP hB hf))
    (hz : Reaches M (P.copiesMap hP hB hf z) c)
    (hw : Reaches M (P.copiesMap hP hB hf w) c) :
    ∃ j : P.Copies hP, Reaches B z j ∧ Reaches B w j ∧
      Reaches M (P.copiesMap hP hB hf j) c := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Copies
def OAI.PartitionConsistency.MergerAlgebra.Word.transport line 394
Source documentation
Simulation on literal merger normal forms, by transporting each coefficient and each final-letter quotient class.
```
def transport (f : B →* M) (g : D → E) : Word B D → Word M E
  | old x => old (f x)
  | snoc t d => snoc (transport f g t) (g d)
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_old line 398
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_snoc line 400
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_act line 408
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_mul line 415
def OAI.PartitionConsistency.MergerAlgebra.Word.transportHom line 421
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transportHom_apply line 426
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_injective line 430
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_factors line 450
Source documentation
Right division of two simulated normal forms produces a smaller normal form. This is stronger than existence of some reflected divisor.
```
theorem transport_factors (hf : Conservative f)
    (hgf : ∀ d e : D, ∀ a : M, RightFreeAction.act (g d) a = g e → ∃ b : B, f b = a)
    (x y : Word B D) (q : Word M E)
    (h : transport f g x * q = transport f g y) :
    ∃ r : Word B D, transport f g r = q := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.Word.transport
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_dvd_iff line 479
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_common_below line 511
Source documentation
Joint lower bounds of old divisors are lifted by induction on the literal larger upper bound. At unequal lengths the comparison reflects by right-factor conservation; at equal lengths the final-letter cone calculation controls the intersection.
```
theorem transport_common_below (x y : Word B D) (c : Word M E)
    (hx : transport f g x ∣ c) (hy : transport f g y ∣ c) :
    ∃ j : Word B D, x ∣ j ∧ y ∣ j ∧ transport f g j ∣ c := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.Word.transport
theorem OAI.PartitionConsistency.MergerAlgebra.Word.transport_conservative line 558
Source documentation
The entire merger normal-form simulation is conservative.
```
theorem transport_conservative : Conservative (transportHom f g hgact) where
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word.transportHom
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerSimulation line 587
Source documentation
Simulate exactly the smaller merger presentation in the larger base, using the same prescribed overlap starts.
```
def mergerSimulation : Word B (P.Copies hP) →*
    Word M ((P.map f).Copies (P.valid_map hP hB hf)) :=
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Copies
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerSimulation_conservative line 593
Source documentation
Merger case of source lem:mono-simulation: the induced homomorphism is conservative, including old factors, all cone intersections, and nonjoins.
```
theorem mergerSimulation_conservative : Conservative (P.mergerSimulation hP hB hf) :=
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerSimulation_old line 598
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerSimulation_snoc line 601