SL000A · theorem body

doubling_gauss_count_shape_exists

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

The explicit reflection-count shape for doubling exists constructively for every odd-prime half.

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.

Statement with defined notation

forall h. exists e. (((h = 2 * e) \/ (exists qst_count_half_shape. h = 2 * qst_count_half_shape + 1 /\ e = S qst_count_half_shape)))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

none

In local proof propositions

none
Exact expanded first-order statement
forall h. exists e. (((h = 2 * e) \/ (exists qst_count_half_shape. h = 2 * qst_count_half_shape + 1 /\ e = S qst_count_half_shape)))

Proof neighborhood

Direct theorem prerequisites

parity_cases · Stable closed

Direct theorem dependents

none

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

13 script commands · 12 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.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro h
02Use earlier factsL2–2

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

  1. L2
    specialize parity_cases h
03Separate the logical casesL3–4

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

  1. L3
    cases parity_cases
  2. L4
    cases parity_cases_witness
04Construct an explicit witnessL5–5

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

  1. L5
    exists x
05Separate the logical casesL6–6

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

  1. L6
    left
06Use earlier factsL7–7

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

  1. L7
    exact parity_cases_witness_left
07Construct an explicit witnessL8–8

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

  1. L8
    exists S x
08Separate the logical casesL9–9

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

  1. L9
    right
09Construct an explicit witnessL10–10

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

  1. L10
    exists x
10Separate the logical casesL11–11

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

  1. L11
    split
11Use earlier factsL12–12

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

  1. L12
    exact parity_cases_witness_right
12Calculate and transport equalitiesL13–13

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

  1. L13
    refl

Library-wide reading audit

Original defined command ledger · 13 lines
  1. 0001intro h
  2. 0002specialize parity_cases h
  3. 0003cases parity_cases
  4. 0004cases parity_cases_witness
  5. 0005exists x
  6. 0006left
  7. 0007exact parity_cases_witness_left
  8. 0008exists S x
  9. 0009right
  10. 0010exists x
  11. 0011split
  12. 0012exact parity_cases_witness_right
  13. 0013refl