QuotientActions.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

SaturatedFibers

theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.square_ideal_probes line 17
Source documentation
Reindex the actual saturated probes into independently hit rows. This uses infinitude of the prescribed multiplicity, not a new saturation step.
```
theorem square_ideal_probes (a b : target M K) (hb : b ≠ 1)
    (U : ConeIdeal (α := LeftDivOrder (target M K)) a) :
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target
instance OAI.PartitionConsistency.LocalDiagramSystem.System.fiberSmall line 42
instance OAI.PartitionConsistency.ProductForcing.eligibleSystem_obj_small line 56
theorem OAI.PartitionConsistency.ProductForcing.classFiber_cardinal_le line 68
Source documentation
The entire eligible quotient bounds every exact fiber. The input is only meeting the explicit, proved dense record sets, not an assumed list of representatives or an assumed fiber cardinal.
```
theorem classFiber_cardinal_le [Infinite M] [Infinite I]
    (hpower : μ ^ Cardinal.aleph0 = μ) (hcard : Cardinal.mk M ≤ μ)
    (hκ : Cardinal.mk κ ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (F : GenericFilter (CohenForcing.Condition I κ))
    {q : Diagram M I} (w : Vertex q)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system

theorem OAI.PartitionConsistency.ConcreteSystem.classFiber_dense_lower line 107

Source documentation

For the concrete executed saturation, an outside witness supplies dense requirements for the exact lower class-fiber bound. All final ideals at all vertices are covered; no algebraic profile or exact-intersection premise is left for the extension argument to supply.

theorem classFiber_dense_lower {q : Diagram T I} (w : Vertex q) (b : T) (hb : b ≠ 1)
    (E : S.Name) (hE : ∀ π ∈ SupportFilter.Fix (q.sub T.e).range, π • E = E)
    (t : Diagram T I) (ht : t.sub b = q.sub T.e)
    (d : CohenForcing.Condition I κ) (hd : d.support ⊆ t.range)
    (j : I) (hj : j ∈ t.range)
    (hout : ∀ z : P, z ≤ (d,t) →
      ¬ S.atomic.MemF z (labelClass aleph0_le_μ (posetCode κ) E j)
        (localList aleph0_le_μ (posetCode κ) cardinal_T.le (q.sub T.e))) :
    ∃ D : K → Set (CohenForcing.Condition I κ), (∀ i, Dense (D i)) ∧
      ∀ F : GenericFilter (CohenForcing.Condition I κ), d ∈ F →
        (∀ i, ∃ a, a ∈ F ∧ a ∈ D i) →
        Nonempty (K ↪ (eligibleSystem aleph0_le_μ (posetCode κ) cardinal_T.le size_lt finiteMergers F q E
…

Mentions: OAI.PartitionConsistency.ConcreteSystem.T, OAI.PartitionConsistency.ConcreteSystem.I, OAI.PartitionConsistency.SupportFilter.Fix, OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ConcreteSystem.κ, OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.ConcreteSystem.K, OAI.PartitionConsistency.ConcreteSystem.size_lt, OAI.PartitionConsistency.ConcreteSystem.finiteMergers

theorem OAI.PartitionConsistency.ConcreteSystem.concreteEligibleFiberSmall line 125

theorem OAI.PartitionConsistency.ConcreteSystem.classFiber_dense_exact line 139

Source documentation

The exact-fiber theorem for the concrete system, with explicitly identified ordinary Cohen requirements. No genericity or existence of an intermediate ordinary extension is claimed by this statement.

theorem classFiber_dense_exact {q : Diagram T I} (w : Vertex q) (b : T) (hb : b ≠ 1)
    (E : S.Name) (hE : ∀ π ∈ SupportFilter.Fix (q.sub T.e).range, π • E = E)
    (t : Diagram T I) (ht : t.sub b = q.sub T.e)
    (d : CohenForcing.Condition I κ) (hd : d.support ⊆ t.range)
    (j : I) (hj : j ∈ t.range)
    (hout : ∀ z : P, z ≤ (d,t) →
      ¬ S.atomic.MemF z (labelClass aleph0_le_μ (posetCode κ) E j)
        (localList aleph0_le_μ (posetCode κ) cardinal_T.le (q.sub T.e))) :
    ∃ D : K → Set (CohenForcing.Condition I κ), (∀ i, Dense (D i)) ∧
      ∀ F : GenericFilter (CohenForcing.Condition I κ), d ∈ F →
        (∀ i, ∃ a, a ∈ F ∧ a ∈ D i) →
        (∀ (τ : LocalName aleph0_le_μ (posetCode κ) w.diagram) (d₀ : CohenForcing.Condition I κ), d₀ ∈ F →
…

instance OAI.PartitionConsistency.ProductForcing.eligibleSystem_glued_small line 197
def OAI.PartitionConsistency.ProductForcing.ChainCode.codeOrderBound line 205
Source documentation
The order bound is the order type of the one fixed ground-code wellordering, computed on a small copy of the code set.
```
def codeOrderBound : Ordinal.{u} :=
…
```
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.orderType_le line 210
Source documentation
The least-code ordering is induced on a subset of the code set, so its order type cannot exceed the chosen ground bound.
```
theorem orderType_le (F : GenericFilter (CohenForcing.Condition I κ)) :
    Ordinal.type (OrderAssignment.smallRel.{u} (LT hμ c hcard hsize hmerger hj E hE C F)) ≤
      codeOrderBound hμ c C := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.LT, OAI.PartitionConsistency.ProductForcing.ChainCode.codeOrderBound
def OAI.PartitionConsistency.ProductForcing.ChainCode.componentTable line 222
Source documentation
This is a bounded table chosen just once for the component and its chain; in particular it has no filter argument.
```
def componentTable : OrderAssignment.Table (labelFiberSet v) (codeOrderBound hμ c C) :=
…
```
Mentions: OAI.PartitionConsistency.OrderAssignment.Table, OAI.PartitionConsistency.ProductForcing.ChainCode.codeOrderBound
def OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary line 228
Source documentation
The preliminary bijection uses the actual least-code order and the one fixed table. The displayed cardinal equality is precisely the point at which the exact-fiber theorem is used.
```
def preliminary (F : GenericFilter (CohenForcing.Condition I κ))
    (hc : Cardinal.mk (Shrink.{u} ((D[F]).Glued hj v)) = Cardinal.mk (labelFiberSet v)) :
    labelFiberSet v ≃ (D[F]).Glued hj v :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition

theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_covariance line 238

Source documentation

Literal covariance of the preliminary assignment between F and kF. The label is unchanged, as every member of the tail fixer fixes all the labels in this fiber. The two cardinal-equality proofs are immaterial.

theorem preliminary_covariance (F : GenericFilter (CohenForcing.Condition I κ))
    (k : C.tailFixer hj)
    (hc : Cardinal.mk (Shrink.{u} ((D[F]).Glued hj v)) = Cardinal.mk (labelFiberSet v))
    (hc' : Cardinal.mk (Shrink.{u}
      ((D[F.move (CohenForcing.Condition.permuteOrderIso k.val.val.val)]).Glued hj v)) =
        Cardinal.mk (labelFiberSet v)) (j : labelFiberSet v) :
    preliminary hμ c hcard hsize hmerger hj E hE C
        (F.move (CohenForcing.Condition.permuteOrderIso k.val.val.val)) hc' j =
      transport hμ c hcard hsize hmerger hj E hE F k.val
        (preliminary hμ c hcard hsize hmerger hj E hE C F hc j) :=
…

Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.permuteOrderIso, OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary, OAI.PartitionConsistency.ProductForcing.ChainCode.transport

instance OAI.PartitionConsistency.ForcingQuotient.(instance at line 266) line 266
theorem OAI.PartitionConsistency.ForcingQuotient.smul_filter line 279
def OAI.PartitionConsistency.LocalDiagramSystem.labelTransport line 291
Source documentation
Coordinate transport for literal label fibers.
```
def labelTransport (π : Equiv.Perm I) : ReindexIso (labelSystem (M := M)) labelSystem π where
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.ReindexIso, OAI.PartitionConsistency.LocalDiagramSystem.labelSystem
theorem OAI.PartitionConsistency.LocalDiagramSystem.labelTransport_fiber_val line 300
theorem OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet_permute line 304
instance OAI.PartitionConsistency.LocalDiagramSystem.Vertex.labelFiberAction line 317
Source documentation
The stabilizer permutes the actual common subset of label indices.
```
instance labelFiberAction : MulAction (componentStabilizer hj v) (labelFiberSet v) where
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer, OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.smul_labelFiber_val line 324
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.tailFixer_fixes_label line 327
def OAI.PartitionConsistency.ProductForcing.ChainCode.Total line 353
Source documentation
The total symbolic component over all ordinary Cohen filters. There is no assertion here that any particular such filter is a ground generic.
```
def Total := Σ F : GenericFilter (CohenForcing.Condition I κ), (D[F]).Glued hj v
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
def OAI.PartitionConsistency.ProductForcing.ChainCode.TotalAt line 356
Source documentation
Representation in the total space, retaining its actual filter.
```
def TotalAt (w : Vertex q) (τ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.total_eq_of_representation line 362
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.total_has_representation line 373
def OAI.PartitionConsistency.ProductForcing.ChainCode.totalMove line 383
Source documentation
A lift of transport to the total space, before verifying the action laws.
```
def totalMove (g : Vertex.componentStabilizer hj v)
    (x : Total hμ c hcard hsize hmerger hj E hE v) :
    Total hμ c hcard hsize hmerger hj E hE v :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode.Total
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.totalAt_move line 388
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.totalMove_one line 396
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.totalMove_mul line 403
instance OAI.PartitionConsistency.ProductForcing.ChainCode.totalAction line 417
Source documentation
A genuine action only on the family of all moved computations.
```
instance totalAction : MulAction (Vertex.componentStabilizer hj v)
    (Total hμ c hcard hsize hmerger hj E hE v) where
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode.Total
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.totalAction_fst line 423
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.chainFix_le_tailGroup line 452
Source documentation
Every one of the shrinking chain diagrams supports the ordinal names, not just the first diagram.
```
theorem chainFix_le_tailGroup (i : ℕ) :
    SupportFilter.Fix (C.vertex i).diagram.range ≤ tailGroup hj C := by
…
```
Mentions: OAI.PartitionConsistency.SupportFilter.Fix, OAI.PartitionConsistency.ProductForcing.ChainCode.tailGroup
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_permute line 469
Source documentation
The same code is linked to the transported name at the moved vertex. It is not necessary for the permutation to fix the original root.
```
theorem links_permute (k : C.tailFixer hj) (d : CohenForcing.Condition I κ)
    (w : Vertex q) (τ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.tail_eq_permute line 487
Source documentation
Local decision reflects a tail-invariant equality back from the moved root. This is the needed covariance of ordinal VALUES, not just names.
```
theorem tail_eq_permute (k : C.tailFixer hj) (d : CohenForcing.Condition I κ)
    (τ σ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalRank_fixed line 514
Source documentation
Both ordinal name constructions are literally fixed by the tail group.
```
theorem ordinalRank_fixed (a : Index hμ c C) (π : Equiv.Perm I) (hπ : π ∈ tailGroup hj C) :
    π • ordinalRank hμ c hcard hsize hmerger hj E hE C a =
      ordinalRank hμ c hcard hsize hmerger hj E hE C a :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode.Index, OAI.PartitionConsistency.ProductForcing.ChainCode.tailGroup, OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalRank
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalType_fixed line 519