MN0002

matrix_skip_index_functional

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Deleting one coordinate induces a unique source coordinate, including both threshold branches.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall i r s t. ((((exists ff_gap_mdm_lt_result_before. ff_gap_mdm_lt_result_before + S (i) = (r)) /\ s = i) \/ ((exists ff_gap_mdm_le_result_after. ff_gap_mdm_le_result_after + (r) = (i)) /\ s = S i))) -> ((((exists ff_gap_mdm_lt_other_before. ff_gap_mdm_lt_other_before + S (i) = (r)) /\ t = i) \/ ((exists ff_gap_mdm_le_other_after. ff_gap_mdm_le_other_after + (r) = (i)) /\ t = S i))) -> s = t

Constructive proof overview

Generated structural guide

Deleting one coordinate induces a unique source coordinate, including both threshold branches.

The unchanged tactic script uses 1 declared prerequisite and contains 35 exact native proof lines.

Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

lt_not_le Stable theorem; checked-use authorized

Direct dependents

MN0006 beta_matrix_minor_cell_functional

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

35 script commands · 15 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro i
  2. L2
    intro r
  3. L3
    intro s
  4. L4
    intro t
  5. L5
    intro hfirst
  6. L6
    intro hsecond
02Separate the logical casesL7–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hfirst
  2. L8
    cases hfirst_left
  3. L9
    cases hsecond
  4. L10
    cases hsecond_left
03Calculate and transport equalitiesL11–11

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L11
    trans i
04Use earlier factsL12–12

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L12
    exact hfirst_left_right
05Calculate and transport equalitiesL13–13

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L13
    symm
06Use earlier factsL14–14

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L14
    exact hsecond_left_right
07Separate the logical casesL15–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L15
    cases hsecond_right
  2. L16
    exfalso
08Use earlier factsL17–21

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    specialize lt_not_le i
  2. L18
    specialize lt_not_le r
  3. L19
    apply lt_not_le
  4. L20
    exact hfirst_left_left
  5. L21
    exact hsecond_right_left
09Separate the logical casesL22–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L22
    cases hfirst_right
  2. L23
    cases hsecond
  3. L24
    cases hsecond_left
  4. L25
    exfalso
10Use earlier factsL26–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    specialize lt_not_le i
  2. L27
    specialize lt_not_le r
  3. L28
    apply lt_not_le
  4. L29
    exact hsecond_left_left
  5. L30
    exact hfirst_right_left
11Separate the logical casesL31–31

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L31
    cases hsecond_right
12Calculate and transport equalitiesL32–32

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    trans S i
13Use earlier factsL33–33

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L33
    exact hfirst_right_right
14Calculate and transport equalitiesL34–34

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L34
    symm
15Use earlier factsL35–35

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L35
    exact hsecond_right_right

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro i
  2. 0002intro r
  3. 0003intro s
  4. 0004intro t
  5. 0005intro hfirst
  6. 0006intro hsecond
  7. 0007cases hfirst
  8. 0008cases hfirst_left
  9. 0009cases hsecond
  10. 0010cases hsecond_left
  11. 0011trans i
  12. 0012exact hfirst_left_right
  13. 0013symm
  14. 0014exact hsecond_left_right
  15. 0015cases hsecond_right
  16. 0016exfalso
  17. 0017specialize lt_not_le i
  18. 0018specialize lt_not_le r
  19. 0019apply lt_not_le
  20. 0020exact hfirst_left_left
  21. 0021exact hsecond_right_left
  22. 0022cases hfirst_right
  23. 0023cases hsecond
  24. 0024cases hsecond_left
  25. 0025exfalso
  26. 0026specialize lt_not_le i
  27. 0027specialize lt_not_le r
  28. 0028apply lt_not_le
  29. 0029exact hsecond_left_left
  30. 0030exact hfirst_right_left
  31. 0031cases hsecond_right
  32. 0032trans S i
  33. 0033exact hfirst_right_right
  34. 0034symm
  35. 0035exact hsecond_right_right

Separate complete second-wave branches: Full T13 proof · Alpha v27.