MN0002

matrix_skip_index_functional

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

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

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.

Historical partial components only: this chapter proves arbitrary signed cofactor minors and exact signed determinants through dimension four. T13 is now closed by the separate Alpha-v27 integer-linear-algebra branch: arbitrary determinant data, rank, and integer column spans, without a claim of lattice index or normal forms. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ i. ∀ r. ∀ s. ∀ t. MatrixSkipIndex(i,r,s) → MatrixSkipIndex(i,r,t) → s = t

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

MatrixSkipIndex(i,r,s) · 2

Actual proof prerequisites

lt_not_le · checked external prerequisite
Original expanded first-order 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

Complete unchanged native tactic proof

All 35 lines are the exact independently kernel-checked original script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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