felix.git/source/Checking/Kernel, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2026-08-06T15:54:00+00:00 Migrate to `Felix` namespace 2026-08-06T15:54:00+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-06T15:54:00+00:00 urn:sha1:82328890108bae64b372b8d58620ebc62699de76 Restore checked set-induction composition 2026-08-05T14:27:44+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-05T14:27:44+00:00 urn:sha1:6353960e8449527314c51546d05414d5218a1c70 Confine contradictory status to falsum targets 2026-08-05T13:24:49+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-05T13:24:49+00:00 urn:sha1:2785025113e8092dc8773e294326005a581a2ca6 Restore exact cases and contradiction 2026-08-05T12:58:32+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-05T12:58:32+00:00 urn:sha1:db5e4920b8b1f0fbc08bf78708ee3076ea895b75 Prepare exact inductive declarations 2026-08-02T00:33:14+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-02T00:33:14+00:00 urn:sha1:d55d2416bc4f6a9aa055a17deae4fba0fe906316 Fall back after reconstruction exhaustion 2026-07-28T19:05:10+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T18:32:53+00:00 urn:sha1:5499f17e80fd55ca3b38364dfde5434f59d90dd7 Remove obsolete kernel authorization projection 2026-07-28T19:05:10+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T18:18:16+00:00 urn:sha1:a03cd6977c4eecbb590f4c9df01bbe0569c37a42 Prepare direct inductive kernel proofs 2026-07-28T12:51:24+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T12:47:19+00:00 urn:sha1:331d86e4a00bae144b6539edeb1deb9af78c5c7e Define bounded fixed-point kernel rules 2026-07-28T11:04:12+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T11:04:12+00:00 urn:sha1:63503003ca8022ad9890396866f52bf56bcb252d Replay scoped HOL derivations independently 2026-07-28T10:25:32+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T10:25:32+00:00 urn:sha1:ed12d0e4bcafd87e73219915ff8a3ae563c4a4cb Replay rechecks stored terms against the current global signature and bounds nodes, lexical depth, and conversion. Import-bearing trees remain replay-only until exact transition-inventory authorization alignment lands.