MX0017

divisor_pair_index_map_value

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

Any decoded value at a certified coordinate equals the actual coordinate product; equality of beta-code components is not asserted.

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 expanded first-order arithmetic statement

forall V L r s i d e z. (((~((V)=0)) /\ (forall dpi_index_dpi_value_map dpi_row_dpi_value_map dpi_column_dpi_value_map. (exists pvs_gap_dpi_value_mapwindow. pvs_gap_dpi_value_mapwindow + S (dpi_index_dpi_value_map) = (L)) -> (exists pvs_gap_dpi_value_mapremainder. pvs_gap_dpi_value_mapremainder + S (dpi_column_dpi_value_map) = (V)) -> (dpi_index_dpi_value_map)=(V)*(dpi_row_dpi_value_map)+(dpi_column_dpi_value_map) -> (((exists ff_h_pvs_dpi_value_mapvalue. ff_h_pvs_dpi_value_mapvalue + S ((dpi_row_dpi_value_map)*(dpi_column_dpi_value_map)) = S ((S (dpi_index_dpi_value_map)) * s)) /\ exists ff_q_pvs_dpi_value_mapvalue. r = ff_q_pvs_dpi_value_mapvalue * S ((S (dpi_index_dpi_value_map)) * s) + ((dpi_row_dpi_value_map)*(dpi_column_dpi_value_map))))))) -> (exists pvs_gap_dpi_value_index. pvs_gap_dpi_value_index + S (i) = (L)) -> (exists pvs_gap_dpi_value_column. pvs_gap_dpi_value_column + S (e) = (V)) -> i=V*d+e -> (((exists ff_h_pvs_dpi_value_entry. ff_h_pvs_dpi_value_entry + S (z) = S ((S (i)) * s)) /\ exists ff_q_pvs_dpi_value_entry. r = ff_q_pvs_dpi_value_entry * S ((S (i)) * s) + (z))) -> z=d*e

Constructive proof overview

Generated structural guide

Any decoded value at a certified coordinate equals the actual coordinate product; equality of beta-code components is not asserted.

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

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized MX0016 divisor_pair_index_map_lookup

Direct dependents

MX0053 dirichlet_coprime_grid_support_injective

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

32 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.

Named ingredients (1)
divisor pair index map lookup
01Fix variables and assumptionsL1–10

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

  1. L1
    intro V
  2. L2
    intro L
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro i
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro z
  9. L9
    intro hm
  10. L10
    intro hi
02Fix variables and assumptionsL11–13

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

  1. L11
    intro he
  2. L12
    intro heq
  3. L13
    intro hz
03Use earlier factsL14–23

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

  1. L14
    specialize beta_at_unique (r)
  2. L15
    specialize beta_at_unique (s)
  3. L16
    specialize beta_at_unique (i)
  4. L17
    specialize beta_at_unique (z)
  5. L18
    specialize beta_at_unique (d*e)
  6. L19
    apply beta_at_unique
  7. L20
    exact hz
  8. L21
    specialize divisor_pair_index_map_lookup (V)
  9. L22
    specialize divisor_pair_index_map_lookup (L)
  10. L23
    specialize divisor_pair_index_map_lookup (r)
04Use earlier factsL24–32

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

  1. L24
    specialize divisor_pair_index_map_lookup (s)
  2. L25
    specialize divisor_pair_index_map_lookup (i)
  3. L26
    specialize divisor_pair_index_map_lookup (d)
  4. L27
    specialize divisor_pair_index_map_lookup (e)
  5. L28
    apply divisor_pair_index_map_lookup
  6. L29
    exact hm
  7. L30
    exact hi
  8. L31
    exact he
  9. L32
    exact heq

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro V
  2. 0002intro L
  3. 0003intro r
  4. 0004intro s
  5. 0005intro i
  6. 0006intro d
  7. 0007intro e
  8. 0008intro z
  9. 0009intro hm
  10. 0010intro hi
  11. 0011intro he
  12. 0012intro heq
  13. 0013intro hz
  14. 0014specialize beta_at_unique (r)
  15. 0015specialize beta_at_unique (s)
  16. 0016specialize beta_at_unique (i)
  17. 0017specialize beta_at_unique (z)
  18. 0018specialize beta_at_unique (d*e)
  19. 0019apply beta_at_unique
  20. 0020exact hz
  21. 0021specialize divisor_pair_index_map_lookup (V)
  22. 0022specialize divisor_pair_index_map_lookup (L)
  23. 0023specialize divisor_pair_index_map_lookup (r)
  24. 0024specialize divisor_pair_index_map_lookup (s)
  25. 0025specialize divisor_pair_index_map_lookup (i)
  26. 0026specialize divisor_pair_index_map_lookup (d)
  27. 0027specialize divisor_pair_index_map_lookup (e)
  28. 0028apply divisor_pair_index_map_lookup
  29. 0029exact hm
  30. 0030exact hi
  31. 0031exact he
  32. 0032exact heq