DL00B1

matrix_lattice_identity_selected_signed

The actual identity-selected signed submatrix is the original signed square matrix in both component codes.

Alpha v34 checked-use · first admitted v27 · 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.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ d. ∀ ib. ∀ ic. ¬d = 0 → IdentityMatrixSelector(ib,ic,d) → SignedSelectedSubmatrix(ab,ac,bb,bc,d,ib,ic,ib,ic,d,ab,ac,bb,bc)

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

Definition DAG

SignedSelectedSubmatrix(pb,pc,nb,nc,w,rb,rc,cb,cc,q,ub,uc,vb,vc) · 1IdentityMatrixSelector(b,c,l) · 1

Actual proof prerequisites

matrix_lattice_identity_selected_natural
Original expanded first-order statement 
forall ab ac bb bc d ib ic. ~(d = 0) -> (forall mdr_i_signed_identity. (exists mdr_gap_signed_identitybound. mdr_gap_signed_identitybound + S (mdr_i_signed_identity) = (d)) -> (((exists ff_h_mdr_signed_identityentry. ff_h_mdr_signed_identityentry + S (mdr_i_signed_identity) = S ((S (mdr_i_signed_identity)) * ic)) /\ exists ff_q_mdr_signed_identityentry. ib = ff_q_mdr_signed_identityentry * S ((S (mdr_i_signed_identity)) * ic) + (mdr_i_signed_identity)))) -> (((forall mdr_i_identity_selected_signedpositive. (exists mdr_gap_identity_selected_signedpositivebound. mdr_gap_identity_selected_signedpositivebound + S (mdr_i_identity_selected_signedpositive) = ((d) * (d))) -> exists mdr_a_identity_selected_signedpositive. (((exists mdr_r_identity_selected_signedpositivepoint mdr_s_identity_selected_signedpositivepoint mdr_u_identity_selected_signedpositivepoint mdr_v_identity_selected_signedpositivepoint. ((mdr_i_identity_selected_signedpositive = (d) * mdr_r_identity_selected_signedpositivepoint + mdr_s_identity_selected_signedpositivepoint) /\ ((exists mdr_gap_identity_selected_signedpositivepointcolumn. mdr_gap_identity_selected_signedpositivepointcolumn + S (mdr_s_identity_selected_signedpositivepoint) = (d)) /\ ((((exists ff_h_mdr_identity_selected_signedpositivepointrow_index. ff_h_mdr_identity_selected_signedpositivepointrow_index + S (mdr_u_identity_selected_signedpositivepoint) = S ((S (mdr_r_identity_selected_signedpositivepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signedpositivepointrow_index. ib = ff_q_mdr_identity_selected_signedpositivepointrow_index * S ((S (mdr_r_identity_selected_signedpositivepoint)) * ic) + (mdr_u_identity_selected_signedpositivepoint))) /\ ((((exists ff_h_mdr_identity_selected_signedpositivepointcolumn_index. ff_h_mdr_identity_selected_signedpositivepointcolumn_index + S (mdr_v_identity_selected_signedpositivepoint) = S ((S (mdr_s_identity_selected_signedpositivepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signedpositivepointcolumn_index. ib = ff_q_mdr_identity_selected_signedpositivepointcolumn_index * S ((S (mdr_s_identity_selected_signedpositivepoint)) * ic) + (mdr_v_identity_selected_signedpositivepoint))) /\ (((exists ff_h_mdr_identity_selected_signedpositivepointsource. ff_h_mdr_identity_selected_signedpositivepointsource + S (mdr_a_identity_selected_signedpositive) = S ((S ((mdr_u_identity_selected_signedpositivepoint) * (d) + (mdr_v_identity_selected_signedpositivepoint))) * ac)) /\ exists ff_q_mdr_identity_selected_signedpositivepointsource. ab = ff_q_mdr_identity_selected_signedpositivepointsource * S ((S ((mdr_u_identity_selected_signedpositivepoint) * (d) + (mdr_v_identity_selected_signedpositivepoint))) * ac) + (mdr_a_identity_selected_signedpositive)))))))) /\ (((exists ff_h_mdr_identity_selected_signedpositiveoutput. ff_h_mdr_identity_selected_signedpositiveoutput + S (mdr_a_identity_selected_signedpositive) = S ((S (mdr_i_identity_selected_signedpositive)) * ac)) /\ exists ff_q_mdr_identity_selected_signedpositiveoutput. ab = ff_q_mdr_identity_selected_signedpositiveoutput * S ((S (mdr_i_identity_selected_signedpositive)) * ac) + (mdr_a_identity_selected_signedpositive)))))) /\ (forall mdr_i_identity_selected_signednegative. (exists mdr_gap_identity_selected_signednegativebound. mdr_gap_identity_selected_signednegativebound + S (mdr_i_identity_selected_signednegative) = ((d) * (d))) -> exists mdr_a_identity_selected_signednegative. (((exists mdr_r_identity_selected_signednegativepoint mdr_s_identity_selected_signednegativepoint mdr_u_identity_selected_signednegativepoint mdr_v_identity_selected_signednegativepoint. ((mdr_i_identity_selected_signednegative = (d) * mdr_r_identity_selected_signednegativepoint + mdr_s_identity_selected_signednegativepoint) /\ ((exists mdr_gap_identity_selected_signednegativepointcolumn. mdr_gap_identity_selected_signednegativepointcolumn + S (mdr_s_identity_selected_signednegativepoint) = (d)) /\ ((((exists ff_h_mdr_identity_selected_signednegativepointrow_index. ff_h_mdr_identity_selected_signednegativepointrow_index + S (mdr_u_identity_selected_signednegativepoint) = S ((S (mdr_r_identity_selected_signednegativepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signednegativepointrow_index. ib = ff_q_mdr_identity_selected_signednegativepointrow_index * S ((S (mdr_r_identity_selected_signednegativepoint)) * ic) + (mdr_u_identity_selected_signednegativepoint))) /\ ((((exists ff_h_mdr_identity_selected_signednegativepointcolumn_index. ff_h_mdr_identity_selected_signednegativepointcolumn_index + S (mdr_v_identity_selected_signednegativepoint) = S ((S (mdr_s_identity_selected_signednegativepoint)) * ic)) /\ exists ff_q_mdr_identity_selected_signednegativepointcolumn_index. ib = ff_q_mdr_identity_selected_signednegativepointcolumn_index * S ((S (mdr_s_identity_selected_signednegativepoint)) * ic) + (mdr_v_identity_selected_signednegativepoint))) /\ (((exists ff_h_mdr_identity_selected_signednegativepointsource. ff_h_mdr_identity_selected_signednegativepointsource + S (mdr_a_identity_selected_signednegative) = S ((S ((mdr_u_identity_selected_signednegativepoint) * (d) + (mdr_v_identity_selected_signednegativepoint))) * bc)) /\ exists ff_q_mdr_identity_selected_signednegativepointsource. bb = ff_q_mdr_identity_selected_signednegativepointsource * S ((S ((mdr_u_identity_selected_signednegativepoint) * (d) + (mdr_v_identity_selected_signednegativepoint))) * bc) + (mdr_a_identity_selected_signednegative)))))))) /\ (((exists ff_h_mdr_identity_selected_signednegativeoutput. ff_h_mdr_identity_selected_signednegativeoutput + S (mdr_a_identity_selected_signednegative) = S ((S (mdr_i_identity_selected_signednegative)) * bc)) /\ exists ff_q_mdr_identity_selected_signednegativeoutput. bb = ff_q_mdr_identity_selected_signednegativeoutput * S ((S (mdr_i_identity_selected_signednegative)) * bc) + (mdr_a_identity_selected_signednegative))))))))

Complete tactic proof in conservative notation

All 26 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

26 script commands · 4 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.

Named ingredients (1)
matrix lattice identity selected natural
01Fix variables and assumptionsL1–9

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro bb
  4. L4
    intro bc
  5. L5
    intro d
  6. L6
    intro ib
  7. L7
    intro ic
  8. L8
    intro hd
  9. L9
    intro hidentity
02Separate the logical casesL10–10

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

  1. L10
    split
03Use earlier factsL11–20

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

  1. L11
    specialize matrix_lattice_identity_selected_natural (ab)
  2. L12
    specialize matrix_lattice_identity_selected_natural (ac)
  3. L13
    specialize matrix_lattice_identity_selected_natural (d)
  4. L14
    specialize matrix_lattice_identity_selected_natural (ib)
  5. L15
    specialize matrix_lattice_identity_selected_natural (ic)
  6. L16
    apply matrix_lattice_identity_selected_natural
  7. L17
    exact hd
  8. L18
    exact hidentity
  9. L19
    specialize matrix_lattice_identity_selected_natural (bb)
  10. L20
    specialize matrix_lattice_identity_selected_natural (bc)
04Use earlier factsL21–26

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

  1. L21
    specialize matrix_lattice_identity_selected_natural (d)
  2. L22
    specialize matrix_lattice_identity_selected_natural (ib)
  3. L23
    specialize matrix_lattice_identity_selected_natural (ic)
  4. L24
    apply matrix_lattice_identity_selected_natural
  5. L25
    exact hd
  6. L26
    exact hidentity

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro d
  6. 0006intro ib
  7. 0007intro ic
  8. 0008intro hd
  9. 0009intro hidentity
  10. 0010split
  11. 0011specialize matrix_lattice_identity_selected_natural (ab)
  12. 0012specialize matrix_lattice_identity_selected_natural (ac)
  13. 0013specialize matrix_lattice_identity_selected_natural (d)
  14. 0014specialize matrix_lattice_identity_selected_natural (ib)
  15. 0015specialize matrix_lattice_identity_selected_natural (ic)
  16. 0016apply matrix_lattice_identity_selected_natural
  17. 0017exact hd
  18. 0018exact hidentity
  19. 0019specialize matrix_lattice_identity_selected_natural (bb)
  20. 0020specialize matrix_lattice_identity_selected_natural (bc)
  21. 0021specialize matrix_lattice_identity_selected_natural (d)
  22. 0022specialize matrix_lattice_identity_selected_natural (ib)
  23. 0023specialize matrix_lattice_identity_selected_natural (ic)
  24. 0024apply matrix_lattice_identity_selected_natural
  25. 0025exact hd
  26. 0026exact hidentity