Paquetes topados en c y el fin del conteo
⟨m| Hk |n⟩ = 0 si |m − n| > k · S(σ) ≤ S(γ) ≤ log d · γ pasivo
La cadena solo salta entre vecinos: después de k pasos nada conecta sitios a más de k de distancia. Dos paquetes que salen del mismo sitio con m pasos de diferencia quedan anidados: el de atrás nunca alcanza el frente del de adelante, porque los dos están topados en c. Y el viaje termina: el estado de Gibbs guarda la máxima entropía que permite su energía, a lo más log d, y es pasivo; ya no hay nada que contar ni trabajo que sacar.
Un evento empieza, transcurre y termina: en un sitio a distancia r se registra exactamente desde el paso r, nunca antes (el frente llega con amplitud (−t)r), y deja de distinguirse cuando el calor alcanza el estado de Gibbs, nunca después. El orden de salida queda grabado en el orden de llegada: ningún paquete rebasa a otro en c. Y el conteo tiene techo: en una celda finita las diferencias se agotan, el estado de Gibbs es pasivo y la información termina su viaje. No es que se destruya, la evolución es unitaria; es que ya no queda nada que distinguir ni que extraer.
Cada valor y su teorema
| Enunciado | Lean | |
|---|---|---|
| cono de luz: ⟨m| H^k |n⟩ = 0 si |m − n| > k | inner_pow_openHamiltonian_eq_zero | probado |
| el frente llega a tiempo: ⟨n + k| H^k |n⟩ = (−t)^k | inner_pow_openHamiltonian_front | probado |
| ventana del evento: a distancia r, nada antes del paso r y amplitud ≠ 0 en el paso r | event_window | probado |
| paquetes anidados: el de atrás no toca el frente del de adelante | inner_pow_openHamiltonian_front_eq_zero | probado |
| a igual energía, γ tiene la máxima entropía; S(γ) ≤ log d; γ es pasivo | gibbsState_end_of_count | probado |