OAI/Algebra/GroupRing/Iso.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Finite names for the actual-image patterns in entropy.tex 126–138. The bounds R,K,T,I are fixed before H grows. No vertex names or letters are stored. Raw codes include invalid multigraphs as an overcount; all validity conditions must still be checked when a code is used in a realization event.

  1. def OAI.TorsionFreeZeroDivisors.PortSubdivision.Iso.sideEmbedding line 22

    Source documentation

    A side-preserving graph isomorphism transports the actual rooted embedding, not just its edge or vertex counts.

    def sideEmbedding (e : RealizationTransport.Embedding (SideRestriction.graph Γ' side' hs' b)
    (fun d => label d.val) outgoing (RootPins.pin (SidePins.root side' root' b) target) bar r) :
    RealizationTransport.Embedding (SideRestriction.graph Γ side hs b)
      (fun d => label (f.dart d.val)) outgoing (RootPins.pin (SidePins.root side root b) target) bar r := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding, OAI.TorsionFreeZeroDivisors.SideRestriction.graph, OAI.TorsionFreeZeroDivisors.RootPins.pin, OAI.TorsionFreeZeroDivisors.SidePins.root

  2. lemma OAI.TorsionFreeZeroDivisors.OriginalPatternIso.length_eq line 65
  3. lemma OAI.TorsionFreeZeroDivisors.OriginalPatternIso.dart_eq line 70
  4. lemma OAI.TorsionFreeZeroDivisors.OriginalPatternIso.realized line 96

    Source documentation

    An unlabeled pattern isomorphism preserves the actual event in each fixed sample. No independence or expected-count assumption is used in this bridge.

    lemma realized (r : Match rep)
    (he : OriginalPattern.Realized Γ' mark' h2' side' hs' paths' hp' root' rep a b C' r) :
    OriginalPattern.Realized Γ mark h2 side hs paths hp root rep a b C r := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.OriginalPattern.Realized

  5. def OAI.TorsionFreeZeroDivisors.PatternCoding.packList line 134

    Source documentation

    A list of at most T chain darts can be stored in T option-valued slots.

    def packList {A : Type*} (T : ℕ) (p : List A) : Fin T → Option A :=
…
  6. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.packList_injective line 137
  7. abbrev OAI.TorsionFreeZeroDivisors.PatternCoding.Interval line 148

    Source documentation

    One interval uses one path index and two integer endpoints.

    abbrev Interval (K H : ℕ) := Fin K × Fin (H+1) × Fin (H+1)
  8. abbrev OAI.TorsionFreeZeroDivisors.PatternCoding.Comparison line 151

    Source documentation

    Two intervals and their comparison sign. Inactive comparison slots are absent.

    abbrev Comparison (K H : ℕ) := Option (Interval K H × Interval K H × Bool)

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.Interval

  9. abbrev OAI.TorsionFreeZeroDivisors.PatternCoding.Code line 156

    Source documentation

    Bounded path sequences, marked graph incidence/reversal, lengths, sides, root designation and interval data. Unused graph indices may be padded. The use of oriented darts avoids choosing orientations of loop chains.

    abbrev Code (R K T I H : ℕ) :=
…
  10. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.card_comparison line 161
  11. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.card_code line 167
  12. def OAI.TorsionFreeZeroDivisors.PatternCoding.coefficient line 177

    Source documentation

    The constant in the polynomial pattern bound depends only on fixed bounds.

    def coefficient (R K T I : ℕ) : ℕ :=
…
  13. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.card_code_polynomial line 180
  14. def OAI.TorsionFreeZeroDivisors.PatternCoding.names line 194

    Source documentation

    The canonical renaming is independent of every target vertex name.

    def names {A : Type*} [Fintype A] (R : ℕ) (h : Fintype.card A ≤ R) : A ↪ Fin R :=
…
  15. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.names_injective line 197
  16. def OAI.TorsionFreeZeroDivisors.PatternCoding.pad line 201

    Source documentation

    Padding a finite table loses none of its entries.

    def pad {A B : Type*} [Fintype A] (R : ℕ) (_h : Fintype.card A ≤ R)
    (default : B) (f : A → B) (i : Fin R) : B :=
…
  17. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.pad_names line 206
  18. def OAI.TorsionFreeZeroDivisors.PatternCoding.endName line 214

    Source documentation

    Thus all the actual comparison endpoints with a ≤H bound fit literally.

    def endName (H : ℕ) (i : ℕ) (hi : i ≤ H) : Fin (H+1) := ⟨i,by omega⟩
  19. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.endName_val line 216
  20. structure OAI.TorsionFreeZeroDivisors.PatternCoding.ActualInterval line 219

    Source documentation

    An actual comparison endpoint. Its path and integer position are retained.

    structure ActualInterval (P : Type*) (H : ℕ) where
…
  21. structure OAI.TorsionFreeZeroDivisors.PatternCoding.ActualComparison line 225

    Source documentation

    The sign records translation versus reflection, not a chosen graph label.

    structure ActualComparison (P : Type*) (H : ℕ) where
…
  22. def OAI.TorsionFreeZeroDivisors.PatternCoding.intervalName line 230
  23. def OAI.TorsionFreeZeroDivisors.PatternCoding.comparisonName line 234
  24. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.intervalName_injective line 238
  25. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.comparisonName_injective line 248
  26. def OAI.TorsionFreeZeroDivisors.PatternCoding.encode line 262

    Source documentation

    Explicit encoding of all source pattern data after suppression. The graph and path carriers can be arbitrary finite types: their old vertex names do not survive. Empty padding is not counted as an actual chain or path.

    def encode {D V P J : Type*} [Fintype D] [Fintype V] [Fintype P] [Fintype J]
    (R K T I H : ℕ) (hR : 0<R)
    (hD : Fintype.card D ≤ R) (hV : Fintype.card V ≤ R)
    (hP : Fintype.card P ≤ K) (hJ : Fintype.card J ≤ I)
    (rev : D → D) (origin : D → V) (side : D → Bool)
    (length : D → Fin (H+1)) (paths : P → List D)
    (root : Option (P × Bool)) (comparisons : J → ActualComparison P H) : Code R K T I H :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.ActualComparison, OAI.TorsionFreeZeroDivisors.PatternCoding.Code

  27. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.encode_preserves line 280

    Source documentation

    Every finite marked multigraph, bounded list of chain traversals, rooted path designation and bounded set of signed comparisons is literally retained in one member of the polynomially counted family.

    theorem encode_preserves {D V P J : Type*} [Fintype D] [Fintype V] [Fintype P] [Fintype J]
    (R K T I H : ℕ) (hR : 0<R)
    (hD : Fintype.card D ≤ R) (hV : Fintype.card V ≤ R)
    (hP : Fintype.card P ≤ K) (hJ : Fintype.card J ≤ I)
    (rev : D → D) (origin : D → V) (side : D → Bool)
    (length : D → Fin (H+1)) (paths : P → List D)
    (root : Option (P × Bool)) (comparisons : J → ActualComparison P H) :
    let c := encode R K T I H hR hD hV hP hJ rev origin side length paths root comparisons
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.ActualComparison, OAI.TorsionFreeZeroDivisors.PatternCoding.encode

  28. lemma OAI.TorsionFreeZeroDivisors.PatternCoding.encoded_paths_injective line 299

    Source documentation

    The bounded-list slots lose no traversal, even if darts are repeated.

    lemma encoded_paths_injective {D : Type*} [Fintype D] (R T : ℕ)
    (hD : Fintype.card D ≤ R) :
    Function.Injective (fun p : {p : List D // p.length ≤ T} =>
      packList T (p.val.map (names R hD))) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.packList, OAI.TorsionFreeZeroDivisors.PatternCoding.names

  29. abbrev OAI.TorsionFreeZeroDivisors.PatternCoding.SizedCode line 317

    Source documentation

    Carrier counts distinguish inactive padding from actual graph indices. The four extra counts are uniformly bounded, independent of H and n.

    abbrev SizedCode (R K T I H : ℕ) :=
…
  30. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.card_sizedCode line 320
  31. def OAI.TorsionFreeZeroDivisors.PatternCoding.rename line 334
  32. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.rename_rank line 337
  33. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.rename_names line 341
  34. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.same_pad line 346
  35. structure OAI.TorsionFreeZeroDivisors.PatternCoding.Data line 355

    Source documentation

    All non-label data of a bounded actual pattern. Proof fields are not encoded, while all data fields are.

    structure Data (D V P J : Type*) (T H : ℕ) where
…
  36. structure OAI.TorsionFreeZeroDivisors.PatternCoding.Isomorphism line 371

    Source documentation

    Exact simultaneous equivalence of graph incidence, orientation, side, length, every path traversal, root path, and comparison intervals.

    structure Isomorphism {T H : ℕ} (a : Data D V P J T H) (b : Data D' V' P' J' T H) where
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.Data

  37. def OAI.TorsionFreeZeroDivisors.PatternCoding.encodeData line 394
  38. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.same_code_canonical_isomorphism line 404

    Source documentation

    Equality of the finite code loses no pattern information: the resulting isomorphism is valid for loops, repeated paths, and repeated comparisons.

    theorem same_code_canonical_isomorphism (a : Data D V P J T H) (b : Data D' V' P' J' T H)
    (cD : Fintype.card D=Fintype.card D') (cV : Fintype.card V=Fintype.card V')
    (cP : Fintype.card P=Fintype.card P') (cJ : Fintype.card J=Fintype.card J')
    (he : encode R K T I H hR hD hV hP hJ a.reverse a.origin a.side a.length a.paths a.root a.comparisons =
      encode R K T I H hR hD' hV' hP' hJ' b.reverse b.origin b.side b.length b.paths b.root b.comparisons) :
    ∃ f : Isomorphism a b, f.dart=rename cD ∧ f.path=rename cP ∧ f.vertex=rename cV := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.Data, OAI.TorsionFreeZeroDivisors.PatternCoding.encode, OAI.TorsionFreeZeroDivisors.PatternCoding.Isomorphism, OAI.TorsionFreeZeroDivisors.PatternCoding.rename

  39. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.same_code_ranked_isomorphism line 476
  40. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.same_code_isomorphism line 488
  41. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.encodeData_complete line 499

    Source documentation

    Equal padded SIZED codes imply actual pattern equivalence, not merely similar numerical bounds or matching cardinalities.

    theorem encodeData_complete (a : Data D V P J T H) (b : Data D' V' P' J' T H)
    (he : encodeData R K T I H hR hD hV hP hJ a =
      encodeData R K T I H hR hD' hV' hP' hJ' b) : Nonempty (Isomorphism a b) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.Data, OAI.TorsionFreeZeroDivisors.PatternCoding.encodeData, OAI.TorsionFreeZeroDivisors.PatternCoding.Isomorphism

  42. theorem OAI.TorsionFreeZeroDivisors.PatternCoding.encodeData_ranked_complete line 509

    Source documentation

    Equal codes additionally preserve the literal rank orientation used in the subdivision realization. This is an output of encoding, not an extra assumption.

    theorem encodeData_ranked_complete (a : Data D V P J T H) (b : Data D' V' P' J' T H)
    (he : encodeData R K T I H hR hD hV hP hJ a =
      encodeData R K T I H hR hD' hV' hP' hJ' b) :
    ∃ f : Isomorphism a b, ∀ d,
      (Fintype.equivFin D' (f.dart d)).val = (Fintype.equivFin D d).val := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternCoding.Data, OAI.TorsionFreeZeroDivisors.PatternCoding.encodeData, OAI.TorsionFreeZeroDivisors.PatternCoding.Isomorphism