# Recursive Asterisms — research journey Content draft, pending visual direction and owner review. Historical B identifiers remain unchanged. Source: research exchange and Lean programme listed in evidence-manifest.json. B026–B039 are written arguments and finite computational evidence, not new Lean proofs. Earlier entries are programme summaries, not fresh website-task replays. ## B001 — Freeze the evidence Hash-check 52 original sources; begin a verification-first programme. This is inventory and execution authority, not proof acceptance. ## B002 — Reuse established dependencies Reproduce 30 original declarations; establish the specified H/A/B selector’s correctness and factor-nine guarantee. The 615 ledger rows are claim/disposition entries, not 615 discoveries. ## B003 — Protect the user’s question Establish concrete blocked-clause deletion, identity-or-pivot repair, reverse trace reconstruction and equality of protected projected models. Full model counts can change. ## B004 — Construct a checked trace Verify a deterministic deletion producer. A correct producer is not yet a full runtime theorem or a SAT decision procedure. ## B005 — Account for the checker Refine explicit list checking and protected-input costs under the declared mathematical charge model. ## B006 — Connect producer and lists Relate list-state execution to the producer and establish cumulative declared costs; separate those charges from machine time. ## B007 — Replay and restore Check each supplied deletion against the current formula and reconstruct a supplied residual witness in reverse order. ## B008 — Make input explicit Verify external data validation and binary framing, including malformed-input behavior. ## B009 — Charge the primitives Establish encoded-size accounting and concrete binary primitive costs within their specified model. ## B010 — Parse complete records Verify the structural-fuel record parser; parsing a whole record has obligations beyond recognizing its fields. ## B011 — Validate actual bit values Verify identifier ranges and normalization on bit-valued data rather than assuming ideal typed inputs. ## B012 — Refine the deletion checker Connect a charged bit-valued single-deletion checker to its established semantics. ## B013 — Build with a fixed pool Verify the bit-valued fixed-pool producer; preserve the distinction between construction and a supplied certificate. ## B014 — Check arbitrary supplied traces Establish exact success/rejection correspondence, current-state checking and protected projection preservation. An empty trace is identity, not validation. ## B015 — Restore bit-valued witnesses Verify numerical first-match lookup, sparse stores, reverse repair and final original-model checking. This verifies a supplied witness; it does not find one. ## B016 — Compose encoded inputs Separate verification of a supplied trace/witness from independent preprocessing; each decodes and validates the entire input once. ## B017 — Serialize without hiding work Verify canonical numerical output, retained order and shadowed bindings; charge discarded padding. An earlier proposed cost coefficient was corrected. ## B018 — Execute an actual append Verify a specified TM2 append routine: first halt after 2n+2 label transitions with preloaded inputs; the first input is consumed. Not CPU time. ## B019 — Preserve borrowed inputs Verify a separate append convention restoring both inputs: 2n+2m+4 label transitions. Counterexamples prevent reusing the old charge without its preconditions. ## B020 — Execute a list writer Verify the selected fused Boolean-list writer, input restoration and frame preservation; exact live-continuation count p+q+2n+4. ## B021 — Compose two writer calls Verify a pair writer retaining the right output before prepending the left. Exact first halt: p+q+2n+2m+10 label transitions in this machine. ## B022 — Prove non-observation Establish suffix commutation under a no-output-read condition and closed-label support. Peek, pop and reset refute weaker versions; this does not prove termination. ## B023 — Answer from the formula alone Verify the M0 wrapper’s definitive answers on guarded encoded CNF. Other admitted formulas can return UNKNOWN; malformed input is REJECTED. ## B024 — Test the environment analogy Distinguish solution-set preservation from energy-sampling behavior. Physical/environmental exploration remains written and finite evidence; return to global portfolio coverage. ## B025 — Add a complete restricted component Verify the Horn core and guarded original-formula bridge. Opposing units and an implication cycle are resolved; a valid non-Horn example still returns UNKNOWN. ## B026 — Learn from relative feedback On 5,435 selected cases: 4,220 checked SAT witnesses, 614 empty-clause UNSAT answers and 601 UNKNOWN cycles. Relative weighting rescues 154 selected SAT cases; no universal claim. ## B027 — Ask what a cycle proves Among 601 cycle inputs, recurrent supports are UNSAT in 455 and SAT in 146. A cycle is not an UNSAT certificate; sound fallback remains necessary. ## B028 — Inspect the alternatives Map all 48 states of a fixed unit-weight/recency core. Evaluated successor clauses resolve 129 of the 146 support gaps; 17 remain. Discovery overhead prevents a total-speedup claim. ## B029 — Refine using a failed witness Add the first original clause falsified by a subset witness. Twenty-two additions close the 17 remaining support cases; seeded and empty-seed costs are mixed. ## B030 — Recover one witness Replace unnecessary all-witness enumeration with one-witness reconstruction. The preserved refinement contract is the benefit; the backend may still take exponential work. ## B031 — Compare fixed compositions Four routes agree on 86 frozen formulas: 74 SAT, 12 UNSAT. Restricted signed reduction helps selected cases; a conditional polynomial argument still needs bounded construction and width. ## B032 — Admit only affordable tables Check order estimates before allocating inference tables. A 106-case expansion gives 88 SAT, 16 UNSAT and two UNKNOWN with cheap witnesses plus the guard. ## B033 — Preprocess with reconstruction Unit and pure-literal steps close the two prior failures. Expanded bank: 109 SAT, 27 UNSAT, one UNKNOWN. Preserve the precise existence/lift contract. ## B034 — Expose a small contradiction Guarded original-clause refinement decides all 137 predecessor formulas. Expanded bank: 124 SAT, 29 UNSAT, five UNKNOWN; clause choice is now the boundary. ## B035 — Choose local clauses Fewest-new-variable selection repairs the five failures. All 182 frozen cases are decided; five of six separate pigeonhole diagnostics still remain UNKNOWN. ## B036 — Certify capacity failure Checked capacity evidence refutes those five diagnostics. Expanded bank: 132 SAT, 75 UNSAT, five UNKNOWN; constructive allocation is the next gap. ## B037 — Construct allocations Matching produces witnesses checked against original clauses. The 240-case combined bank is fully decided: 157 SAT, 83 UNSAT. Matching alone is not a universal solver. ## B038 — Condition on the residual Checked demand/capacity decomposition and bounded residual queries reduce fallback from 165 to 137 calls on 278 fixed cases. Overall coverage is unchanged; standalone gains and losses both matter. ## B039 — Preserve future questions Checked elimination reduces three chain residuals from 49/121/241 clauses to one each, reconstructing original SAT witnesses. Fallback falls 137→134; overall 183 SAT/95 UNSAT coverage is unchanged and one measured run is slower. ## B039 scope and retained failures Three chain residuals 49 / 121 / 241 became one each after 18 / 40 / 70 elimination steps. Original SAT witnesses were reconstructed and validated. Future pins on eliminated coordinates are refused. Fixed caps remain two residual clauses and 256 tuples. Both full compositions decided the same 278 cases: 183 SAT and 95 UNSAT. Standalone conditional repair gained 27 answers, but B037 already handled 24; only three additional fallback calls were avoided (137 to 134). One accepted-run timing was 5.966 seconds old versus 6.612 seconds new. This is a slower measured run, not a calibrated performance comparison or speedup. Accepted run003 reportedly passed 30 controls, 20,412 one-step semantic presentations, 128 signed/sparse two-step traces and 3,954 small formulas. Runs 001 and 002 failed in the auditor: JSON key comparison and attempted lifting of core-only models. The research record retains failed sources and logs; eliminate.py was unchanged. The website task inspected the reporting, not the complete experiment or an independent replay. No general polynomial SAT theorem, new Lean acceptance or independent external verification follows.