Colla z P oo Ve i ica ion: Isabelle/HOL
Isabelle/HOL Ve i ied he P oo and Ce i ica e
Aleksanda Pe išić
Oc obe 2025
Abs ac
This no e gi es a ully explici , lemma-by-lemma speci ica ion o he Lyapuno -ce i ica e
me hod o he accele a ed Colla z map. I is a anged o be di ec ly ansc ibed in o a p o e
Isabelle/HOL and a oids hidden assump ions. The only ex e nal ini e inpu we assume is a
e i ied esidue ce i ica e ( o
k
= 13,ase o 2
12
= 4096 linea inequali ies). We en o ce a
s ic , conse a i e policy on he unique excep ional esidue class
∗
: a
∗
we always ake he
minimal admissible alua ion
2
=
k
and he canonical successo
R⋆
=
odd
(3
∗
+ 1)
mod
2
k
.
S anda d ac s om elemen a y numbe heo y a e s a ed when used and e e enced o
s anda d sou ces. No esul s abou global unc ional g aphs o p obabilis ic heu is ics a e
in oked. All ela ed Isabelle/HOL heo ies, which co e he p oo and beyond, a e ully
execu able, and all sessions build cleanly in Isabelle (all p oo s checked; e e y hing g een).
Con en s
1 Objec s, maps, and s anding no a ion 1
2 Elemen a y 2-adic and esidue ac s (all explici ) 2
3 One-s ep scale decomposi ion and classwise bound 3
4 Fini e ce i ica e hypo hesis (s ic policy) 3
5 Main d i inequali y and elescoping 4
6 Consequences: en y in o a ini e se ; uni o m d i c i e ion 4
7 Ve i ie in e ace and s ic -excep ional lag (speci ica ion) 5
8 Wha is no used 5
9 O e iew o Isabelle Theo ies (Execu able Layou ) 6
10 Closu e Theo y: Re iewe -Facing Lemmas (wi h P oo s) 7
1 Objec s, maps, and s anding no a ion
Accele a ed odd s ep. Fo odd N∈Nde ine
F♯(N) := 3N+ 1
2 2(3N+1) =: odd(3N+ 1),
whe e
2
(
m
)is he 2-adic alua ion ( he exponen o 2in
m
) and
odd
(
m
) :=
m/
2
2(m)
is he
odd pa o m.
1
Modulus and esidue se . Fix an in ege k≥1, se M:= 2k, and le
S:= { ∈ {0,1,...,M −1}: odd }={1,3,...,2k−1}.
Residue dynamics. De ine he esidue map Fk:S→Sby
Fk( )≡odd(3 + 1) (mod 2k).
Excep ional class. Since
gcd
(3
,
2
k
) = 1,3has a unique in e se modulo 2
k
. De ine
∗≡ −
3
−1
(mod 2k). Then ∗is he unique odd class wi h 3 ∗+ 1 ≡0 (mod 2k).
Lemma 1.1 (Exis ence/uniqueness o
∗
).The e is a unique
∗∈S
wi h 3
∗
+ 1
≡
0 (
mod
2
k
).
P oo .
Elemen a y modula a i hme ic (e.g. [
1
, Ch. 2]): since 3is in e ible mod 2
k
, he cong u-
ence 3
≡ −
1has he unique solu ion
≡ −
3
−1
modulo 2
k
, and he in e se o an odd is odd, so
∈S.
S ic excep ional policy. We ix he successo a ∗ o be he canonical
R⋆:= Fk( ∗)≡odd(3 ∗+ 1) (mod 2k).
De ine he s ic esidue policy Rnex :S→Sby
Rnex ( ) := (R⋆, = ∗,
Fk( ), = ∗.
We use
Rnex
e e ywhe e in he ce i ica e and in he d i , ne e mixing i wi h any “obse ed”
al e na i e a ∗.
2 Elemen a y 2-adic and esidue ac s (all explici )
Lemma 2.1 (Odd-pa ac o iza ion).Fo any
n≥
1one has
n
=
odd
(
n
)
·
2
2(n)
wi h
odd
(
n
)
odd and 2(n)∈N.
P oo .
De ine
2
(
n
)as he la ges
such ha 2
|n
; hen
n/
2
is odd by maximali y. (See [
1
,
Ch. 5].)
Lemma 2.2 (Residue de e mines alua ion o
∗
).Fix
k≥
1. Le
∈S
,
=
∗
, and se
:= 2(3 + 1). Then <kand o e e y odd N≡ (mod 2k)one has 2(3N+ 1) = .
P oo .
W i e any odd
N
wi h
N≡
(
mod
2
k
)as
N
=
+2
km
. Then 3
N
+1 = (3
+1)+3
·
2
km
.
W i e 3
+ 1 = 2
u
wi h
u
odd. I
=
∗
hen 2
k∤
(3
+ 1) so
<k
. Now 3
·
2
km
= 2
(3
·
2
k− m
)
has e en b acke , hence
3N+ 1 = 2 u+ 3 ·2k− m
| {z }
e en
has odd b acke ; hus 2(3N+ 1) = . (Pu e 2-adic bookkeeping; c . [2, §3].)
Lemma 2.3 (Excep ional-class lowe bound).I
N
is odd wi h
N≡ ∗
(
mod
2
k
), hen
2
(3
N
+
1) ≥k.
P oo .
W i e
N
=
∗
+ 2
km
. Then 3
N
+ 1 = (3
∗
+ 1) + 3
·
2
km
and 2
k|
(3
∗
+ 1) by de ini ion,
so 2k|(3N+ 1); hence 2(3N+ 1) ≥k.
2
3 One-s ep scale decomposi ion and classwise bound
Scale and co ec ion. De ine
ε
(
N
) :=
ln
(1 +
1
3N
) o odd
N≥
1. No e
ε
(
N
)
∈
(0
,ln
(4
/
3)]
and ε(N)↓0as N↑ ∞.
Lemma 3.1 (Exac one-s ep log decomposi ion).Fo odd N≥1,
ln F♯(N)−ln N= ln 3 − 2(3N+ 1) ln 2 + ε(N).
P oo .
By Theo em 2.1 wi h
n
= 3
N
+1,
ln odd
(3
N
+1) =
ln
(3
N
+1)
− 2
(3
N
+1)
ln
2
.
Sub ac
ln Nand use ln(3N+1)−ln N= ln 3 + ln(1 + 1
3N).
Classwise bound a( ).De ine
a( ) :=
ln 3 − 2(3 + 1) ln 2, = ∗,
ln 3 −kln 2, = ∗.
Lemma 3.2 (Residue-wise s ep bound).Fix
k≥
1and
∈S
. Fo e e y odd
N≡
(
mod
2
k
),
ln F♯(N)−ln N≤a( ) + ε(N).
P oo .
I
=
∗
, hen by Theo em 2.2,
2
(3
N
+ 1) =
2
(3
+ 1) and he claim ollows om
Theo em 3.1. I
=
∗
, hen
2
(3
N
+1)
≥k
by Theo em 2.3, so
ln
3
− 2
(3
N
+1)
ln
2
≤ln
3
−kln
2;
again apply Theo em 3.1.
Lemma 3.3 (Conse a i eness o he excep ional policy).I he obse ed alua ion a
∗
is
2(3 ∗+ 1) = k+ ∆ wi h ∆≥0, hen
(ln 3 −(k+ ∆) ln 2) ≤(ln 3 −kln 2) = a( ∗).
Hence eplacing
2
by
k
a
∗
makes
a
(
∗
)la ge (a s ic e inequali y) and is he e o e conse -
a i e.
P oo . Immedia e om ∆≥0and ln 2 >0.
4 Fini e ce i ica e hypo hesis (s ic policy)
De ini ion 4.1 (Ce i ica e da a).Fix ϕ:S→Rand pa ame e s δ > 0,ρ≥0.
De ini ion 4.2 (S ic -policy ce i ica e inequali ies).We say (
ϕ, δ, ρ
)is a one-s ep ce i ica e
(a k) i
a( ) + ρ+ϕRnex ( )+δ≤ϕ( ) (∀ ∈S).
Rema k 4.3 (Fini e check).Fo
k
= 13 we ha e
|S|
= 2
12
= 4096 cons ain s. In his documen
we assume hey a e e i ied in e al- igo ously by code; his ini e ac is he unique ex e nal
inpu . (Algo i hmic backg ound: max-plus di e ence cons ain s / Bellman–Fo d and Ka p’s
cycle-mean cha ac e iza ion [4, 5].)
3
5 Main d i inequali y and elescoping
Theo em 5.1 (One-s ep s ic -policy d i ).Assume he ce i ica e inequali ies
(4.2)
hold. Fix
k≥1. Le Nbe odd wi h N≥1, and le := Nmod 2k( educed o S). Then
ln F♯(N)+ϕ
Rnex ( )≤ln N+ϕ( )−h(δ+ρ)−ε(N)i.
P oo .
By Theo em 3.2,
ln F♯
(
N
)
−ln N≤a
(
) +
ε
(
N
)
.
By he ce i ica e a
,
a
(
) +
ρ
+
ϕ(Rnex ( ))+δ≤ϕ( ).Add he wo and ea ange.
De ini ion 5.2 (Decoupled Lyapuno p o ile).Fo an odd
N
wi h esidue
=
Nmod
2
k
de ine
V(N, ) := ln N+ϕ( ).
Gi en any odd ajec o y
N +1
=
F♯
(
N
)and a de e minis ic esidue chain
+1
=
Rnex
(
)
(ini ialized by 0:= N0mod 2k), w i e V := V(N , ).
P oposi ion 5.3 (Pe -s ep dec ease).Unde Theo em 4.2, o all ≥0,
V +1 ≤V −h(δ+ρ)−ε(N )i.
P oo . Apply Theo em 5.1 o (N , )a each s ep.
Theo em 5.4 (Telescoping).Fix J∈N. Then
VJ≤V0−
J−1
X
=0 h(δ+ρ)−ε(N )i.
P oo . Sum Theo em 5.3.
6 Consequences: en y in o a ini e se ; uni o m d i c i e ion
Lemma 6.1 (Uni o m bound on
ε
).Fo
N≥
1,
ε
(
N
) =
ln
(1 +
1
3N
)
∈
(0
,ln
(4
/
3)] and is s ic ly
dec easing in N.
P oo . Elemen a y calculus (mono onici y o ln(1 + x),x > 0).
Co olla y 6.2 (Fini e-en y p inciple).Assume δ+ρ < ln(4/3). Fix ζ⋆∈(0, δ +ρ)and
N⋆:= l1
3eζ⋆−1m,
so ha ε(N)≤ζ⋆ o all N≥N⋆. I N ≥N⋆ o 0≤ <J hen
VJ≤V0−J(δ+ρ)−ζ⋆.
Hence he odd alues mus e en ually en e {1,3, . . . , N⋆−2}.
P oo .
By Theo em 6.1,
ε
(
N
)
≤ζ⋆
on [0
, J
), so each s ep dec eases
V
by a leas (
δ
+
ρ
)
−ζ⋆>
0;
elescope.
P oposi ion 6.3 (Uni o m one-s ep dec ease c i e ion).I
ε
(
N
)
≤δ
+
ρ−η
o all odd
N≥N0
and some
η >
0, hen
V
s ic ly dec eases by a leas
η
as long as
N ≥N0
. In pa icula , i
ε(3) ≤δ+ρ hen he odd subsequence is s ic ly dec easing o all N≥3.
P oo . Immedia e om Theo em 5.3.
4
7 Ve i ie in e ace and s ic -excep ional lag (speci ica ion)
This sec ion speci ies he minimal unc ionali y a checke mus implemen o ce i y Theo em 4.2
wi h he s ic excep ional policy.
Inpu s
•k∈N,k≥1; se M= 2k,S={1,3,...,2k−1}.
•Table ϕ:S→R( a ional o loa ing wi h in e al w appe s).
•Pa ame e s δ > 0,ρ≥0wi h δ+ρ < ln(4/3).
•
S ic -excep ional policy lag (“
– o ce-excep ional
”): a
∗
o ce
2
:=
k
and a ge
R⋆:= Fk( ∗), as in Theo em 3.3.
Checks
Fo each ∈S:
1. Compu e a( ):
a( ) = (ln 3 − 2(3 + 1) ln 2, = ∗,
ln 3 −kln 2, = ∗(en o ced),
and Rnex ( ):Rnex ( ) = R⋆i = ∗,else Fk( ).
2. Ve i y he inequali y a( )+ρ+ϕ(Rnex ( ))+δ≤ϕ( ).
In e al igo (op ional bu ecommended)
Sandwich
ln
2
,ln
3by a ionals
L2< U2
,
L3< U3
and compu e a p o able uppe bound
Uρ≥ρ
o use in he le -hand side bound
U3− 2(3 + 1) L2
| {z }
uppe bounds ln 3− 2ln 2
+Uρ+ϕ(Rnex ( )) + δ≤ϕ( ).
This emo es loa ing-poin isk. (See gene al in e al echniques in [6, Ch. 2] i desi ed.)
8 Wha is no used
No assump ion on he global s uc u e o Fk, no equidis ibu ion, no heu is ic a e aging; only:
•elemen a y 2-adic ac s (Theo ems 2.2 and 2.3),
• he exac one-s ep decomposi ion (Theo em 3.1),
•a ini e ce i ica e unde he s ic policy (Theo em 4.2),
•and elescoping.
Acknowledgmen s
We in en ionally sepa a ed he esidue chain (d i en by
Rnex
) om he in ege chain o a oid
any hidden dependence on he excep ional a ge . This ma ches a clean p o e a chi ec u e.
5
9 O e iew o Isabelle Theo ies (Execu able Layou )
This sec ion documen s he logical and execu able oles o he Isabelle/HOL heo ies used o
mechanize he ce i ica e-d i en a gumen , wi h names ma ching he heo y iles.
Colla z_Ce i ica e_C i icalPa hNew
.This heo y p o ides he co e numbe - heo e ic
sca olding and he max-plus/di e ence-cons ain s algeb a. I o malizes: (i) 2-adic ac s (
2
and
odd
(
·
)), (ii) he accele a ed odd-s ep
F♯
and he esidue map
Fk
on
S
=
{
1
,
3
,...,
2
k−
1
}
, (iii)
closed- o m cycle/mean-slack ela ions, b idge cons ain s, and igh pe -edge inequali ies ha
unde lie easibili y o a po en ial
ϕ
. I also exposes “b idge” lemmas ensu ing ha ce i ica e
inequali ies glue co ec ly ac oss modula phases (pa i y and modulus 2k).
Colla z_K13_Phi_Pai s
.This is he conc e e, ini e, execu able da ase o
k
= 13: a lis o
phi-pai s
( , ϕ( ) ), ∈S={1,3,...,213 −1},
oge he wi h he successo
Fk
(
)and he
2
(3
+ 1) in o ma ion needed o build he le -hand
sides o all ce i ica e inequali ies. The heo y packages he able as Isabelle alues (e icien
lis s/maps) wi h o ali y and domain lemmas “ o ee” om cons uc ion.
Colla z_K13_B_In e nal_Checke
.This heo y de ines compu able p edica es ha e i y,
esidue-by- esidue, ha he CSV/ able en ies sa is y he equi ed inequali y
a( ) + ρ+ϕ(Fk( )) + δ≤ϕ( ),
unde he s ic excep ional policy (canonical a ge a he unique
†
and conse a i e alua ion
a
†
). The main boolean
all_checks_ok
educes he ini e amily o linea checks o a single bi ;
p oo s show ha all_checks_ok =T ue implies he abs ac ce i ica e p ope y.
Colla z_K13_B_Ve i ie
.This b idges he in e nal checke o a human- acing
e i ie _OK
s a emen and de i es s uc u al co olla ies. I es ablishes ha he impo ed phi- able is o al
on
S
(
phi_de ined_on_S
), ha he op ion-
B
/s ic -excep ional policy is he one being en o ced,
and ha he checke ’s boolean indeed implies he uni e sal amily o ce i ica e inequali ies. In
sho : all_checks_ok ⇒ e i ie _OK, plus con enience lemmas o subsequen d i a gumen s.
Colla z_K13_Closu e
.This heo y packages “ e iewe - acing” consequences: exis en ial/leas -
alue p inciples o
ϕ
, boundedness o he Lyapuno p o ile
V
(
N,
) :=
ln N
+
ϕ
(
)on
S
, and
he s epwise/ elescoping d i ha yields e en ual dec ease/en y esul s. I u ns he aw
e i ica ion bi
e i ie _OK
in o s a emen s one ypically wan s o ci e in a na a i e p oo (e.g.
“
ϕ
a ains a minimum on
S
”, “
V
is bounded below uni o mly on he esidue classes”, “e en ual
d op below a ixed h eshold”).
Colla z_K13_Flip_Tes s
.A ligh weigh nega i e es ha ness ha sani y-checks he wi ing
be ween he impo ed
ϕ
- able and he e i ie p edica es. I de ines local copies o he
k=
13
pa ame e s (
k13
,
_s a
,
M
,
S
,
S_lis
), a simpli ied ansi ion
Rnex
(special only a
⋆=
5461),
a local
a
(
·
)(nonze o only a
⋆
), and a
ϕ
lookup om
phi_pai s
. I hen in oduces execu able
booleans
ineq_ok,b idge_ok_s ong,b idge_ok_exc, e i ie _OK, e i ie _OK_wi h_exc
and p o es “ lip” lemmas showing hese ail unde con olled pe u ba ions: (i) o cing
ϕ
(5461)
<
h _5461
b eaks
ineq_ok
; (ii) choosing
b <
0(wi h
ln
2
>
0) b eaks
b idge_ok_s ong
6
since
Fk
=
Rnex
; (iii) lis ing an excep ional a ge
wi h
ϕ
(
)
> ϕ
(
Rnex ⋆
) +
bln
2b eaks
b idge_ok_exc
. The ile hus p o ides e iewe - acing uni es s: i does no asse new Colla z
ac s, bu con i ms he e i ie lags go alse exac ly when expec ed.
10 Closu e Theo y: Re iewe -Facing Lemmas (wi h P oo s)
In his sec ion we p esen lemmas ha mi o he logical con en o
Colla z_K13_Closu e
,
s a ed and p o ed in a compac ma hema ical s yle. They a e in ended as di ec answe s o
na u al e iewe ques ions (“wha exac ly is being used/claimed a his poin ?”). Th oughou ,
assume he s ic excep ional policy, he ixed pa ame e s
δ >
0,
ρ≥
0, and he e i ied amily
o ce i ica e inequali ies
a( ) + ρ+ϕ(Fk( )) + δ≤ϕ( ) (∀ ∈S),
wi h
S
=
{
1
,
3
,...,
2
k−
1
}
and
k
= 13 ( he
k
- ixed p esen a ion is pu ely conc e e; he a gumen s
a e schema ic).
Lemma 10.1 (Ce i ica e inequali ies om e i ie _OK).I
e i ie _OK
holds, hen o e e y
∈S,
a( )+ρ+ϕ(Fk( ))+δ≤ϕ( ).
P oo .
By cons uc ion, e i ie _OK is de ined as he logical image o he execu able p edica e
all_checks_ok, which enume a es all esidues
∈S
and e i ies he displayed inequali y using he
s ic -excep ional policy a
†
. The
all_checks_ok ⇒
uni e sal inequali y implica ion is p o ed
in he Ve i ie heo y; we euse i .
Lemma 10.2 (To ali y and ini eness).
ϕ
is o al on
S
and
S
is ini e. Consequen ly,
ϕ
(
S
)is a
ini e subse o R.
P oo .
To ali y on
S
is es ablished in he e i ie laye om he impo ed able (
phi_de ined_on_S
).
Fini eness o Sis immedia e: |S|= 2k−1. Hence ϕ(S)is ini e.
Lemma 10.3 (Exis ence o a minimal po en ial alue).The e exis s min ∈Ssuch ha
ϕ( min) = min{ϕ( ): ∈S}.
Mo eo e , o any ∈S he e holds ϕ( min)≤ϕ( ).
P oo .
By Theo em 10.2,
ϕ
(
S
)is a ini e nonemp y subse o
R
; hence i has a minimum, a ained
a some min ∈S.
Lemma 10.4 (Uni o m lowe bound o
V
on esidue classes).De ine
V
(
N,
) :=
ln N
+
ϕ
(
)
o odd N≥1wi h esidue ∈S. Then o each ixed ∈S,
in
N∈2N+1 V(N, )>−∞.
P oo .
Fo ixed
,
ϕ
(
)is cons an and
ln N
is bounded below on
N≥
1(indeed
ln N≥
0 o
N≥1). Thus V(N, )≥ϕ( ) o all odd N≥1, gi ing a ini e lowe bound.
Lemma 10.5 (Pe -s ep d i unde he ce i ica e).Le Nbe odd wi h esidue := Nmod 2k.
Then
(ln F♯(N)+ϕ(Fk( ))) −(ln N+ϕ( )) ≤ −(δ+ρ)−ε(N),
whe e ε(N) = ln
1 + 1
3N.
7
P oo .
F om he one-s ep decomposi ion
ln F♯
(
N
)
−ln N
=
ln
3
− 2
(3
N
+ 1)
ln
2 +
ε
(
N
)and
he classwise bound
ln
3
− 2
(3
N
+ 1)
ln
2
≤a
(
), we ob ain
ln F♯
(
N
)
−ln N≤a
(
) +
ε
(
N
).
Adding he ce i ica e inequali y a( ) + ρ+δ+ϕ(Fk( )) ≤ϕ( )yields he claim.
Lemma 10.6 (Telescoping dec ease).Le (
N
)
≥0
be he odd accele a ed sequence and
:=
N mod 2k. De ine V := ln N +ϕ( ). Then o all J≥1,
VJ≤V0−
J−1
X
=0 (δ+ρ)−ε(N ).
P oo . Sum he inequali y o Theo em 10.5 o e = 0, . . . , J −1and elescope.
Lemma 10.7 (E en ual d op below a h eshold).Fix
η∈
(0
, δ
+
ρ
). The e exis s
Nη
such ha
o e e y s ep wi h N ≥Nη,
V +1 ≤V −η.
Consequen ly, ei he he odd alues e en ually en e he ini e se
{
1
,
3
,...,
2
Nη−
1
}
o
V
dec eases wi hou bound, con adic ing Theo em 10.4; hence en y occu s.
P oo .
Choose
Nη
so ha
ε
(
N
)
≤δ
+
ρ−η
o all
N≥Nη
; hen apply Theo em 10.5. The
al e na i e a gumen ollows om Theo em 10.4.
Lemma 10.8 (Closu e o he ce i ica e unde s ic excep ional policy).Le
†
be he unique
class wi h 3
†
+ 1
≡
0 (
mod
2
k
). I , a
†
, he inequali y is en o ced wi h conse a i e alua ion
2
:=
k
and canonical successo
Fk
(
†
), hen he ce i ica e emains alid and all abo e lemmas
hold unchanged.
P oo .
A
†
he conse a i e choice inc eases
a
(
†
)(i.e. makes he le -hand side la ge ) ela i e
o any obse ed alua ion
k
+ ∆ wi h ∆
≥
0. Hence he co esponding inequali y becomes
s ic ly ha de and i s sa is ac ion implies he non-conse a i e e sion. All subsequen lemmas
depend only on he amily o ce i ica e inequali ies and he e o e emain alid.
Rema k (Execu able s a us). Each lemma abo e co esponds o a named ac in he
Closu e
he-
o y:
ce _ineq_ o al_o _OK
(Theo em 10.1),
ini e_phi_image
/
phi_pai s_nonemp y_i _ o al
(Theo em 10.2),
phi_min_le_any
(Theo em 10.3),
V_lowe _bound_on_S
(Theo em 10.4), and
he d i / elescoping and e en uali y lemmas (Theo ems 10.5 o 10.7). They a e s uc u ed o
be di ec ly execu able: he hypo heses a e he single p edica e
e i ie _OK
plus ixed pa ame e s,
and conclusions a e algeb aic inequali ies o e eals and na u als, discha ged inside Isabelle/HOL
wi hou addi ional o acles.
Re e ences
[1]
G. H. Ha dy and E. M. W igh , An In oduc ion o he Theo y o Numbe s, 6 h ed., Ox o d
Uni . P ess, 2008. (Uni s mod 2k, in e ses; basic p-adic alua ion laws.)
[2]
K. I eland and M. Rosen, A Classical In oduc ion o Mode n Numbe Theo y, 2nd ed.,
Sp inge GTM 84, 1990. (p-adic alua ions; cong uences; li ing a gumen s.)
[3]
J. C. Laga ias, “The 3
x
+1 p oblem and i s gene aliza ions,” Ame ican Ma hema ical Mon hly
92 (1985), 3–23. (Backg ound on accele a ed maps and olklo e ac s.)
[4]
R. Bellman, Dynamic P og amming, P ince on Uni . P ess, 1957. (Max-plus/di e ence
cons ain s iewpoin .)
8
[5]
R. M. Ka p, “A cha ac e iza ion o he minimum cycle mean in a dig aph,” Disc e e Ma he-
ma ics 23 (1978), 309–311. (Cycle-mean easibili y c i e ion unde lying ce i ica es.)
[6]
N. J. Higham, Accu acy and S abili y o Nume ical Algo i hms, 2nd ed., SIAM, 2002. (Gene al
in e al/ ounding-con ol backg ound.)
9
