TS000X

beta_affine_residue_grid_bounded

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 0 declared prerequisites and contains 25 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

none

Direct dependents

TS000Z prime_floor_affine_residue_grid_collision

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

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.

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 : 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)))))))
  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 exact 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 : 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