WEBVTT 00:00:00.500 --> 00:00:07.155 Abre Cuantización y certificados en la nueva opción de investigación. Son diagnósticos independientes, con 00:00:07.155 --> 00:00:14.285 entradas racionales exactas e hipótesis separadas. La demo guiada cambia los controles reales. Cumplir un 00:00:14.285 --> 00:00:20.560 criterio aritmético es un ingrediente de consistencia. No certifica un modelo completo de unificación gauge 00:00:20.560 --> 00:00:22.500 Higgs. 00:00:23.250 --> 00:00:29.730 Elige C partido por dos. La clase universal no cumple, mientras que los períodos sobre variedades espín 00:00:29.730 --> 00:00:37.585 cerradas de dimensión cuatro sí cumplen. No es una contradicción. Las pruebas usan fondos distintos. La 00:00:37.585 --> 00:00:43.935 prueba universal detecta un período de un medio. En los fondos espín indicados, el período de Y al cuadrado 00:00:43.935 --> 00:00:49.708 es par. Ese hecho topológico es externo a la prueba aritmética Lean. 00:00:50.458 --> 00:00:56.618 Los rombos son clases integrales universales. Los anillos intermedios cumplen solo la prueba de períodos 00:00:56.618 --> 00:01:04.008 espín cerrados de dimensión cuatro. La cruz marca alfa y delta actuales, a beta constante. Selecciona un 00:01:04.008 --> 00:01:11.773 punto en la aplicación y gamma cambia de forma exacta. Son criterios matemáticos, no medidas experimentales. 00:01:11.773 --> 00:01:18.625 Fuera de la ventana, la interfaz indica las coordenadas exactas en lugar de pegar el punto al borde. 00:01:19.375 --> 00:01:26.440 Ahora elige C partido por treinta y seis. La dirección del recubrimiento da un entero, uno. Pero el 00:01:26.440 --> 00:01:32.390 cocarácter del cociente mostrado da uno partido por treinta y seis. Comprobar una dirección cómoda del 00:01:32.390 --> 00:01:39.070 recubrimiento puede omitir un período prohibido. Lee el testigo junto al criterio. La aplicación usa 00:01:39.070 --> 00:01:43.833 fracciones exactas, sin tolerancia de coma flotante. 00:01:44.583 --> 00:01:51.443 Elige A más B. Alfa y beta valen uno; gamma vale siete doceavos. Al cambiar a la base integral, delta es 00:01:51.443 --> 00:01:58.648 cero. Se cumplen ambos criterios. Las contribuciones fraccionarias deben combinarse antes de juzgar la clase 00:01:58.648 --> 00:02:05.667 total. Los controles, el testigo y el resultado exportado usan el mismo cálculo. 00:02:06.417 --> 00:02:12.652 El panel del axión usa la normalización de Choi y colaboradores. La combinación entera dieciocho K dos más 00:02:12.652 --> 00:02:19.287 veinticuatro K tres más K uno debe ser divisible por treinta y seis. El ejemplo cero, uno, doce la 00:02:19.287 --> 00:02:26.542 satisface. Reproduce el criterio publicado para q igual a seis. Identificar este axión con el campo Higgs 00:02:26.542 --> 00:02:31.208 gauge sigue siendo una cuestión física distinta y no resuelta. 00:02:31.958 --> 00:02:37.988 El mapa parental tiene dos columnas y un anulador común. Con el espectro heredado y fuentes Green Schwarz 00:02:37.988 --> 00:02:44.498 integrales ordinarias, seis veces el anulador es dieciséis menos tres p menos tres q menos seis r. Para 00:02:44.498 --> 00:02:50.658 emparejamientos enteros vale uno módulo tres y no puede anularse. Lean demuestra esa aritmética para todos 00:02:50.658 --> 00:02:56.853 los enteros. Este resultado no resuelve los fondos admisibles del orbifold ni las respuestas adicionales de 00:02:56.853 --> 00:02:58.792 esquina. 00:02:59.542 --> 00:03:05.707 El ejemplo U dos muestra por qué la integralidad conjunta difiere de exigirla a cada factor separado. Con b 00:03:05.707 --> 00:03:12.387 cero igual a uno y b uno igual a seis, la forma cuadrática es m al cuadrado más m n más n al cuadrado. Es 00:03:12.387 --> 00:03:18.332 integral para toda pareja de enteros. El criterio formal también cubre coeficientes racionales con un 00:03:18.332 --> 00:03:25.417 denominador común no nulo. Este ejemplo no es un espectro de supergravedad libre de anomalías. 00:03:26.167 --> 00:03:33.642 Cambia b uno de seis a cinco. Cada celda es un cocarácter etiquetado por enteros m y n. Su fracción impresa 00:03:33.642 --> 00:03:40.717 y color son Q módulo uno, calculado con aritmética entera exacta. El punto uno, cero tiene ahora período 00:03:40.717 --> 00:03:48.732 siete octavos: un testigo concreto del fallo. Al volver a seis, todas las celdas son integrales. Las ochenta 00:03:48.732 --> 00:03:55.042 y una celdas ilustran el criterio; el teorema Lean lo establece para toda pareja entera. 00:03:55.792 --> 00:04:01.842 En la auditoría de Spin veinte, el elemento Clifford de grado dieciocho tiene cuadrado menos uno. 00:04:01.842 --> 00:04:08.052 Multiplicarlo por menos i hace que la matriz de representación tenga cuadrado más uno. La distinción importa 00:04:08.052 --> 00:04:14.657 para un levantamiento ordinario de isotropía. No demuestra inconsistencia del modelo: puede ser posible una 00:04:14.657 --> 00:04:21.787 acción torcida o combinada. Cada campo e interacción, incluido Omega bosónico, debe compartir una acción 00:04:21.787 --> 00:04:24.125 especificada. 00:04:24.875 --> 00:04:31.195 El catálogo contiene cuatro archivos Lean con cuarenta y nueve declaraciones de teoremas, scripts exactos, 00:04:31.195 --> 00:04:38.450 comprobaciones registradas y hashes. Los cuatro archivos se verifican con Lean cuatro punto veintisiete. El 00:04:38.450 --> 00:04:45.385 archivo antiguo de S U siete se adaptó de List bind a List flat Map, conservando sus enunciados. Descarga la 00:04:45.385 --> 00:04:52.265 evidencia, comprueba su integridad y ejecuta los comandos indicados. La cancelación completa de anomalías y 00:04:52.265 --> 00:04:55.833 la novedad científica siguen abiertas.