Lemma: Agent20_CollatzRound2_01a13459_E20_V2.multistep_merge_certificate
A conditional affine certificate transfers an exact meeting of two base orbits and matching coefficients to a whole infinite residue family, with a positive smaller predecessor. All certificate hypotheses are explicit.
Exact formal statement
∀ (r k b ell t0 D a : Nat),
LT.lt.{0} 0 b →
LT.lt.{0} (HAdd.hAdd.{0, 0, 0} b (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell) t0)) r →
Eq.{1} (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter r k)
(HAdd.hAdd.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter b ell)
(HMul.hMul.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.coeff b ell) t0)) →
Eq.{1} (Agent20_CollatzRound2_01a13459_E20_V2.Core.coeff r k)
(HMul.hMul.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.coeff b ell) D) →
LE.le.{0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell) D) (HPow.hPow.{0, 0, 0} 2 k) →
And
(Eq.{1}
(Agent20_CollatzRound2_01a13459_E20_V2.Core.iter
(HAdd.hAdd.{0, 0, 0} r (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 k) a)) k)
(Agent20_CollatzRound2_01a13459_E20_V2.Core.iter
(HAdd.hAdd.{0, 0, 0} b
(HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell)
(HAdd.hAdd.{0, 0, 0} t0 (HMul.hMul.{0, 0, 0} D a))))
ell))
(And
(LT.lt.{0} 0
(HAdd.hAdd.{0, 0, 0} b
(HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell)
(HAdd.hAdd.{0, 0, 0} t0 (HMul.hMul.{0, 0, 0} D a)))))
(LT.lt.{0}
(HAdd.hAdd.{0, 0, 0} b
(HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 ell)
(HAdd.hAdd.{0, 0, 0} t0 (HMul.hMul.{0, 0, 0} D a))))
(HAdd.hAdd.{0, 0, 0} r (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 k) a))))This is a published formal lemma. Its scope is the exact statement above.
Environment availability: available.