OAI/GroupTheory/BooneHigman/TreeRefinement.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_left_injective line 19
2. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit_comp_comm line 25
3. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit_comp_disjoint line 34
4. inductive OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Coherent line 46

   Source documentation

   Syntactic coherence generated exclusively by commuting two different coordinate splits. No semantic equality is admitted as a generating relation.

   inductive Coherent : Tree X → Tree X → Prop
     | refl (t) : Coherent t t
     | symm {s t} : Coherent s t → Coherent t s
     | trans {r s t} : Coherent r s → Coherent s t → Coherent r t
     | split (x) {a b c d} : Coherent a c → Coherent b d →
         Coherent (.split x a b) (.split x c d)
     | interchange {x y : X} (hxy : x≠y) (a b c d) :
         Coherent (.split x (.split y a b) (.split y c d))
           (.split y (.split x a c) (.split x b d))

   Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree

5. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leaves_nonempty line 56
6. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brickSet line 63
7. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brickSet_leaf line 65
8. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brickSet_split line 71
9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.image_comp_comp line 85
10. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Coherent.brickSet_eq line 92
11. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.extract_root line 108

    Source documentation

    If every leaf has already read a bit on x, the x split can be commuted all the way to the root. This is the nontrivial coordinate-coherence step.

    lemma extract_root (x : X) (t : Tree X)
        (h : ∀ i,(t.brick i).word x≠[]) :
        ∃ a b,Coherent t (.split x a b) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Coherent

12. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brickSet_split_injective line 131
13. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brickSet_eq_leaf line 156
14. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.coherent_of_brickSet_eq line 169

    Source documentation

    Completeness of local interchange for finite coloured trees. The proof uses tree induction and root extraction, not an equality-as-relation shortcut.

    lemma coherent_of_brickSet_eq (s t : Tree X) (h : brickSet s=brickSet t) : Coherent s t := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brickSet, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Coherent

15. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.coherent_iff_brickSet_eq line 187
16. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.mapColors line 199
17. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.mapColors_id line 203
18. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.mapColors_comp line 208
19. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Coherent.mapColors line 214
20. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.mapColors_smul_inv line 226
21. inductive OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.OrbitCoherent line 236

    Source documentation

    A single coloured-interchange schema and its acting-group translates, closed under tree contexts. The action's two-transitivity is not hidden in the constructors: it is used explicitly in the completeness theorem below.

    inductive OrbitCoherent (x₀ y₀ : X) : Tree X → Tree X → Prop
      | refl (t) : OrbitCoherent x₀ y₀ t t
      | symm {s t} : OrbitCoherent x₀ y₀ s t → OrbitCoherent x₀ y₀ t s
      | trans {r s t} : OrbitCoherent x₀ y₀ r s → OrbitCoherent x₀ y₀ s t → OrbitCoherent x₀ y₀ r t
      | split (x) {a b c d} : OrbitCoherent x₀ y₀ a c → OrbitCoherent x₀ y₀ b d →
          OrbitCoherent x₀ y₀ (.split x a b) (.split x c d)
      | conjugate (g : Γ) {s t} : OrbitCoherent x₀ y₀ s t →
          OrbitCoherent x₀ y₀ (mapColors (fun x => g • x) s) (mapColors (fun x => g • x) t)
      | interchange (a b c d) :
          OrbitCoherent x₀ y₀ (.split x₀ (.split y₀ a b) (.split y₀ c d))
            (.split y₀ (.split x₀ a c) (.split x₀ b d))
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.mapColors

22. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.OrbitCoherent.coherent line 251
23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.coherent_orbit_complete line 265
24. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.orbitCoherent_iff_brickSet_eq line 283
25. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.element_eq_of_leaves line 300
26. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move.exchange line 305

    Source documentation

    Symmetry of the two subtrees, with its literal untwisted cube chart.

    def exchange [MulAction.IsPretransitive Γ X] (x : X) (a b : Tree X) :
        Move (Γ:=Γ) x (.split x a b) (.split x b a) where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Move

27. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_pentagon line 327

    Source documentation

    The actual associator satisfies the pentagon, proved by its four leaf charts, not imposed on the constructed group as an extra hypothesis.

    lemma associator_pentagon :
        associator (Γ:=Γ) x * associator x =
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator

28. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip_hexagon line 346

    Source documentation

    The actual associator and half swaps satisfy the symmetry hexagon.

    lemma flip_hexagon :
        flip (Γ:=Γ) x = associator x * localize (right x) (flip x) * (associator x)⁻¹ *
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.right

29. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_middle_naturality line 367
30. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_right_naturality line 374
31. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.rightLocalizationSeed line 391

    Source documentation

    The lifted right localization is obtained by the actual half swap.

    def rightLocalizationSeed : Seed (Γ:=Γ) x →* Seed (Γ:=Γ) x :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

32. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_rightLocalizationSeed line 394
33. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralComm line 401
34. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralMiddle line 405
35. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralRight line 409
36. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.pentagonWord line 413
37. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.hexagonWord line 418
38. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralRelations line 424

    Source documentation

    All root-level structural laws are finite after checking naturality and commutation only on a finite generating family of Seed.

    def structuralRelations (s : Finset (Seed (Γ:=Γ) x)) : Finset (Seed (Γ:=Γ) x) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

39. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_structuralComm line 429
40. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_structuralMiddle line 434
41. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_structuralRight line 438
42. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_pentagonWord line 442
43. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.evaluation_hexagonWord line 446
44. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralRelations_valid line 451
45. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.StructuralQuotient line 467

    Source documentation

    Finitely presented structural quotient with genuine evaluation map. The absence of an injectivity assertion is substantive: coloured coherence and label covariance/completeness are still required for the main theorem.

    abbrev StructuralQuotient (s : Finset (Seed (Γ:=Γ) x)) := LocalQuotient x s (structuralRelations x s)

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.LocalQuotient, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralRelations

46. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralQuotient_finitelyPresented line 469
47. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralEvaluation line 472
48. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralEvaluation_surjective line 476
49. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject line 490
50. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_rel line 493
51. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_comm line 497
52. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_middle line 510
53. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_right line 523
54. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_comm_all line 540

    Source documentation

    Infinite naturality families are consequences of their finite generator checks. This is an algebraic reduction, not an appeal to diagram coherence.

    lemma structuralProject_comm_all (g h : Seed (Γ:=Γ) x) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed

55. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_middle_all line 548
56. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_right_all line 560
57. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_left_all line 572
58. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralLocalization line 579

    Source documentation

    The endomorphism exists on the finitely presented structural quotient, not just on its semantic image in the actual table group.

    def structuralLocalization : StructuralQuotient x s →* StructuralQuotient x s :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.StructuralQuotient

59. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralLocalization_project line 582
60. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_flip_square line 587
61. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_pentagon line 593
62. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_hexagon line 597
63. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_surjective line 610
64. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralSymmetry line 613
65. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralAssociator line 614
66. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralSymmetry_square line 616
67. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralSymmetry_inv line 619
68. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralRightLocalization line 622
69. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralRightLocalization_project line 625
70. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralLocalizations_commute line 633
71. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralTensor line 643

    Source documentation

    A genuine binary tensor homomorphism on the actual finite structural quotient. Its functoriality follows from the finitely generated disjointness relations, not from semantic equality after evaluation.

    def structuralTensor : StructuralQuotient (Γ:=Γ) x s × StructuralQuotient x s →*
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.StructuralQuotient

72. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralTensor_apply line 648
73. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralConjugate_left line 652
74. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralConjugate_middle line 660
75. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralConjugate_right line 668
76. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralTensor_associativity line 676

    Source documentation

    Associativity is natural for every morphism of the finite quotient.

    lemma structuralTensor_associativity (g h k : StructuralQuotient (Γ:=Γ) x s) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.StructuralQuotient

77. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralSymmetry_localization line 689
78. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralTensor_symmetry line 703

    Source documentation

    The symmetry is natural, using involutivity and disjointness inside the finite quotient, not merely a relation holding in the semantic group.

    lemma structuralTensor_symmetry (g h : StructuralQuotient (Γ:=Γ) x s) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.StructuralQuotient

79. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralTensor_pentagon line 714
80. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralTensor_hexagon line 722