Dérouler dichotomie sur 1, 3, 5, 7, 9, 11 en cherchant, puis

Les deux traces. Le variant est $V=\text{droite}-\text{gauche}+1$, le nombre d'indices encore candidats.

Pour $v=9$ : la fonction renvoie $4$ au deuxième tour. Pour $v=4$ : après le troisième tour, $\text{gauche}=2>\text{droite}=1$, la boucle s'arrête et la fonction renvoie $-1$.

Le variant décroît bien strictement : $6\to 3$ puis $6\to 2\to 1$. Il ne décroît pas régulièrement de moitié — de $6$ à $3$, puis de $6$ à $2$ : la division entière fait que la coupe n'est pas toujours équilibrée. Ce que la démonstration exige, ce n'est pas « $V$ est divisé par deux » mais « $V$ diminue d'au moins $1$ » ; c'est plus faible, et cela suffit à conclure.

La trace, obtenue par la machine. Plutôt que de recopier à la main, on instrumente la fonction :

def dichotomie_tracee(t, v):
    """Meme algorithme, mais qui renvoie AUSSI la trace des tours."""
    gauche, droite = 0, len(t) - 1
    trace = []
    while gauche <= droite:
        milieu = (gauche + droite) // 2
        trace.append((gauche, droite, milieu, t[milieu], droite - gauche + 1))
        if t[milieu] == v:
            return milieu, trace
        elif t[milieu] < v:
            gauche = milieu + 1
        else:
            droite = milieu - 1
    return -1, trace

t = [1, 3, 5, 7, 9, 11]
assert dichotomie_tracee(t, 9) == (4, [(0, 5, 2, 5, 6), (3, 5, 4, 9, 3)])

r, tr = dichotomie_tracee(t, 4)
assert r == -1
variants = [x[4] for x in tr]
assert variants == [6, 2, 1]
assert all(variants[i] > variants[i + 1] for i in range(len(variants) - 1))

Le dernier assert est la propriété du variant, écrite en Python : une suite strictement décroissante. C'est le seul du lot qui resterait pertinent si l'on changeait le tableau.