GateTowers.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite descent through a continuous tower of old gates

def OAI.PartitionConsistency.DiagramOrder.NoNewOldDivisors line 15
Source documentation
The no-new-divisors alternative at a successor stage. All divisibility statements are in the ambient final monoid.
```
def NoNewOldDivisors (B C : Submonoid T) : Prop :=
…
```
def OAI.PartitionConsistency.DiagramOrder.OldGateStep line 22
Source documentation
The least-old-multiple alternative at a successor stage, including the old-input implication used for descent. The new word must belong to the successor stage; arbitrary elements of the final monoid are not called new at this stage.
```
def OldGateStep (B C : Submonoid T) : Prop :=
…
```
structure OAI.PartitionConsistency.DiagramOrder.GateTower line 31
Source documentation
A continuous concrete tower with the two successor alternatives of thm:monoid. Terminal segments may be constant. The successor alternatives are recorded in the final divisibility relation, as allowed by conservative embeddings in the source. This definition is not an existence assertion.
```
structure GateTower (T : Type u) [Monoid T] where
…
```
def OAI.PartitionConsistency.DiagramOrder.Replaces line 41
Source documentation
A single admissible replacement, with both endpoints in the stipulated set of alignments. Its right factor is the same as that of the path indices.
```
def Replaces (n : ℕ → T) (A : Set (ℕ × T)) (p q : ℕ × T) : Prop :=
…
```

theorem OAI.PartitionConsistency.DiagramOrder.GateTower.finite_descent line 51

Source documentation

The finite descent in lem:mono-descent. The proof is by induction on stages. Hence its result is an actual finite chain of admissible replacements, not an appeal to the absence of an infinite decreasing sequence alone. Countability of the initial stage is not needed for this descent.

theorem finite_descent
    (hn : ∀ i, n i ∈ S.stage 0)
    (hq : ∀ i j d, n i * d = n j → d ∈ S.stage 0)
    (hbound : ∀ p ∈ A, ∃ N, p.2 ∣ n N)
    (hreplace : ∀ p ∈ A, ∀ N, ∃ l' d,
      (l', p.2 * d) ∈ A ∧ p.1 ≤ l' ∧ n p.1 * d = n l' ∧ n N ∣ p.2 * d)
    (α : Ordinal.{v}) (p : ℕ × T) (hp : p ∈ A) (hα : p.2 ∈ S.stage α) :
    ∃ q ∈ A, q.2 ∈ S.stage 0 ∧ Relation.ReflTransGen (Replaces n A) p q := by
…

Mentions: OAI.PartitionConsistency.DiagramOrder.Replaces

theorem OAI.PartitionConsistency.DiagramOrder.GateTower.finite_descent_terminal line 84

Source documentation

The terminal-stage formulation: every initial alignment can be brought to the designated base by finitely many replacements.

theorem finite_descent_terminal
    (hn : ∀ i, n i ∈ S.stage 0)
    (hq : ∀ i j d, n i * d = n j → d ∈ S.stage 0)
    (hbound : ∀ p ∈ A, ∃ N, p.2 ∣ n N)
    (hreplace : ∀ p ∈ A, ∀ N, ∃ l' d,
      (l', p.2 * d) ∈ A ∧ p.1 ≤ l' ∧ n p.1 * d = n l' ∧ n N ∣ p.2 * d)
    (ω : Ordinal.{v}) (hterminal : S.stage ω = ⊤)
    (p : ℕ × T) (hp : p ∈ A) :
    ∃ q ∈ A, q.2 ∈ S.stage 0 ∧ Relation.ReflTransGen (Replaces n A) p q := by
…

Mentions: OAI.PartitionConsistency.DiagramOrder.Replaces