这份终点把仿射归纳变量强度削弱和线性函数测试替换分成两次真正的程序改写。第一次维护 h=mi+c，第二次改写比较并在无外部使用时删除 i。两次都要交出目标程序、条件真假与源变量状态，不能只比较最后一个数字。
路线入口见从变化的值到等价的循环测试。输入为数学整数上的规范标量循环，不包含机器回绕、浮点、内存、异常或可观察事件。最后的回绕与浮点例子故意离开合同，用来指出为什么不能直接移植证明。
运行准备
下载标准库参考器，保存在当前目录。需要Python 3.10或更新版本；执行器无网络和输入文件依赖，只向标准输出写JSON。
python foundation-affine-induction-check.py > result.json
python -O foundation-affine-induction-check.py > optimized.json
cmp result.json optimized.json两个输出应逐字节相同，status为PASS。900个固定种子生成输入中，593个正常返回，307个在规定轮次后仍需执行，报告budget_exhausted。后者是已经核对的有限前缀，不应写成“307个程序已经证明发散”。全部断言采用显式检查，不依赖-O会关闭的Python assert。
IR中的表达式是整数、变量名，或(op,left,right)三元组；赋值为(destination,expression)。source_example构造规范循环，strength_reduce输出第一次改写，linear_test_replacement从实际源重新建立递推并尝试第二次改写。失败时最终program为null，reason说明拒绝位置；前阶段合法报告放在strength_reduction字段。
任务一：把非零起点算对，逐头对齐
使用start=2、limit=13、bias=−4、seed=0、prior=99。源初始化sum=seed、j=prior，最后i=start；体内先令j=5i+bias，再累加sum，最后i增加3。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
m=runpy.run_path('foundation-affine-induction-check.py')
p,e=m['source_example']()
q=m['strength_reduce'](p,'i',e)
inp={'start':2,'limit':13,'bias':-4,'seed':0,'prior':99}
a=m['execute'](p,inp); b=m['execute'](q['program'],inp)
print('sites',q['sites'],'carrier',q['carrier'],'delta',q['delta'])
print('target',q['program'])
print('heads',[(s['i'],t[q['carrier']],s['sum'],s['j']) for s,t in zip(a['headers'],b['headers'])])
print('same states',a['headers']==m['visible_headers'](b,p))
print('values',a['value'],b['value'],'counts',a['counts'],b['counts'])
PY五个头上的(i,h,sum,j)应依次为(2,6,0,99)、(5,21,6,6)、(8,36,27,21)、(11,51,63,36)、(14,66,114,51)。返回(114,51)。最后一行h=66是在维护下次条件检查点的表达式，j=51则是最后实际赋值的结果；不能拿一个覆盖另一个。
替换位置是体中第0条j赋值，occurrences为1。源乘法4次、加法12次，目标乘法1次、加法13次；delta的5×3在编译期折叠为15。提交时还应给出全部语法与赋值数，不把只减少乘法当作总指令数减少。
然后做两个错误变体并实际运行。把h更新挪到体开头，得到(174,66)。把h初始化错写成bias，得到(74,41)。前者错在相位，后者错在把非零i₀当成0；两者都不是循环边界的小数值误差。
任务二：改比较后才删除i
在同一输入上执行linear_test_replacement。新界是5×13−4=61，新比较为h<61。请打印源的i序列、目标h序列及每一次真假，而不是只打印新分支文本。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
m=runpy.run_path('foundation-affine-induction-check.py')
for slope,bias in ((5,-4),(-2,9)):
p,e=m['source_example'](slope)
q=m['linear_test_replacement'](p,'i',e)
inp={'start':2,'limit':13,'bias':bias,'seed':0,'prior':99}
a=m['execute'](p,inp); b=m['execute'](q['program'],inp)
h=q['strength_reduction']['carrier']
print('slope',slope,'guard',q['guard_after'],'bound',b['headers'][0][q['bound_name']])
print('source',[(s['i'],m['evaluate'](p['guard'],s)) for s in a['headers']])
print('target',[(s[h],m['evaluate'](q['program']['guard'],s)) for s in b['headers']])
print(a['value'],b['value'],m['visible_headers'](a,p,'i')==m['visible_headers'](b,p,'i'))
PY正斜率的目标检查值是6、21、36、51、66，新界61。负斜率−2且偏移9时，检查值是5、−1、−7、−13、−19，新界−17，条件必须改成h>−17。两份真假都为1、1、1、1、0；负斜率程序返回(−16,−13)。
将负斜率目标的gt故意改为lt，第一轮前就退出，错误返回(0,99)。请解释为何这里i每轮仍加3，比较却要反转：步长控制访问次序，斜率控制两套值刻度之间的次序关系。
正斜率主例的源、仅削弱、再替换测试，乘法分别4、1、2，加法分别12、13、10。第二阶段删除i的4次加法，但多计算一次新界。提交这份分开的账，而不是“两个优化每一步都让所有运算减少”。
任务三：零轮、零斜率与仍活跃的出口
把start改为14。源第一次比较就失败，返回(0,99)。两个正确目标也必须返回(0,99)，并保留j的原值99；最终目标会额外做两次初始化乘法和两次加法，语义保持不等于零轮加速。
接着把斜率改为0。仿射表达式每轮等于bias，第一次强度削弱仍合法；线性测试替换必须报告zero slope is not injective，program为null。m=0把所有i映为同一值，不能从h与bias比较恢复原i<limit的真假。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
m=runpy.run_path('foundation-affine-induction-check.py')
for label,args in (('zero slope',{'slope':0}),('live exit',{'live_exit':True})):
p,e=m['source_example'](**args)
q=m['linear_test_replacement'](p,'i',e)
print(label,q['status'],q['reason'],q['program'])
p,e=m['source_example'](live_exit=True)
inp={'start':2,'limit':13,'bias':-4,'seed':0,'prior':99}
print('live value',m['execute'](p,inp)['value'])
PY活跃出口报告induction live at exit；源返回(114,51,14)。不能用13代替最后的14，也不能省去最后一项。如果体内sum仍直接加i，另一项拒绝为induction still read in body。只有i递增的内部自读不是拒绝理由；算法已证明这个整块递推分量不再通向外部观察。
继续提交两项候选结构拒绝：循环体写bias；循环体写作为步长的参数。检查应在编译候选时失败，而不是等某组数值输出不同再临时禁用优化。
任务四：保留比较种类，正确理解预算
主例i依次2、5、8、11、14，h依次6、21、36、51、66。将目标h<61改成h!=61不会在第四轮退出，且6+15k=61无整数解。正确变换必须保留严格不等式种类；跨过边界不是到达边界。
现在让源本来就是i!=limit，步长仍为3。limit=14时，2+3k=14在k=4成立，源与目标都执行4轮后退出；limit=13时没有非负整数解，这个具体循环持续执行。用30轮预算核对后一份程序，双方报告budget_exhausted，并交出31个循环头对应关系。
PYTHONDONTWRITEBYTECODE=1 python - <<'PY'
import runpy
m=runpy.run_path('foundation-affine-induction-check.py')
for limit in (14,13):
p,e=m['source_example'](relation='ne')
q=m['linear_test_replacement'](p,'i',e)
inp={'start':2,'limit':limit,'bias':-4,'seed':0,'prior':99}
a=m['execute'](p,inp,30); b=m['execute'](q['program'],inp,30)
print(limit,a['status'],b['status'],a['iterations'],len(a['headers']))
print(m['visible_headers'](a,p,'i')==m['visible_headers'](b,p,'i'))
PY步长改成0且初始2<13时，也不会退出。尽管h同样不变，非零斜率仍保证每次比较相同。请区分“某个具体循环有算术发散证明”与“执行器只是走完了指定预算”。不能把所有预算耗尽的生成样例一律宣称已证明发散。
任务五：不能移植的模型与成本证据
使用8位无符号回绕的另一个解释。源i从0开始，while i<100，每轮加1，执行100轮。若错误把数学整数证明用于h=4i，把界400回绕为144并比较h<144，目标只执行36轮。提交i=36、h=144这一条直接反证：源条件真，目标条件假。
这里的错误不在“乘法改加法”必定不适用于回绕，而在模环等式并不保序。若将来加入机器整数优化，必须提供相关范围或单独的比较规则。当前参考器无回绕配置，拒绝把不同语义输入当成同一合同。
浮点也另做一次检查：六次加0.1与0.1×6分别得到0.6和0.6000000000000001。说明舍入使每轮重算与递推可能不同，不能使用本数学整数保持证明。
最后为输入参数增加__iv_value_0、__iv_delta_0、__iv_bound_0，分别给71、72、73。改写必须避开这些名字，并在状态投影中保留原参数；它们虽然长得像临时量，仍是源变量。提交新名字及全部原状态核对结果。
最终材料包括源程序、两个目标程序、各自的初始化/体/条件、全部替换证据、五个主例循环头、正负斜率真假表、零轮返回、四类拒绝或失败变体、预算前缀与真实运算计数。分析成本要包含语法比较、不变性验证、常量折叠和重复检查；动态计数要包含新增初值与新界，不能只统计循环体里消失的乘号。