◂ NRS³

NRS³ · Cristales — la simetría da la forma, el espectro da el tamaño

Una red de Bravais tiene un sitio por celda, y toda red así es simétrica bajo la inversión n ↦ −n. Junto con la inversión temporal, eso obliga a que la energía H y la posición X no estén correlacionadas en toda onda plana: Σ_HX = 0 en todas las direcciones. La entrada que sobrevive, Ω_HX = ⟨⁅H, X⁆⟩, la fija el espectro: en cajas grandes tiende a −½ por la velocidad de grupo de la banda. Elige una red, cambia sus longitudes y el momento, o rompe la simetría con un estado aleatorio y mira cómo reaparece la covarianza. Arrastra la red para girarla. Cada cifra cita su lema de Lean.

a b c región L k_x/π k_y/π k_z/π t

La red y el estado

tamaño |ψ|² · color = fase

Los enlaces naranjas son los vecinos del sitio central, los mismos del grafo de Lean. La flecha violeta es la velocidad de grupo v; la verde punteada, −2 (Ω_HX, Ω_HY, Ω_HZ), a la misma escala: al crecer la región se encima con la violeta.

Σ y Ω de (H, X, Y, Z)

verde = cero forzado por un lema

Robertson 1934: |det Ω| ≤ det Σ (robertson_det), en todo estado. Los pares (X, Y) conmutan: su Ω es cero siempre y solo queda la positividad de la Gram.

Par que no conmuta: (H, X)

Par que conmuta: (X, Y)

La banda y el tamaño de lo que sobrevive

banda en la dirección de k

La banda es ε(k) = −t Σ_δ cos(k·δ) (band), sumando sobre los vectores de enlace. Su pendiente es la velocidad de grupo (hasDerivAt_band). En la región finita, Ω_HX es exactamente una suma sobre los enlaces internos (expectation_bracket_unitPlaneWave). Al crecer la caja tiende a −½ v (tendsto_expectation_bracket_box); mueve región L y míralo acercarse.

Lo que está probado en Lean

Todo está en la rama mosaic-cristales del fork de Physlib y se repite, con su enunciado, en NRS3Cristales/Resumen.lean. Solo usa los axiomas propext, Classical.choice y Quot.sound.

Qué dice	Lema	Archivo

modelo numérico Las cifras de los paneles se calculan en el navegador sobre la región {−L, …, L}³ en coordenadas de red, con salto real −t en cada enlace del grafo. Que Σ_HX salga cero en la onda plana y que Ω_HX coincida con la fórmula exacta no es una aproximación: son los lemas. El límite −½ v se alcanza solo cuando la caja crece. En una caja finita, el valor óptimo exacto es el espectro finito, que para cajas producto de caminos es el cos(π/(N+1)) de la cadena; en FCC o BCC no tiene fórmula cerrada. Faltan en Lean la romboédrica, las dos monoclínicas y la triclínica.