OAI/Geometry/HyperbolicGroups/StarModel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.StarModel.Var line 17

    Source documentation

    Actual amalgamated fields: one copy in U, one copy per branch outside U.

    abbrev Var (U : Finset F) := U ⊕ (B × {f : F // f ∉ U})
  2. abbrev OAI.HyperbolicObstruction.StarModel.Pos line 21

    Source documentation

    Actual amalgamated row positions; all positions still refer to the original arrays, not to newly independent copies of an array.

    abbrev Pos (support : R → Finset F) (U : Finset F) :=
…
  3. def OAI.HyperbolicObstruction.StarModel.coord line 24
  4. def OAI.HyperbolicObstruction.StarModel.field line 27
  5. lemma OAI.HyperbolicObstruction.StarModel.field_coord line 31
  6. lemma OAI.HyperbolicObstruction.StarModel.coord_injective line 35
  7. lemma OAI.HyperbolicObstruction.StarModel.coord_in line 39
  8. lemma OAI.HyperbolicObstruction.StarModel.coord_out line 42
  9. def OAI.HyperbolicObstruction.StarModel.array line 45
  10. def OAI.HyperbolicObstruction.StarModel.branch line 49
  11. def OAI.HyperbolicObstruction.StarModel.row line 53
  12. def OAI.HyperbolicObstruction.StarModel.rowSupport line 57
  13. lemma OAI.HyperbolicObstruction.StarModel.read_row line 61
  14. def OAI.HyperbolicObstruction.StarModel.InjectiveFields line 73

    Source documentation

    The only injectivity imposed is within one field across branches.

    def InjectiveFields (U : Finset F) (σ : Var (B := B) U → A) : Prop :=
…

    Mentions: OAI.HyperbolicObstruction.StarModel.Var

  15. instance OAI.HyperbolicObstruction.StarModel.(instance at line 76) line 76
  16. lemma OAI.HyperbolicObstruction.StarModel.row_injective line 81
  17. lemma OAI.HyperbolicObstruction.StarModel.present_iff line 110

    Source documentation

    Every actual branch is a master match exactly when every amalgamated row trial is present. This identity permits the later coupling on actual matches.

    lemma present_iff [Nonempty B] (support : R → Finset F) (U : Finset F)
    (σ : Var (B := B) U → A) (w : TableModel.Entry (A := A) support → Bool) :
…

    Mentions: OAI.HyperbolicObstruction.StarModel.Var, OAI.HyperbolicObstruction.TableModel.Entry