# Recursive Asterisms — selected evidence cards

Content draft for the website exhibit and AI companion. Snapshot: 2 October 2026. Historical source identifiers retain their original names. The public-facing brand is Recursive Asterisms.

## 01 — Factor-nine selector guarantee

**Stable source:** TRS-LEAN-HAB9-001; HAB9.lean; `TRSHAB9.producer_factor9` and `TRSHAB9.encoded_producer_factor9`.

**Displayed equation:** |B| ≤ 9κ(F).

**Plain language.** In a specified Boolean-constraint model, the selector constructs a valid set of variables whose size is at most nine times the smallest valid set. The guarantee concerns how many variables are selected.

**Mathematics.** F is a finite list of explicit Boolean relation tables. Each table has arity at most three and distinct variables within its scope. B is the set returned by the specified producer, and κ(F) is the minimum cardinality of a valid set for this exact model. For every assignment to a valid set, all residual constraints must belong to one common target class: Horn, affine or bijunctive. The class may depend on the assignment. This is a whole-instance condition, not permission to choose a different class independently for each component. In the formalization, these classes are represented by closure under Boolean conjunction, ternary XOR and majority, respectively. Empty and nullary tables are retained; there is no global false-instance shortcut.

**Formal evidence.** `producer_factor9` asserts validity of the selected set together with its cardinality bound; `encoded_producer_factor9` relates the bound to the specified encoded tables. The presentation task's replay records three successful positive runs in HAB9 and one deliberately false control rejected. The website task hash-matched these sources and logs to that receipt; it did not rerun Lean.

**Boundary.** This does not bound total runtime, solve unrestricted SAT, settle P versus NP, establish novelty or certify an entire app. A numerical illustration such as κ(F)=2 → |B|≤18 only illustrates the bound. It is not an executed selector or evidence that the bound is tight on an actual input.

**Source hash:** HAB9.lean — cfe1f8d39620c7e52ae5b0c50e32633eddc0c90ea5a603640d60c604606ce765.

## 02 — Protected projection and reconstruction

**Stable sources:** B003; ProtectedBCE.lean; BCEProjectedCount.lean; BCETraceCheck.lean; BCEScopeCorollaries.lean. Namespace `TRSProtectedBCE`; declarations include `repair_valid`, `repair_protected`, `restore_valid`, `restore_observe` and the one-step and trace `projected_models_iff` results.

**Plain language.** A checked deletion may simplify a Boolean formula while preserving the possible answers on a designated set of protected variables. Given a residual solution, reverse repair reconstructs an original solution without changing those protected answers.

**Mathematics.** The current CNF uses finite literal sets over a fixed finite variable universe. A permitted step requires the current formula to be normalized (non-tautological clauses), the deleted clause to occur in that formula, a blocking literal to occur in the clause, its variable to lie outside the protected set, and the blocked-clause condition to hold. A valid trace checks each step against the current formula. Equality concerns the projections of model sets onto protected variables. An arbitrary predicate depending only on the protected values therefore preserves its satisfiability through the transformation.

**Formal evidence.** The selected ProtectedBCE replay records eight positive runs and three deliberately false controls rejected: unrestricted context, empty-clause deletion and full-model-count preservation. Source and stdout hashes matched the supplied receipt in this website task.

**Boundary.** Full model sets and full model counts may change. Reconstruction of a supplied residual model does not find a model. The theorem is not a complete SAT solver, a universal deletion schedule or a runtime result.

**Source hash:** ProtectedBCE.lean — 744b263f9d85a320df30f004f3f2f2150ae357ebf59cda73ff462c4d142dca09.

## 03 — Horn decision core and guarded CNF bridge

**Stable sources:** B025; HornCore.lean and HornCNFBridge.lean. `TRSProtectedBCE.HornCore.solve_iff`; bridge declarations `run_sat_sound`, `run_unsat_sound`, `run_admitted_horn` and `run_admitted_horn_definitive`.

**Plain language.** The Horn core correctly decides its restricted rule class. A separate guarded bridge ties accepted encoded CNF inputs to statements about the original formula.

**Mathematics.** The core computes synchronous immediate-consequence rounds, with fuel equal to the number of distinct appearing heads, and checks conflict after saturation. `solve_iff` relates success to existence of a rule model. The encoded wrapper requires successful parsing and admission checks, including the specified external-input validity and clause-width-at-most-three guard. On admitted Horn formulas its answer is definitive. Definitive answers are sound for the represented original formula.

**Formal evidence.** The selected HornDecision replay records three positive runs and one false conflict control rejected. Website preparation matched source and stdout hashes to the parent receipt.

**Boundary.** Malformed or inadmissible input is rejected. An admitted non-Horn formula can return UNKNOWN. This is not a claim that all CNF is decided, a bit-machine runtime theorem or a claim that historical in-place Python scans have the same trajectory.

**Source hashes:** HornCore.lean — ea30461ad1bd7de3bc738f716feeeb34a42aa9ee856b3422af522f28980f37d5; HornCNFBridge.lean — 0ab06c2e611bd484e54447605cf7914782ec29a7ad6b43a87f734d1b4da9f6d6.

## 04 — Output-suffix commutation

**Stable sources:** B022; SuffixFrame.lean and PairSuffix.lean; `TRSProtectedBCE.SuffixFrame.run_suffix_commutes`.

**Plain language.** In the specified machine semantics, adding a suffix to a designated output stack can commute with a fixed number of execution steps when those steps cannot inspect or remove that stored output and execution stays inside the declared safe region.

**Mathematics.** The pinned TM2 model requires `SafeMachine` on a closed set of labels and `Supported` for the initial configuration. Safe statements forbid peek and pop on the designated output, permit pushes, and require every goto target to remain in the safe set. Under these premises, running k steps after adding a suffix equals running k steps first and then adding that suffix to any resulting configuration.

**Formal evidence.** The selected BCESuffixFrame replay records three positive runs and three false controls rejected: peek, pop and reset-region counterexamples. Website preparation matched source and stdout hashes to the parent receipt.

**Boundary.** This is a sufficient condition in the specified semantics, not a necessary condition, a termination theorem, a CPU-time estimate or a general claim that output never affects computation. The reset-region control prevents widening the safe region without checking its premises.

**Source hash:** SuffixFrame.lean — 34e2e4a80807f39b9cf0d21e2eee8ad02c70bebb7fb0247f732657e789ee9c24.

## Evidence status and access

Across these four frozen families, the parent presentation task recorded 17 successful positive runs and eight deliberately false controls rejected, using existing pinned dependencies. These are 25 runs, not 25 discoveries or external certifications. The website task matched all 25 source files and stdout logs to the recorded hashes. It did not perform an independent Lean replay, clean-machine build, complete axiom audit or external mathematical review.

[Research exchange](https://app.notion.com/p/3ecfa095894c8147ae79e270070cef70) and [Lean programme](https://app.notion.com/p/3ecfa095894c810ea625ed08e17671a2) are private source records and may require permission. The companion supplies summaries and identifiers; it does not grant access to those records or contain the full proof sources. Request an approved proof packet from Ashley for independent checking.

Lean distinguishes proof validity from the meaning of the statement. Explanations are interpretations and must retain the exact conditions. [Lean reference](https://lean-lang.org/doc/reference/latest/ValidatingProofs/).