OAI/NumberTheory/Ostmann/Characters/AnchorPairCode.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.anchorSignPair line 12
2. theorem OAI.Ostmann.transferCopySign_sq line 15
3. theorem OAI.Ostmann.transferCopySign_injective line 18
4. theorem OAI.Ostmann.transferred_anchor_pair line 25

   Source documentation

   Normalize by the new bulk parity. Its inverse equals itself, since it is a sign. Both entries come directly from the copied graph, including the cross-copy incoming-pivot coefficient.

   theorem transferred_anchor_pair {H Y : Type*}
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) (a i : H) (α ε : ℤ)
       (hε : ε = 1 ∨ ε = -1)
       (hincoming : b (some (.inl a)) (some (.inl i)) = ε)
       (hpivot : b (some (.inl a)) none = α) (t : Bool) :
       (transferCopySign t * ε * transferredGraph b (.inl (true, a)) (.inl (t, i)),
         transferCopySign t * ε * transferredGraph b (.inl (false, a)) (.inl (t, i))) =
         anchorSignPair α ε t := by
   …

   Mentions: OAI.Ostmann.transferCopySign, OAI.Ostmann.transferredGraph, OAI.Ostmann.anchorSignPair

5. theorem OAI.Ostmann.transferred_anchor_code_preserved line 38

   Source documentation

   Once created, an outside anchor's normalized code is unchanged by every later bulk copy.

   theorem transferred_anchor_code_preserved {H Y : Type*}
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) (y : Y) (i : H)
       (ε : ℤ) (t : Bool) :
       (transferCopySign t * ε) * transferredGraph b (.inr y) (.inl (t, i)) =
         ε * b (some (.inr y)) (some (.inl i)) := by
   …

   Mentions: OAI.Ostmann.transferCopySign, OAI.Ostmann.transferredGraph

6. theorem OAI.Ostmann.anchorSignPair_determines_parity line 45
7. def OAI.Ostmann.copyPathParity line 52
8. theorem OAI.Ostmann.copyPathParity_sign line 56
9. def OAI.Ostmann.finiteCopyPath line 64
10. def OAI.Ostmann.finiteAnchorCode line 67
11. def OAI.Ostmann.finalCopyParity line 70
12. theorem OAI.Ostmann.finiteAnchorCode_prefix_parity line 72
13. theorem OAI.Ostmann.finiteAnchorCode_final_injective line 80

    Source documentation

    All code pairs determine the incoming parities; the final parity then determines the last copy sign as well.

    theorem finiteAnchorCode_final_injective {n : ℕ} (α : Fin n → ℤ)
        (hα : ∀ j, α j = 1 ∨ α j = -1) :
        Function.Injective (fun t : Fin n → Bool => (finiteAnchorCode α t, finalCopyParity t)) := by
    …

    Mentions: OAI.Ostmann.finiteAnchorCode, OAI.Ostmann.finalCopyParity

14. theorem OAI.Ostmann.card_anchorCode_fiber_le_two line 100

    Source documentation

    There are at most two paths with any fixed anchor code.

    theorem card_anchorCode_fiber_le_two {n : ℕ} (α : Fin n → ℤ)
        (hα : ∀ j, α j = 1 ∨ α j = -1) (code : Fin n → ℤ × ℤ) :
        Fintype.card {t : Fin n → Bool // finiteAnchorCode α t = code} ≤ 2 := by
    …

    Mentions: OAI.Ostmann.finiteAnchorCode