Scoped replays annotate existing claims; prize and theorem statuses are unchanged.
- refutation: Exact replay refutes the proposed F_endpoint^3(22122v)=F_endpoint^3(22222v); the host catalog record states the valid correction and is NOT refuted.
Historical receipt — revalidation required. Changed or missing: rule30_orchestrator/engine.py; rule30_orchestrator/obligations.json; rule30_orchestrator/worker.py; witness_bank.jsonl
Claim r30-rw-defect-exact-correction; evidence replay-f12ca37601da7d64a176Remaining: RW separator; period-two exclusion; higher periods
- finite_check: All four-state suffixes of length <= 3 only; no all-length proof
Historical receipt — revalidation required. Changed or missing: rule30_orchestrator/engine.py; rule30_orchestrator/obligations.json; rule30_orchestrator/worker.py; witness_bank.jsonl
Claim r30-rw-run-erasure-padding; evidence replay-7dde47ac1b50522bb1afRemaining: No parent prize obligation discharged
- external_certificate: Uniform mortality for this displayed endpoint family with its supplied initial-history label; no unrestricted mortality or period-two conclusion
Historical receipt — revalidation required. Changed or missing: rule30_orchestrator/engine.py; rule30_orchestrator/obligations.json; rule30_orchestrator/worker.py
Claim r30-cap18-joint-three-closed; evidence replay-d4a12c5dc36018ed0933Remaining: capacity-language initial-history correspondence; unrestricted mortality; mortality_to_period_two; higher periods
- incomplete: Exact joint family closure only. Initial tape is supplied from the capacity-language classification; the scanner checks every further guard. A cap is incomplete, and survivor counts count joint states, not parameter pairs or original ancestors.
Historical receipt — revalidation required. Changed or missing: rule30_orchestrator/engine.py; rule30_orchestrator/obligations.json; rule30_orchestrator/worker.py
Claim r30-cap18-joint-four-open; evidence replay-7f69b3f042b622ad5160Remaining: No parent prize obligation discharged
- external_certificate: Independent exact local proof components plus finite directed controls; no broad frontier census, RW separator, mortality, or period-two theorem.
Historical receipt — revalidation required. Changed or missing: rule30_orchestrator/engine.py; rule30_orchestrator/obligations.json; rule30_orchestrator/worker.py
Claim r30-rw-run-erasure-padding; evidence replay-1a0df3727ce41a01f972Remaining: all-k induction source-reviewed, unformalized; interrupted-source RW separator; actual ancestry
- lean_reduction: Concrete ordered pair-energy recurrence and Rule 30 singleton specializations; no all-scale decay theorem
Historical receipt — revalidation required. Changed or missing: rule30_orchestrator/engine.py; rule30_orchestrator/obligations.json; rule30_orchestrator/worker.py
Claim b9cafb0e27086145; evidence replay-ce2662ba5716cf9d8ac9Remaining: dyadic shell maximal-discrepancy/energy bridge; singleton-specific flexible-scale decay
- external_certificate: Index15 initial00, all independent a,b>=0: fixed-depth4 spatial quotient128/128 states and fixed-depth8 quotient6784/15104 states, every ordered transport and terminal chronology independently replayed. Eight reachable coarse-summary obstructions retained. No temporal lift or mortality theorem. Claim r30-cap18-joint-four-open; evidence verified-index15-spatial-quotient-depth4-8
Remaining: Prove a temporally liftable quotient preserving ordered seam transport and births; Close a complete empty guard-survivor set at some temporal depth, or establish another sound mortality argument; Formalize the auxiliary-to-period-two bridge; higher periods remain
- external_certificate: Anchored prefixes 2212222 and 2222222: independently checked all-finite-word J-machine action identity with explicit diagonal invariant. Endpoint consequence retains unformalized J bijection/conjugacy; no preservation of 22222-free source language or actual ancestry.
Historical receipt — revalidation required. Changed or missing: witness_bank.jsonl
Claim r30-rw-run-erasure-padding; evidence verified-anchored-section-0Remaining: J is a bijection on every finite endpoint-word length; J(wv)=J(w) M_w(J(v)) and J(F_endpoint(e))=tail(J(e)); source-prefix erasure applicability to full RW guards and actual ancestry remains separate
- external_certificate: Anchored prefixes 221212222222222 and 222222222222222: independently checked all-finite-word J-machine action identity with explicit diagonal invariant. Endpoint consequence retains unformalized J bijection/conjugacy; no preservation of 22222-free source language or actual ancestry.
Historical receipt — revalidation required. Changed or missing: witness_bank.jsonl
Claim r30-rw-run-erasure-padding; evidence verified-anchored-section-9Remaining: J is a bijection on every finite endpoint-word length; J(wv)=J(w) M_w(J(v)) and J(F_endpoint(e))=tail(J(e)); source-prefix erasure applicability to full RW guards and actual ancestry remains separate
- refutation: Actual index15 parameters(26,34),(26,162), initial00, share full depth8 column51747 and tape10010110 but produce depth9 tapes100101101 and100101100. Two independent replays refute prediction by unchanged depth8 summary. Host catalog open-family record is not refuted; augmented temporal lifts remain possible. Claim r30-cap18-joint-four-open; evidence refuted-unchanged-depth8-temporal-lift
Remaining: Find a sufficient augmented temporal summary; All four open capacity18 patterns; Mortality to period2 bridge; Higher periods
- lean_reduction: Lean4.33.1 checked B_two_time_guard and C_two_time_guard for every finite low-first itinerary word and every non-origin site: low(g(xs)[i-1])=0 and low(g(xs)[i])=1 imply high(g(g(xs))[i])=high(xs[i]). Concrete A/B/C permutation-to-bitplane and recursive-list correspondence included. B origin high flip and C origin fixed digit separately checked. Axioms: propext only (permutation_bitplanes has none). This formalizes the single-guard component of the cited record, not its entire chain or infinite singleton correspondence. Claim r30-p3-rise-chain-transparency-pause; evidence lean-bc-single-rise-guard-8027c1f6ff50
Remaining: finite-prefix compatibility with the infinite itinerary ray and its exact singleton center-query correspondence; chronological guard-chain language, actual predecessor ancestry and guard occurrence; construction of actual predecessor words and earlier high endpoints; shrinking total-work recurrence charging construction, memory, indexing and preprocessing under the fixed P3 model