PA008O

scaled_inverse_transport_right

Alpha v34 checked-use theorem · independently closed; not Stable

A scaled inverse survives replacement by a congruent right factor.

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 PA statement

forall p a x y z. (exists esi_mod_left_transport_source esi_mod_right_transport_source. (x * y) + p * esi_mod_left_transport_source = (a) + p * esi_mod_right_transport_source) -> (exists esi_mod_left_transport_argument esi_mod_right_transport_argument. (y) + p * esi_mod_left_transport_argument = (z) + p * esi_mod_right_transport_argument) -> (exists esi_mod_left_transport_result esi_mod_right_transport_result. (x * z) + p * esi_mod_left_transport_result = (a) + p * esi_mod_right_transport_result)

Structural proof guide

Generated structural guide

A scaled inverse survives replacement by a congruent right factor.

Use the direct prerequisites mod_eq_mul_left, mod_eq_symm, mod_eq_trans as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA008Q prime_scaled_inverse_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

27 script commands · 4 reading checkpoints · 2 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 (3)
mod eq mul leftmod eq symmmod eq trans
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro z
  6. L6
    intro hxy
  7. L7
    intro hyz
02Establish hscaledL8–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq mul left.

  1. L8
    have hscaled : exists esi_mod_left_transport_scaled esi_mod_right_transport_scaled. (x * y) + p * esi_mod_left_transport_scaled = (x * z) + p * esi_mod_right_transport_scaled
  2. L9
    specialize mod_eq_mul_left p
  3. L10
    specialize mod_eq_mul_left y
  4. L11
    specialize mod_eq_mul_left z
  5. L12
    specialize mod_eq_mul_left x
  6. L13
    apply mod_eq_mul_left
  7. L14
    exact hyz
03Establish hreverseL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L15
    have hreverse : exists esi_mod_left_transport_reverse esi_mod_right_transport_reverse. (x * z) + p * esi_mod_left_transport_reverse = (x * y) + p * esi_mod_right_transport_reverse
  2. L16
    specialize mod_eq_symm p
  3. L17
    specialize mod_eq_symm (x * y)
  4. L18
    specialize mod_eq_symm (x * z)
  5. L19
    apply mod_eq_symm
  6. L20
    exact hscaled
  7. L21
    specialize mod_eq_trans p
  8. L22
    specialize mod_eq_trans (x * z)
  9. L23
    specialize mod_eq_trans (x * y)
  10. L24
    specialize mod_eq_trans a
04Use earlier factsL25–27

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

  1. L25
    apply mod_eq_trans
  2. L26
    exact hreverse
  3. L27
    exact hxy

Library-wide reading audit

Original exact command ledger · 27 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro z
  6. 0006intro hxy
  7. 0007intro hyz
  8. 0008have hscaled : exists esi_mod_left_transport_scaled esi_mod_right_transport_scaled. (x * y) + p * esi_mod_left_transport_scaled = (x * z) + p * esi_mod_right_transport_scaled
  9. 0009specialize mod_eq_mul_left p
  10. 0010specialize mod_eq_mul_left y
  11. 0011specialize mod_eq_mul_left z
  12. 0012specialize mod_eq_mul_left x
  13. 0013apply mod_eq_mul_left
  14. 0014exact hyz
  15. 0015have hreverse : exists esi_mod_left_transport_reverse esi_mod_right_transport_reverse. (x * z) + p * esi_mod_left_transport_reverse = (x * y) + p * esi_mod_right_transport_reverse
  16. 0016specialize mod_eq_symm p
  17. 0017specialize mod_eq_symm (x * y)
  18. 0018specialize mod_eq_symm (x * z)
  19. 0019apply mod_eq_symm
  20. 0020exact hscaled
  21. 0021specialize mod_eq_trans p
  22. 0022specialize mod_eq_trans (x * z)
  23. 0023specialize mod_eq_trans (x * y)
  24. 0024specialize mod_eq_trans a
  25. 0025apply mod_eq_trans
  26. 0026exact hreverse
  27. 0027exact hxy