Four formal result families anchor this exhibit. The wider programme connects them to a claim ledger and reusable proofs. Later experiments show how questions changed when a method met its limits. They retain different evidence statuses.
17positive runs passed
8false controls rejected
4frozen formal families
Selected local replay by the parent presentation task, using existing pinned dependencies. Website preparation hash-matched all 25 source files and stdout logs. These are runs, not discoveries or external certification. No new Lean replay was performed here.
01 · TRS-LEAN-HAB9-001
The factor-nine guarantee.
|B| ≤ 9κ(F)
Specified arity-at-most-three, whole-instance Horn/affine/bijunctive model. Selected-set size, not runtime or P versus NP.
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.
Unfold the definitions
F — the input
A finite list of explicit Boolean relation tables. Each table has at most three distinct variables. Empty and nullary tables are retained.
B — what is selected
The set of variables returned by the specified producer.
κ(F) — the comparison
The minimum cardinality of a valid set in this same model. It is not elapsed time.
Whole-instance validity
For every assignment to the selected set, one common target class covers all residual constraints. The class may depend on that assignment; it cannot be chosen independently for each component.
Assumptions, scope and exact source
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.
Arithmetic illustration only. This does not run the selector, find κ(F), produce an actual B or show tightness.
02 · Protected projection & 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.
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.
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.
The research is organized around a simple requirement: a result must carry its exact statement, dependencies, checks and remaining obligations. The Lean Establishment Programme records how that requirement becomes a working research process.
Programme inventory · source-reported checkpoint, 1 October 2026
Inventory
What it means
52 baseline sources
Original source files tracked by hash; coverage must be closed claim by claim.
615 claim/disposition rows
Definitions, compound claims, experiments, conjectures, dependencies and process records. Not 615 independent theorems.
18 initial groups
A dependency-driven organization of the work. Later batches add modules; this is not a count of completed groups.
One proof can make another possible.
The B002 record identifies actual applied proof dependencies within the factor-nine development:
witness_intersectionEvery valid backdoor meets the failed witness.
charged_decreaseThe witness supports the charging step.
run_specThe argument applies through the producer’s run.
This is a recorded proof-dependency path, not a claim that every proposed connection has been proved. The programme records 42 direct HAB9 theorem dependencies in this checkpoint. The website has not rerun that graph extraction.
Four questions stay separate.
Proof
Did the kernel accept the exact statement, with its dependencies and axiom audit?
Meaning
Does that statement express the intended mathematics, including quantifiers and representation?
Runtime
What operations, encodings, input access and storage does the cost model actually charge?
Integration
Does an implementation follow the formal specification?
A correction that improved the mathematics
B004 identified a missing cost variable: the protected set may contain arbitrarily many unused variables, even when the formula is small. B005 then formalized the eager list-checker protection charge as 2s + 1, where s is the raw protected-list length.
In that particular model, formula length and clause width alone cannot bound the guard cost. This is a precise correction, not an impossibility result for other data structures. The programme records the general proof separately from finite controls; this website has not replayed the B005 packet.
These are formalization areas, not a claim that all areas are complete. The page preserves later source-reported progress through B039, corrected statements, unsuccessful attempts and unresolved obligations. The full 52-source programme remains open.
Source: TRS-LEAN-ALL-001 · Lean Establishment Programme, fetched directly for this website; page revision 2 October 2026, 20:54 UTC. Programme reports are attributed to their research records. The website’s separately hash-checked 17-positive / 8-negative selected replay remains the narrower verification described above.
Progress includes corrections.
The B026–B039 journey consists of written arguments and finite computational evidence, not new Lean proofs. A repaired example is a reason to ask the next question, not permission to generalize.
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.
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.
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.
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.
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: a smaller residual, the same full-bank coverage.
Three chain examples · fixed admission caps
Example
Residual clauses
Elimination steps
1
49 → 1
18
2
121 → 1
40
3
241 → 1
70
Both combined methods decided the same 278 cases: 183 SAT and 95 UNSAT. Fallback calls fell from 137 to 134. One accepted-run timing was 5.966 seconds old versus 6.612 seconds new: slower, and not a calibrated performance comparison.
Failures, fixed caps and remaining boundaries
Caps stayed at two residual clauses and 256 tuples. Future pins on eliminated coordinates were refused. Two preparation runs failed in the auditor—JSON-key comparison and attempted lifting of core-only models—and their sources/logs were retained in the research record. The elimination implementation was unchanged.
These are reported same-host finite checks. The website did not replay B039; they add no general polynomial SAT bound, new Lean acceptance or independent external review.
We can only see a short distance ahead, but we can see plenty there that needs to be done.
A. M. Turing · Computing Machinery and IntelligenceRead the context & source
A. M. Turing, “Computing Machinery and Intelligence” (1950), §7, closing sentence, original page 460. Original English; no translator. Checked in the MSU-hosted transcription.
Turing closes a discussion of learning machines by considering different research starting points and acknowledging uncertainty about which approach to pursue. The sentence is not a prediction that this venture will succeed or a statement of present-day AI capability.
Author’s viewpoint, not proof evidence or an endorsement of RA.
Read the boundary as carefully as the result.
The historical TRS source identifiers remain unchanged. RA is the visitor-facing name. This public exhibit contains summaries and selected receipt metadata, not the private engine or a full proof package.
Research exchange — private Notion record; permission may be required.
Novelty, clean-machine reproduction, semantic review and product validation remain separate questions. Ask Ashley for an approved proof packet for independent checking; these links do not grant access.