OAI/Combinatorics/MatrixRemoval/BodyRoles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact body signatures and extraction of body roles

All signatures refer to fixedH, including its zero entries.

  1. def OAI.Problem348.BodySignatures52.anchorIndex line 13
  2. def OAI.Problem348.BodySignatures52.bodyIndex line 15
  3. theorem OAI.Problem348.BodySignatures52.fixedH_anchor_anchor line 17
  4. theorem OAI.Problem348.BodySignatures52.fixedH_body_anchor line 21
  5. theorem OAI.Problem348.BodySignatures52.fixedH_anchor_body line 25
  6. theorem OAI.Problem348.BodySignatures52.fixedH_body_body line 29
  7. theorem OAI.Problem348.BodySignatures52.anchor64_row_ne_body_signature line 34

    Source documentation

    No anchor row has either of the two body-row signatures.

    theorem anchor64_row_ne_body_signature (u : Fin 64) (b : Fin 2) :
    (fun v => anchor64 u v) ≠ (fun v : Fin 64 => decide (v.val = b.val)) := by
…

    Mentions: OAI.Problem348.anchor64

  8. theorem OAI.Problem348.BodySignatures52.anchor64_col_ne_body_signature line 42

    Source documentation

    No anchor column has either of the two body-column signatures.

    theorem anchor64_col_ne_body_signature (v : Fin 64) (b : Fin 2) :
    (fun u => anchor64 u v) ≠ (fun u : Fin 64 => decide (u.val = b.val)) := by
…

    Mentions: OAI.Problem348.anchor64

  9. theorem OAI.Problem348.BodySignatures52.zero_ne_body_signature line 49
  10. theorem OAI.Problem348.BodySignatures52.copy_body_row_signature line 55
  11. theorem OAI.Problem348.BodySignatures52.copy_body_col_signature line 64