TS000X · theorem body

beta_affine_residue_grid_bounded

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

The encoded affine residue grid is an explicit BoundedInto map from its full domain into the modulus.

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

∀ p. ∀ w. ∀ r. ∀ b. ∀ c. ∀ l. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. ∃ m. x = w · y + z ∧ (Lt(z,w) ∧ (r · y + z = p · n + m ∧ (Lt(m,p) ∧ BetaAt(b,c,x,m))))) → ∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,p)

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

PD0002 Lt PD0013 BetaAt

In local proof propositions

PD0002 Lt PD0013 BetaAt
Exact expanded first-order statement
forall p w r b c l. (forall ftrg_index_bounded_source. (exists ftrg_gap_bounded_source_index. ftrg_gap_bounded_source_index + S (ftrg_index_bounded_source) = (l)) -> exists ftrg_row_bounded_source ftrg_column_bounded_source ftrg_quotient_bounded_source ftrg_remainder_bounded_source. ((ftrg_index_bounded_source) = (w) * ftrg_row_bounded_source + ftrg_column_bounded_source /\ ((exists ftrg_gap_bounded_source_column. ftrg_gap_bounded_source_column + S (ftrg_column_bounded_source) = (w)) /\ ((r * ftrg_row_bounded_source + ftrg_column_bounded_source = (p) * ftrg_quotient_bounded_source + ftrg_remainder_bounded_source) /\ ((exists ftrg_gap_bounded_source_residue. ftrg_gap_bounded_source_residue + S (ftrg_remainder_bounded_source) = (p)) /\ (((exists ff_h_ftrg_bounded_source_entry. ff_h_ftrg_bounded_source_entry + S (ftrg_remainder_bounded_source) = S ((S (ftrg_index_bounded_source)) * c)) /\ exists ff_q_ftrg_bounded_source_entry. b = ff_q_ftrg_bounded_source_entry * S ((S (ftrg_index_bounded_source)) * c) + (ftrg_remainder_bounded_source)))))))) -> (forall fom_index_ftrg_bounded. (exists fom_gap_ftrg_bounded_index_bound. fom_gap_ftrg_bounded_index_bound + S (fom_index_ftrg_bounded) = l) -> exists fom_value_ftrg_bounded. ((((exists fom_beta_height_ftrg_bounded_entry. fom_beta_height_ftrg_bounded_entry + S (fom_value_ftrg_bounded) = S ((S (fom_index_ftrg_bounded)) * c)) /\ exists fom_beta_quotient_ftrg_bounded_entry. b = fom_beta_quotient_ftrg_bounded_entry * S ((S (fom_index_ftrg_bounded)) * c) + (fom_value_ftrg_bounded))) /\ (exists fom_gap_ftrg_bounded_value_bound. fom_gap_ftrg_bounded_value_bound + S (fom_value_ftrg_bounded) = p)))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

TS000Z prime_floor_affine_residue_grid_collision

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

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

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–9

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

  1. L1
    intro p
  2. L2
    intro w
  3. L3
    intro r
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro l
  7. L7
    intro hgrid
  8. L8
    intro k
  9. L9
    intro hk
02Use earlier factsL10–10

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

  1. L10
    specialize hgrid k
03Establish hpointL11–13

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

  1. L11
    have hpoint : ∃ i. ∃ j. ∃ q. ∃ t. k = w · i + j ∧ (Lt(j,w) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,k,t))))Definitions: Lt(j,w)Lt(t,p)BetaAt(b,c,k,t)Original native command in the exact edition
  2. L12
    apply hgrid
  3. L13
    exact hk
04Separate the logical casesL14–21

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

  1. L14
    cases hpoint
  2. L15
    cases hpoint_witness
  3. L16
    cases hpoint_witness_witness
  4. L17
    cases hpoint_witness_witness_witness
  5. L18
    cases hpoint_witness_witness_witness_witness
  6. L19
    cases hpoint_witness_witness_witness_witness_right
  7. L20
    cases hpoint_witness_witness_witness_witness_right_right
  8. L21
    cases hpoint_witness_witness_witness_witness_right_right_right
05Construct an explicit witnessL22–22

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

  1. L22
    exists x3
06Separate the logical casesL23–23

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

  1. L23
    split
07Use earlier factsL24–25

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

  1. L24
    exact hpoint_witness_witness_witness_witness_right_right_right_right
  2. L25
    exact hpoint_witness_witness_witness_witness_right_right_right_left

Library-wide reading audit

Original defined command ledger · 25 lines
  1. 0001intro p
  2. 0002intro w
  3. 0003intro r
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro hgrid
  8. 0008intro k
  9. 0009intro hk
  10. 0010specialize hgrid k
  11. 0011have hpoint : ∃ i. ∃ j. ∃ q. ∃ t. k = w · i + j ∧ (Lt(j,w) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,k,t))))
    Exact native replay linehave hpoint : exists i j q t. (k = w * i + j /\ ((exists gap. gap + S j = w) /\ ((r * i + j = p * q + t) /\ ((exists gap. gap + S t = p) /\ (((exists ff_h_ftrg_bounded_point. ff_h_ftrg_bounded_point + S (t) = S ((S (k)) * c)) /\ exists ff_q_ftrg_bounded_point. b = ff_q_ftrg_bounded_point * S ((S (k)) * c) + (t)))))))
  12. 0012apply hgrid
  13. 0013exact hk
  14. 0014cases hpoint
  15. 0015cases hpoint_witness
  16. 0016cases hpoint_witness_witness
  17. 0017cases hpoint_witness_witness_witness
  18. 0018cases hpoint_witness_witness_witness_witness
  19. 0019cases hpoint_witness_witness_witness_witness_right
  20. 0020cases hpoint_witness_witness_witness_witness_right_right
  21. 0021cases hpoint_witness_witness_witness_witness_right_right_right
  22. 0022exists x3
  23. 0023split
  24. 0024exact hpoint_witness_witness_witness_witness_right_right_right_right
  25. 0025exact hpoint_witness_witness_witness_witness_right_right_right_left