Collatz 24h run: ledger, Lean stack, novelty diff, ROFL test-drive verdict - #2
Open
Disentinel wants to merge 95 commits into
Open
Collatz 24h run: ledger, Lean stack, novelty diff, ROFL test-drive verdict#2Disentinel wants to merge 95 commits into
Disentinel wants to merge 95 commits into
Conversation
Seed sources sha-verified against the Enox handoff package (audit-v0.2.rofl, collatz-models.rofl, PROTOCOL.md verbatim + declared run-local adaptations). Warm-up chain executed per protocol: - R1: open_risk(slow_set_signals_divergence) abandoned (assert-only) — the engine's own computation had refuted its ground - R2: level(depth_30_level) declared; the R10 silently-missed derivation miscast(slow, slowness) now fires - R3: reattach decision + audit extension (readdressed/open_miscast); ledger clean: open_risk/vocab_drift/groundless/open_miscast all empty Engine (owner-authorized, tested): api.load defer option — batch loads evaluate once at the end; rebuild flat ~3.4s instead of O(files x eval). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…st flaw caught R4: Track A pipeline (run/terras.rofl scratch program + independent TS oracle in driver). Five rows agree exactly (3,4,8,13,19 undecided; densities monotone non-increasing). Memory anchor to classical counts kept as hypothesis-ground: shaky stands deliberately, oeis.org egress-blocked, no fabricated citation. R5: round 4's unrelated attach decision instantly fired miscast(terras, slowness) - v0.2's miscast rule cross-joins any leveled decision with any split ledger (no subject linkage). Claim asserted with computed ground; assert-only repair: concerns/2 + miscast3/readdressed3/open_miscast3; live audit moved to open_miscast3 (empty). The substrate audited its own audit theory. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
R6: rows k=9..12 (38/64/128/226) engine==oracle; CPU profile of k=12 found O(n) sorted-insert splices, per-read array copies, subst-map clones. Engine #2: store index -> append + merge-on-read FactRec buckets with tombstoned removals; O(1) amortized insert, same canonical order; 29/29 tests green; k=12 scratch 10.1s -> 5.8s. R7: k=13 (367), k=14 (734, 590k facts, 70.9s). Memory wall projected at k~16 from provenance doubling - to be measured, not dodged; rows beyond the wall would be oracle-only and marked as such (SUBSTRATE_ISSUES #5). Density pair-doubling across adjacent k noted as computed observation. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
R8: engine==oracle at k=15 (1295) and k=16 (2114, 32min, 2.62M facts); in-substrate ceiling k=16 measured and asserted with the timing curve as ground. R9: k=17..20 (4228/7495/14990/27328) via TS oracle alone, kept in a separate terras_oracle_only/2 relation with oracle_only grounds. Process catch logged: numbers were drafted from memory before the oracle ran - caught pre-commit, oracle run first, order violation recorded in RUN_LOG. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
R10: source registry for the literature layer, every src honestly marked from_memory (egress blocked); all obstacles and partial_results linked; unsourced_obstacle / unsourced_partial audits empty; memory_only_source kept as the standing caveat. R11: why hard_core(no_divergence) captured as run/hard_core_proof.md - in-substrate shallow proof over the sourced obligation graph (uncovered + no partials), explicitly not new mathematics. 2h degradation check: clean, with a watch item - predicate births hit 15 per 10 rounds (threshold is >15); vocabulary growth to slow down. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
R12: gen 199->999 + value window 10^6 (seed's 20k guard would silently
truncate - 703 peaks at 250,504), zero new predicates. slowres stays
within {7,11,15} mod 16 at 5x range; 33 slow residues.
R13: still_slow(703) at horizon 120 while reach1(703) holds - the R1
repair's reason broke though its conclusion stands; superseding repair
with range-independent reason, horizon 120->260, transient(703) restored.
Coverage-honest evidence atom for the widened batch.
Engine #3: sha-keyed snapshot cache in driver + trusted fromSnapshot;
92s rebuild pays once, queries 0.6s. 29/29 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…999)
und32={7,15,27,31} dual-computed (k=5 scratch engine == oracle lists);
in-substrate inclusion test slow_outside_und32 EMPTY, and slowres32 fills
the undecided set exactly - the seed's mod-16 observation refines to
precisely the Terras classes. Claimed as a range-999 equality, no theorem.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
R16: inclusion persists at both moduli (slow_outside_m empty) but exact fill breaks at mod 64 - branch 15 mod 64 undecided yet slow-empty, child 79 mod 128 likewise; R15's mod-32 equality was granularity-specific. DEGRADATION CHECK FIRED: 16 predicate births in R7..R16 (> 15). Stop-and- audit performed: ledger fully clean, births = protocol-mandated sourcing layer + terminal parametric measurement vocabulary. Disposition recorded in RUN_LOG: continue under a vocabulary freeze until R27+; any groundless or freeze break halts the run with no second exemption. R17: R16 recorded as claims, zero new predicates (freeze honored). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…estored Probe (scratch, 808k facts, 4.03h in-substrate): engine == oracle on the full 285-member slow set; inclusion persists at mod 32/64/128; exact fill RESTORED at all three moduli (the 15-mod-64 gap at n<=999 was a range artifact - R17's range-scoped hedge needs no repair, scope discipline paid); still_slow empty at horizon 260. Container-restart wall-clock gap (21:40-00:17Z) recorded honestly; probe relaunched from committed state. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
und256 dual-computed (19 residues, engine==oracle); host-side join with the R18-verified slow set: inclusion and exact fill extend to mod 256 at range 9999. Ground names the hybrid method explicitly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…classes, all n Owner redirect: attempt the mathematics with the ledger as harness. Lemma 1 upgrades the run's empirical inclusion to an unconditional statement for k<=8: class-affine induction + exact thresholds (M_5..7=4, M_8=24), finite part machine-checked twice (TS integers; in-substrate over terras.rofl facts). The dual-check caught an inequality-encoding mismatch (theta<=M vs theta<M+1) at class 11 mod 32 in one round - the harness working as asked. Proof and both checkers committed under run/math/. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Lemma 3: u_k = dominated parity strings (bijection proof). Lemma 2:
u_{k+1} = 2u_k - w_k with float-free doubling criterion (no 3-power in
(2^k, 2^{k+1})) - R7's empirical pair-doubling is now a theorem.
Four independent verification paths, newly including Lean 4.21.0
(owner request): CollatzLedgerCheck.lean compiles exit 0 - core
inequalities kernel-checked proofs, finite parts (DP==classification
k=4..20, recurrence, doubling criterion, Lemma 1 thresholds, affine
invariant) via native_decide. Caveats documented in lemma2_3.md.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
First non-memory sources (WebSearch 2026-08-20): Barina 2025 (2^71), Hercher 2023 (no m-cycles m<=91), Tao 2019 (almost-all, log density), Krasikov-Lagarias (x^0.84), ccchallenge.org. Six memory anchors upgraded to verified; five stay flagged. THE REVISION EVENT: fetched partials for no_divergence refuted the ground of hard_core_is_no_divergence - the graph self-corrected (hard_core stopped deriving), audit chain fired in full (refuted -> at_risk -> repair by supersession). Refined sourced claim survives: the hard core is "no known route from density to totality". FRONTIER.md maps proved territory vs literature vs the gap. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…ed cores) Proved: half-threshold (dominated strings are majority-odd: 2s<=k => 3^s < 2^k via elementary 3^k < 4^k), eta monotone, u_k bounded by the binomial end-tail beyond k/2 (Lean finite check k<=20, Pascal choose). Observed rate vs LD heuristic recorded as a deliberately-shaky claim (hypothesis ground, no evidence) - the ballot-constraint gap stays flagged unproven. Terras attribution honesty preserved. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Determinism probe: rebuild-from-sources vs untrusted snapshot restore in separate OS processes -> identical canonicalState sha256 (d2e7ceee..., 70,822 facts). SATURATION.md: predicate-birth curve over 24 rounds with the n=1 caveat stated up front - three nameable vocabulary bursts, then 8+ rounds flat under the freeze while atom vocabulary grew linearly; the predicate/atom split is where saturation discipline bites. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…e to k=40
R24: cross-process determinism - sources-rebuild vs untrusted snapshot
restore give identical canonicalState sha256 at 70,822 facts; SATURATION.md
delivered with the n=1 caveat. R25: u_{k+1} <= 2u_k proved for ALL k in
Lean (Lemma5Check.lean, kernel-checked; sum machinery from scratch on core
lists). R26: undecided-count table extended to k=40 via two independent
BigInt implementations (exact agreement); Lemma 2's doubling criterion
holds at every step k=1..39. Continuous-work mode per owner.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
The missing direction - a 3-power in (2^k, 2^{k+1}) forces w_k > 0 - is
now a general kernel-checked theorem via the greedy minimal dominated
string (Lemma6Check.lean: gs_dominated, gs_minimal, dpf_gs_pos,
wf_pos_of_gap). Together with one_ext_survives and gap_unique the
doubling criterion is an iff proved in both directions for all k.
Round-23 honesty limitation repaired by supersession in lemma2_3.md.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
R28: every proof ground linked to its checker file via source_of; math artifacts registered as repo_committed sources; run/math/README.md indexes them with re-run commands. Freeze window ends, held unbroken (0 births/11 rounds). R29: horizon.js computes the exact first-drop horizon — 96/132/132/220 for N=199/999/9999/99999 — explaining the run's R13/R18 horizon-chase episodes by computation and validating the 10^8 overflow window. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…kernel) Lemma7Check.lean: all-integer Chernoff at lambda=2 — counts below binomials, weighted binomial theorem, 63/100 threshold from 3^63 < 2^100, chernoff bound u_k * 2^(63k/100+1) <= 3^k, and density_decay: c*u_k <= 2^k for k >= c^100. No native_decide in the load-bearing chain (axioms: propext, choice, quot). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…erion, general Lemma8Check.lean: T defined; kernel-proved for all j,n: 2^j T^j(n) = 3^A n + D, coefficient periodicity mod 2^j, D < 3^j, and the drop criterion (decided class + n >= 3^j => T^j(n) < n). Finite bridge: undecided classes of the real map = string-DP uf (k <= 14). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…orem TerrasAlmostAll.lean (self-contained, 949 lines): general counting theorem NN_eq_dpf / NU_eq_uf (undecided residues of the real map = string DP, all k; two-lifts pairing via the affine lemma) + assembled terras_almost_all: c * NU k <= 2^k and every n >= 3^k in a decided class drops within k steps. Axioms: propext, Classical.choice, Quot.sound. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…ntegers ndrop indicator + periodic-sum machinery; kernel theorem: c * ND(q*2^k, k) <= q*2^k + c*3^k for k >= max(1, c^100) — among the first q*2^k integers, k-step non-droppers have density at most 1/c + o(1). Axioms: propext, choice, quot. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Catch: terras_table.md still called the pair-doubling mechanism an unproved observation after R27 kernel-proved the iff for all k. Docs brought current with the R30-33 kernel state; FRONTIER marks the result as base camp, density-to-totality untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
thm/thm_dep/thm_reach (3 declared births): the Lean development's dependency spine as facts + transitive-closure rule; engine derives the 28-theorem support cone of terras_integers, why walks the chains; the only numeric leaves are 3^63 < 2^100 and 22*3^100 <= 2^163. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…e mode Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
density_decay_log + eta_exponential in TerrasAlmostAll.lean: logarithmic accuracy threshold replacing the c^100 form; explicit per-k exponential bound u_k * 2^(k/25) <= 2^k. Same axioms. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
… form C defined; T^i = C^j correspondence (i <= j <= 2i); non-dropper inclusion; sharp-threshold integer bounds for both maps. Almost every n drops below itself under the literal Collatz iteration — kernel-checked. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…ssue #6 Engine derives the terras_integers cone's 14 leaves (12 inductions + 2 numeric facts); Lean corollary: never-dropping n is undecided at every depth <= log3 n; prose-outside-audit-net lesson recorded as issue #6. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…llary Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…kernel-checked Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…scent Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…assembly Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
… x5.4-x8.4 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…corded Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…ss of every odd modulus Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…27 to depth 58 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…n-field corrections Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
… realized in the core Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…block, determinism probe #3 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…s dilution by proved laws Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…71 floor supports Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…uctions unified as one-place blindness Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
… cycle_not_in_core proved Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
… exact; 2r+1 correlation opens Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…-class prediction Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
… honest note Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…theorems integrated Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
….538 -> 3/4 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…WALKTHROUGH refresh Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
…r corpus Verdicts: classical layer rediscovery (mechanization is the artifact); cycles known-stronger; coupling transducer probable rediscovery of the CCV 2004 shift commutator (ledgered shaky); not found in corpus: superadditivity lower bound, covering obstruction, exact 3-adic flow laws, constructive core points. Two corrections ledgered: ffi-ligature grep artifact on 'coefficient stopping' (the term is Terras's own), and Tao does prove superpolynomial mod-3^n fine-scale mixing. FINAL.md gains a post-window addendum with the calibrated novelty verdict. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
The substrate report as a user deliverable: usage envelope, 15 caught distortions in 5 classes, determinism record, saturation lesson (schema saturates, knowledge doesn't), honest division of labor, and feature requests ranked by real friction. Verdict: the substrate multiplied honesty, not intelligence. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Что это
24-часовой (плюс санкционированное продолжение) прогон автономного sustained reasoning на гипотезе Коллатца с ROFL как эпистемическим субстратом: 98 раундов ledger-протокола (audit → act → record → snapshot → commit), Lean 4 как слой верификации, честная дисциплина «ни одного числа, которое не прочитано».
Граница, сразу: гипотеза Коллатца этим прогоном не решена и остаётся открытой. Что сделано — ниже.
Итоговые документы
run/TESTDRIVE.mdrun/FINAL.mdrun/NOVELTY_DIFF.mdrun/math/TerrasAlmostAll.leanWALKTHROUGH.md— карта для математикаrun/RUN_LOG.mdМатематический результат (kernel-checked)
NU_superadd, у метода нет потолка ниже энтропии h ≈ 0.95).collatz_iff_descent; общая covering-обструкцияcore_meets_every_class(никакая накрывающая система ни по какому нечётному модулю не сертифицирует спуск); точный закон роста ядраcount_law; две явные вычислимые 2-адические точки ядра (alphaT,stairT— слово Штурма для log₂3).run/math/check_all.shпереверифицирует весь стек.Вердикт по новизне (честный)
Границу известного в сильном смысле не расширили: классический слой — переоткрытие (ценность — механизация), циклы слабее известного, coupling-транздьюсер — вероятное переоткрытие shift-коммутатора CCV 2004 (заледжерено shaky). Кандидаты на новое, не найденные в корпусе ни в каком виде: супераддитивная нижняя оценка u_k, covering-обструкция, точные 3-адические законы потока, конструктивные точки ядра. До публичного клейма нужен проход по MathSciNet/zbMATH.
Вердикт по субстрату
Субстрат умножил не интеллект, а честность на дистанции: ноль groundless-клеймов на каждой границе раунда, 4 sha-идентичные пробы детерминизма (rebuild vs snapshot-restore в раздельных процессах, 70k→73.7k фактов), сатурация схемы при линейном росте знания. Математику сделали Lean и оракулы; граф сделал так, что итоговым документам можно верить по команде, а не по доверию. Запросы на фичи из реального трения — в TESTDRIVE.md, топ: doc_note/stale_note (единственная найденная дыра honesty-контура), builtin-folding для
why, компактный тир провенанса, bignum.Состояние ledger на merge
73,783 факта; аудит: open_risk/vocab_drift/groundless/open_miscast3/holes — все пусто; 4 стоячих shaky-флага (включая намеренный CCV до прочтения полной статьи); снапшот sha 18f76f7a…, воспроизводим из исходников.
🤖 Generated with Claude Code
https://claude.ai/code/session_01FrZEaNpkncqQXRjhd2tLuj
Generated by Claude Code