MD0003

beta_matrix_cell_exists_unique

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

Every finite beta-coded matrix entry has exactly one actual value.

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 b c w i j. exists n. ((((exists fs_h_matrix_entry. fs_h_matrix_entry + S (n) = S ((S (i * w + j)) * c)) /\ exists fs_q_matrix_entry. b = fs_q_matrix_entry * S ((S (i * w + j)) * c) + (n))) /\ forall m. (((exists fs_h_matrix_other. fs_h_matrix_other + S (m) = S ((S (i * w + j)) * c)) /\ exists fs_q_matrix_other. b = fs_q_matrix_other * S ((S (i * w + j)) * c) + (m))) -> n = m)

Constructive proof overview

Generated structural guide

Every finite beta-coded matrix entry has exactly one actual value.

The unchanged tactic script uses 2 declared prerequisites and contains 26 exact native proof lines.

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

Proof neighborhood

Direct dependencies

MD0001 beta_matrix_cell_exists MD0002 beta_matrix_cell_functional

Direct dependents

none

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

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

Named ingredients (2)
beta matrix cell existsbeta matrix cell functional
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro w
  4. L4
    intro i
  5. L5
    intro j
02Use earlier factsL6–10

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

  1. L6
    specialize beta_matrix_cell_exists b
  2. L7
    specialize beta_matrix_cell_exists c
  3. L8
    specialize beta_matrix_cell_exists w
  4. L9
    specialize beta_matrix_cell_exists i
  5. L10
    specialize beta_matrix_cell_exists j
03Separate the logical casesL11–11

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

  1. L11
    cases beta_matrix_cell_exists
04Construct an explicit witnessL12–12

Supply the displayed value, then prove that it has the required property.

  1. L12
    exists x
05Separate the logical casesL13–13

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

  1. L13
    split
06Use earlier factsL14–14

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

  1. L14
    exact beta_matrix_cell_exists_witness
07Fix variables and assumptionsL15–16

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

  1. L15
    intro m
  2. L16
    intro hm
08Use earlier factsL17–26

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

  1. L17
    specialize beta_matrix_cell_functional b
  2. L18
    specialize beta_matrix_cell_functional c
  3. L19
    specialize beta_matrix_cell_functional w
  4. L20
    specialize beta_matrix_cell_functional i
  5. L21
    specialize beta_matrix_cell_functional j
  6. L22
    specialize beta_matrix_cell_functional x
  7. L23
    specialize beta_matrix_cell_functional m
  8. L24
    apply beta_matrix_cell_functional
  9. L25
    exact beta_matrix_cell_exists_witness
  10. L26
    exact hm

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro i
  5. 0005intro j
  6. 0006specialize beta_matrix_cell_exists b
  7. 0007specialize beta_matrix_cell_exists c
  8. 0008specialize beta_matrix_cell_exists w
  9. 0009specialize beta_matrix_cell_exists i
  10. 0010specialize beta_matrix_cell_exists j
  11. 0011cases beta_matrix_cell_exists
  12. 0012exists x
  13. 0013split
  14. 0014exact beta_matrix_cell_exists_witness
  15. 0015intro m
  16. 0016intro hm
  17. 0017specialize beta_matrix_cell_functional b
  18. 0018specialize beta_matrix_cell_functional c
  19. 0019specialize beta_matrix_cell_functional w
  20. 0020specialize beta_matrix_cell_functional i
  21. 0021specialize beta_matrix_cell_functional j
  22. 0022specialize beta_matrix_cell_functional x
  23. 0023specialize beta_matrix_cell_functional m
  24. 0024apply beta_matrix_cell_functional
  25. 0025exact beta_matrix_cell_exists_witness
  26. 0026exact hm

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