OAI/Combinatorics/MatrixRemoval/HostSampledPath.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Concrete sampled-path role membership for the canonical host. The input is one common leaf seed and arbitrary within-class offset seeds.

  1. def OAI.Problem348.HostSampledPath.position line 15

    Source documentation

    The variable-position sample, injected into the full host axis.

    def position (h i : ℕ) (hi : i ≤ h) (plus : Bool)
    (z u : Fin (2 ^ h)) : Construction.Position h :=
…

    Mentions: OAI.Problem348.Construction.Position

  2. def OAI.Problem348.HostSampledPath.dummy line 20

    Source documentation

    A sampled dummy position.

    def dummy (h : ℕ) (u : Fin (2 ^ h)) : Construction.Position h :=
…

    Mentions: OAI.Problem348.Construction.Position

  3. theorem OAI.Problem348.HostSampledPath.sample_atLevel line 23
  4. theorem OAI.Problem348.HostSampledPath.sample_hostNode line 33
  5. theorem OAI.Problem348.HostSampledPath.position_shared_leaf line 38
  6. def OAI.Problem348.HostSampledPath.mode line 46

    Source documentation

    Encode the mode at the edge from depth i to depth i+1.

    def mode {h : ℕ} (i : Fin h) (k : Fin 6) : Construction.Mode h :=
…

    Mentions: OAI.Problem348.Construction.Mode

  7. theorem OAI.Problem348.HostSampledPath.mode_level line 49
  8. theorem OAI.Problem348.HostSampledPath.mode_kind line 56
  9. def OAI.Problem348.HostSampledPath.verticalKind line 63
  10. def OAI.Problem348.HostSampledPath.horizontalKind line 67
  11. def OAI.Problem348.HostSampledPath.vertical line 73
  12. def OAI.Problem348.HostSampledPath.horizontal line 75
  13. def OAI.Problem348.HostSampledPath.parity line 78
  14. theorem OAI.Problem348.HostSampledPath.parity_eq_false line 80
  15. theorem OAI.Problem348.HostSampledPath.parity_eq_true line 84
  16. theorem OAI.Problem348.HostSampledPath.vertical_plus_row_first line 87
  17. theorem OAI.Problem348.HostSampledPath.vertical_plus_row_second line 92
  18. theorem OAI.Problem348.HostSampledPath.vertical_minus_row_first line 97
  19. theorem OAI.Problem348.HostSampledPath.vertical_minus_row_second line 102
  20. theorem OAI.Problem348.HostSampledPath.vertical_col_first line 107
  21. theorem OAI.Problem348.HostSampledPath.vertical_col_second line 111
  22. theorem OAI.Problem348.HostSampledPath.horizontal_row_second line 115
  23. theorem OAI.Problem348.HostSampledPath.horizontal_row_first line 119
  24. theorem OAI.Problem348.HostSampledPath.horizontal_plus_col_first line 127
  25. theorem OAI.Problem348.HostSampledPath.horizontal_plus_col_second line 132
  26. theorem OAI.Problem348.HostSampledPath.horizontal_minus_col_first line 139
  27. theorem OAI.Problem348.HostSampledPath.horizontal_minus_col_second line 146