PA00FK

mod_two_one_to_odd

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

Congruence to one modulo two supplies an odd witness.

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 n. (exists pmt_u_n_one pmt_v_n_one. n + 2 * pmt_u_n_one = 1 + 2 * pmt_v_n_one) -> (exists pmt_odd_n. n = 2 * pmt_odd_n + 1)

Structural proof guide

Generated structural guide

Congruence to one modulo two supplies an odd witness.

Use the direct prerequisites mod_eq_to_remainder_decomposition, mul_comm as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1), closed numeral normalization (1).

Referenced ingredients

PA002V mod_eq_to_remainder_decomposition PA000H mul_comm

Proof neighborhood

Direct dependencies

PA002V mod_eq_to_remainder_decomposition PA000H mul_comm

Direct dependents

PA00FL mod_two_preserves_parity

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

20 script commands · 12 reading checkpoints · 1 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)
mod eq to remainder decompositionmul comm
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro hone
02Establish hdecompL3–10

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

  1. L3
    have hdecomp : exists q. n = q * 2 + 1
  2. L4
    specialize mod_eq_to_remainder_decomposition 2
  3. L5
    specialize mod_eq_to_remainder_decomposition n
  4. L6
    specialize mod_eq_to_remainder_decomposition 1
  5. L7
    apply mod_eq_to_remainder_decomposition
  6. L8
    intro htwo
  7. L9
    apply PA1
  8. L10
    exact htwo
03Construct an explicit witnessL11–11

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

  1. L11
    exists 0
04Calculate and transport equalitiesL12–12

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L12
    norm_num
05Use earlier factsL13–13

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

  1. L13
    exact hone
06Separate the logical casesL14–14

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

  1. L14
    cases hdecomp
07Construct an explicit witnessL15–15

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

  1. L15
    exists x
08Calculate and transport equalitiesL16–16

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L16
    trans x * 2 + 1
09Use earlier factsL17–17

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

  1. L17
    exact hdecomp_witness
10Calculate and transport equalitiesL18–18

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L18
    congr
11Use earlier factsL19–19

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

  1. L19
    apply mul_comm
12Calculate and transport equalitiesL20–20

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L20
    refl

Library-wide reading audit

Original exact command ledger · 20 lines
  1. 0001intro n
  2. 0002intro hone
  3. 0003have hdecomp : exists q. n = q * 2 + 1
  4. 0004specialize mod_eq_to_remainder_decomposition 2
  5. 0005specialize mod_eq_to_remainder_decomposition n
  6. 0006specialize mod_eq_to_remainder_decomposition 1
  7. 0007apply mod_eq_to_remainder_decomposition
  8. 0008intro htwo
  9. 0009apply PA1
  10. 0010exact htwo
  11. 0011exists 0
  12. 0012norm_num
  13. 0013exact hone
  14. 0014cases hdecomp
  15. 0015exists x
  16. 0016trans x * 2 + 1
  17. 0017exact hdecomp_witness
  18. 0018congr
  19. 0019apply mul_comm
  20. 0020refl