OAI/NumberTheory/Ostmann/Construction/FinalReassignmentInteraction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.anchorCodeEntry line 10
2. theorem OAI.Ostmann.anchorCodeEntry_sign line 14
3. theorem OAI.Ostmann.distinct_anchor_code_entry line 22
4. theorem OAI.Ostmann.final_reassignment_interaction line 36

   Source documentation

   The small anchor suffices at the final stage because the constructed reassignments preserve final parity. The forward exponent is exactly ±2 and the reverse exponent is zero.

   theorem final_reassignment_interaction {n m : ℕ}
       (α : Fin (n + 1) → ℤ) (hα : ∀ j, α j = 1 ∨ α j = -1)
       (e f : FinalParityReassignments n m) (hef : e ≠ f) :
       ∃ (x : ParityPathSum n × Fin m) (j : Fin (n + 1)) (b : Bool),
         let t := parityPathValue (paritySlotPerm e x).1
   …

   Mentions: OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.ParityPathSum, OAI.Ostmann.parityPathValue, OAI.Ostmann.paritySlotPerm