Точные часы

На сегодняшний день сверхточные часы представляют из себя прожорливые по части электропитания установки размером со шкаф, требующие постоянного охлаждения и всяческой изоляци от окружающих воздействий: сильных электрических и магнитных полей, ионизирующего излучения, вибрации. Есть миниатюрные варианты, влезающие в наручные часы, но там точность сильно страдает.

В ближайшем будущем часовой механизм, влезающий в наручные часы и работающий от батарейки, будет не только значительно привышать по точности современные сверхточные часы, но и работать в широком диапазоне температур, не бояться электромагнитных полей и тем более механических воздействий.
— Основа механизма (“маятник”) — полупроводниковый лазер (типа тех, что в лазерных указках) со встроенным в него кристаллом фиксации частоты, содержащий торий-229. Кристалл (про механизм для простоты умолчим) заботится о том, что длина волны лазера составляет ровно* 159 нанометров, что соответствует частоте в 1886 THz.
— Дальше лазер направляется в устройство (метакристалл), которое называется частотной расчёской. Луч монохроматического света частоты F прошедший через этот кристалл, начинает варьировать яркость (становиться то ярче, то тусклее) с частотой ровно F/2ⁿ, где n — порядок кристалла. В наших часах будет использоваться кристалл порядка 14, т.е. на выходе будет луч с биением яркости с очень стабильной частотой в районе 115 GHz.
— Затем луч будет подаваться на фотоэлемент со счётчиком, который считает биения яркости. Т.е. он считает, сколько прошло тактов времени длинной 0.9 пикосекунд с момента запуска.
Всё устройство целиком будет плоским, компактным, твердотельным, смонтированным на одном кристалле, замкнутым и запаяным.

* Обычно для стабилизации частоты в сверхточных часах используются электронные переходы в атомах. Это имеет ряд минусов: во-первых при повышении температуры частота расплывается, во-вторых при появлении сильных фоновых электрических или магнитных полей, частота сдвигается. Для стабилизации частоты в вышеуказанных твердотельных ториевых часах используется переход в ядре тория, что имеет ряд плюсов. Во-первых, высокая температура выражается в основном в колебаниях электронных оболочек атомов, но не ядра, таким образом точность часов останется высочайшей при температурах до 300 °C, тогда как атомные часы требуют температур близких к абсолютному нулю. Во-вторых, фоновые электромагнитные поля ядрам тоже непочём и ионизирующее излучение побоку. Ну и наконец, в отличие от случая атомных часов, нам не нужно ловить отдельные атомы в сложную ионную ловушку, можно просто взять крисстал допированный торием, кристалл уже и есть ловушка для ядер. Частота этого перехода (коротковолновый ультрафиолет) много выше частоты применяющихся для атомных часов электронных переходов, а его квантовая размытость много меньше.

В результате такие часы имеют неточность порядка 1/10¹⁹. То есть если положить на стол набор таких часов на стол, одновременно запустить и подождать 14 миллиардов лет (возраст вселенной), то разночтения показаний часов будут в пределах одной десятой секунды**.

С появлением таких часов изменят определение секунды: сейчас секунда определена как 9192631770 биений цезиевого "маятника", а будет определена как определённое количество “биений” ториевых часов.

(Частично по материалам http://arxiv.org/pdf/1204.3268v3.pdf)

_____
** 0.1 с при охлаждении до температуры кипения азота и ниже, в высокотемпературном (от комнатной температуры до 300 °C) режиме работы — до 1 секунды.

Идеи

[У меня уже давно была мысль, что постулаты трансфинитной индукции в каком-то смысле эквивалентны постулатам о достаточном количестве выч.ресурсов (памяти и времени выполнения) для проведения аналитической верификации доказательства (т.е. по сути cut elimination) в системе с этой самой индукцией. В предельном случае, в системе вообще без индукции (даже конечной индукции) аналитическая проверка доказательства может быть произведена без использования дополнительной памяти и за столько шагов, сколько шагов в доказательстве. Для таких систем не работает «Вторая теорема о неполноте»: зачастую силами самой системы можно доказать её непротиворечивость. Для систем более мощных возможность аналитической проверки доказательства уже является чистой (нефизичной) абстракцией, ведь можно всегда можно найти такое доказательство p, что само p еще влезает в память, а для аналитической проверки потребуется больше памяти чем существует во вселенной.

Эта нефизичность — красивое философское объяснение «Второй теоремы о неполноте» и исключений из неё: “Если проверка доказательств может быть произведена inplace — можно доказать непротиворечивость изнутри системы, а для остальных систем мы не можем доказать непротиворечивость таких систем в смысле естественой дедукции потому что при достаточно длинном доказательстве мы не можем быть уверены в достаточности во вселенной выч.ресурсов для его проверки. При этом можем доказать её из более сильных систем, потому что там посылка о достаточном для этого количестве выч.ресурсов в аксиомы заложена. А вообще, пока доказательства обозримого размера, можно не заморачиваться”. Вот только что такое “обозримый размер”? Есть ли какая-нибудь система оценки, влезет ли “аналитическая расшифровка” доказательства в атомы наблюдаемой вселенной и сколько (тысяч) лет займёт довести до конца cut elimination? Вот об этом я тут и размышлял.]

Будем называть систему взаимодействия (Σ, ℛ) завершимой, если существует такой фундированный порядок ≺ на конфигурациях системы, такой, что всякая редукция уменьшает конфигурацию в смысле (≺). Для завершимых систем будем называть порядком системы минимальный ординал α, изоморфный какому-либо порядку с вышеописанным свойством. В таком случае трансфинитная индукция порядка α необходима и достаточна для того чтобы доказать, что все стартовые конфигурации редуцируются до нормальной формы.

Гипотеза 1: Существует такое семейство функций G_α(n: Nat): Nat, индексируемое рекурсивными ординалами, что:

1) Функция G_α(n) вычислима при помощи системы взаимодействия порядка α.
2) Всякая конфигурация С (системы взаимодействия порядка α) с n связями может быть сведена к нормальной форме цепью не более чем G_α(n) редукций с использованием промежуточных конфигураций с не более чем G_α(n) связями.

Прим: число G_α(n) очевидно является оптимальной оценкой типа (2) в плане памяти, т.к. вычисление самой G_α(n) использует G_α(n) памяти: если стартовать с числа n (выражается цепью с n связями), в конце получится цепь из G_α(n) связей.

Гипотеза 2: Семейство G_α(n) задаётся для ординалов меньше ε₀ через
G_ω^k(n) = n [k] 1,
G_{a + b}(n) = G_b(G_b(n)),
где
n [0] m = n + m
n [k] m = (x ↦ x [k-1] x)^m n.

В частности G_{ω^k∙m + c}(n) = n [k + 1] m + c:
G₀(n) = n
G₁(n) = n + 1
G_ω(n) = 2n
G_{ω∙2 + 1}(n) = 3n + 1
G_ω²(n) = n²
G_{ω²∙2 + ω∙3 + 5}(n) = 4n³ + 5
G_ω³∙2(n) = nⁿⁿ
и т.д.

Вероятно, используя технику Chris'а Bird'а можно в явном виде указать такие функции вплоть до ординала Бахмана-Говарда.


Предельные цели программы:
— Доказать финитарными методами возможность замены аксиомы трансфинитной индукции порядка α аксиомой вида (∀ n: Nat) ENOUGH_SPACETIME^α(n), где ENOUGH_SPACETIME^α(n) определяется как (∃ N: Nat) N = G_α(n).
— Разработать самоверифицирующуюся логическую систему, в которой тем не менее возможны рассуждения о растущих функциях f(n) в предположении ENOUGH_SPACETIME^α(|n|), где α ординал вычислительной сложности f, а |n| количество связей в граф-представлении аргумента n.