RERUN_LOG.txt -- re-runs of the programs of this package, 11 October 2026
Python 3.13.5, mpmath 1.3.0, sympy 1.14.0, numpy 2.5.2; macOS, one laptop.

PART 1.  Output of "sh run_quick.sh", run from an extracted copy of the archive (before this log was added).
Each line: name of the new output (running time): result of the comparison with the recorded output.

python: Python 3.13.5
--- writing_stage (the program of the note)
check_note_output.txt (25 s): identical
--- original (first form of the results)
original_verify_lemma.out (68 s): identical up to running times
original_adversarial_search.out (5 s): identical up to running times
original_verify_theorem1.out (10 s): identical up to running times
original_verify_theoremA_general.out (2 s): identical up to running times
original_construct_divergence.out (5 s): identical up to running times
original_sharpness_examples.out (0 s): identical up to running times
--- earlier_check (the three programs without a time budget)
earlier_t6_misc.out (2 s): identical
earlier_t6b_ftheta_exact.out (0 s): identical
earlier_t8_sum_integral.out (8 s): identical
--- verification_run_A
A_t1_lemma1_families.out (69 s): identical up to running times
A_t5_theoremA.out (6 s): identical up to running times
A_t6_propE_F_appendix.out (17 s): identical up to running times
A_t7_break_iff.out (3 s): identical up to running times
A_t8_sharpness_i_ii.out (0 s): identical
A_t9_symbolic.out (0 s): identical
--- verification_run_B
B_t1_G_lin7_N8.out (1 s): identical up to running times
B_t1_C_ext3_N13.out (1 s): identical up to running times
B_t2_basic.out (1 s): identical up to running times
B_t2_tinyA.out (0 s): identical up to running times
B_t4_Ea.out (18 s): identical up to running times
B_t4_Eb.out (6 s): identical
B_t4_D.out (2 s): identical
B_t4_F.out (0 s): identical
B_t5_11.out (12 s): identical
B_t6_split.out (0 s): identical
B_t7_sharp12.out (0 s): identical
B_t8_refs.out (44 s): identical
RESULT: all quick programs reproduce the recorded outputs

PART 2.  Slow programs, run separately from the same folder layout with the commands given in README.md
(five processes at a time; about 18 minutes in all).  Comparison with the recorded outputs after the
fields that record running times have been removed.

verification_run_A: t1_lemma1_families.py (also part of run_quick.sh): identical up to running times
verification_run_A: t2_lemma1_exhaustive.py K 6, K = 0..5, outputs concatenated: identical up to running times
verification_run_A: t3_lemma1_search.py SEED 100000, SEED = 1..6, outputs concatenated: identical up to running times
verification_run_A: t3_lemma1_search.py SEED 100000 40000, SEED = 11..16, outputs concatenated: identical up to running times
verification_run_A: t4_propB.py: identical up to running times
verification_run_B: t1_exhaustive.py . A_lin5_N10: identical up to running times
verification_run_B: t1_exhaustive.py . A_lin5_N12: identical up to running times
verification_run_B: t1_exhaustive.py . B_geo5_N10: identical up to running times
verification_run_B: t1_exhaustive.py . B_geo5_N12: identical up to running times
verification_run_B: t1_exhaustive.py . C_ext3_N13: identical up to running times
verification_run_B: t1_exhaustive.py . C_ext3_N16: identical up to running times
verification_run_B: t1_exhaustive.py . D_bin_N22: identical up to running times
verification_run_B: t1_exhaustive.py . D_bin_N26: identical up to running times
verification_run_B: t1_exhaustive.py . E_tiny_N10: identical up to running times
verification_run_B: t1_exhaustive.py . E_tiny_N11: identical up to running times
verification_run_B: t1_exhaustive.py . F_abs5_N10: identical up to running times
verification_run_B: t1_exhaustive.py . F_abs5_N11: identical up to running times
verification_run_B: t1_exhaustive.py . G_lin7_N8: identical up to running times
verification_run_B: t1_exhaustive.py . G_lin7_N10: identical up to running times
verification_run_B: t1_exhaustive.py . H_six_N9: identical up to running times
verification_run_B: t1_exhaustive.py . H_six_N10: identical up to running times
verification_run_B: t1_exhaustive.py . J_pow2_N8: identical up to running times
verification_run_B: t1_exhaustive.py . K_abs7_N9: identical up to running times
verification_run_B: t2_families.py . random 101 3000: identical up to running times
verification_run_B: t2_families.py . random 202 3000: identical up to running times
verification_run_B: t2_families.py . random 303 3000: identical up to running times
verification_run_B: t2_families.py . tinyB 1: identical up to running times
verification_run_B: t5_theoremA.py . 22 1500: identical
verification_run_B: claim_instr_verify_lemma.py: identical up to running times
original: verify_lemma.py (also part of run_quick.sh): identical up to running times

Not run again: the six time-budgeted programs of earlier_check/ (t1, t2, t3, t4, t5, t7) and the 25 runs of
verification_run_B/scripts/t3_optimize.py (see README.md).

PART 3.  Re-runs by the final verification run, 11 October 2026 (same machine and versions as above).

(a) "sh run_quick.sh" from an extracted copy of the archive in its first state (the 28 programs of parts
    writing_stage, original, earlier_check, verification_run_A, verification_run_B; the folder
    independent_run_2/ did not exist yet): 13 outputs identical, 15 identical up to running times;
    RESULT: all quick programs reproduce the recorded outputs.

(b) Output of "sh run_quick.sh", run from an extracted copy of the present archive before this part of the log
    was added.  (Changed afterwards: one sentence of main.tex, README texts, and in
    earlier_check/t1_lemma1_families.py one comment line and the text of two assertion messages.  No program of
    the quick part and no recorded output was changed.)

python: Python 3.13.5
--- writing_stage (the program of the note)
check_note_output.txt (33 s): identical
--- original (first form of the results)
original_verify_lemma.out (81 s): identical up to running times
original_adversarial_search.out (5 s): identical up to running times
original_verify_theorem1.out (13 s): identical up to running times
original_verify_theoremA_general.out (2 s): identical up to running times
original_construct_divergence.out (7 s): identical up to running times
original_sharpness_examples.out (0 s): identical up to running times
--- earlier_check (the three programs without a time budget)
earlier_t6_misc.out (2 s): identical up to running times
earlier_t6b_ftheta_exact.out (0 s): identical
earlier_t8_sum_integral.out (9 s): identical
--- verification_run_A
A_t1_lemma1_families.out (97 s): identical up to running times
A_t5_theoremA.out (9 s): identical up to running times
A_t6_propE_F_appendix.out (24 s): identical up to running times
A_t7_break_iff.out (5 s): identical up to running times
A_t8_sharpness_i_ii.out (0 s): identical
A_t9_symbolic.out (0 s): identical
--- verification_run_B
B_t1_G_lin7_N8.out (2 s): identical up to running times
B_t1_C_ext3_N13.out (1 s): identical up to running times
B_t2_basic.out (1 s): identical up to running times
B_t2_tinyA.out (1 s): identical up to running times
B_t4_Ea.out (22 s): identical up to running times
B_t4_Eb.out (8 s): identical
B_t4_D.out (2 s): identical
B_t4_F.out (0 s): identical
B_t5_11.out (14 s): identical
B_t6_split.out (0 s): identical
B_t7_sharp12.out (0 s): identical
B_t8_refs.out (47 s): identical
--- independent_run_2 (the final verification run)
R2_t4_constructions.out (15 s): identical up to running times
R2_t6_characterization.out (12 s): identical up to running times
R2_t5_theorems.out (56 s): identical up to running times
R2_t2_families.out (74 s): identical up to running times
RESULT: all quick programs reproduce the recorded outputs

(c) The two slow programs of independent_run_2/, run from the same extracted copy with five processes, compared
    with the recorded outputs after the fields that record running times have been removed:

independent_run_2: t1_exhaustive.py 5 (85 s): identical up to running times
independent_run_2: t3_search.py 5 40000 (488 s): identical up to running times
