Recursive Asterisms

An Anavi app In development

Explore the frontiers
of mathematics.

Build on verifiable foundations.

Explore a transformation

Follow a question. Transform its structure.
Inspect what holds.

(¬x∨y)∧x→x→true

Simplify the formula. Preserve the protected answer.

01 / A mathematical transformation

Change the formula.
Keep what matters.

A complete, eight-assignment example.
One protected variable. A trace we can reverse.

Original formula

Satisfying assignments
2
Possible protected values
z ∈ {0, 1}

● z = 0● z = 1

Each point is an assignment (x, y, z). Cube edges show one-bit differences; they are not proof steps.

Two solutions form a line through the cube.
1 / 6
Why these deletions are permitted

Start with F = (¬x ∨ y) ∧ x and protect z. First delete ¬x ∨ y using pivot y: no clause contains ¬y, so the blocking condition holds. Then delete the unit x using pivot x: no remaining clause contains ¬x. Both pivots are outside the protected set. The residual is true.

In reverse order, restore x before restoring ¬x ∨ y. Starting at 001, set x to 1, then y to 1. The result 111 satisfies F and keeps z = 1. In the wrong order, the first clause initially needs no repair, then setting x produces 101, which fails F.

The scene is a finite illustration of protected blocked-clause elimination, derived from the accepted opportunity paper. Its eight assignments and both repair orders are checked locally. It does not execute Lean or a live AI model.

Inspect the formal result and assumptions ↗

02 / Verifiable foundations

Wonder opens the question.
Evidence carries it forward.

The inquiry into P versus NP produced results worth understanding in their own right. Four selected formal families connect precise statements to recorded checks.

Explore the research ↗Read the two-page paper ↓
|B| ≤ 9κ(I)A proved size guaranteeBoolean tables · arity ≤ 3↗πS(Mod F)
= πS(Mod R)Protected answers surviveWith a valid reconstruction trace↗HornA correct restricted solverA guarded bridge; honest UNKNOWN↗runnWhen output cannot interfereScoped suffix commutation↗

Selected recorded replay: 17 positive runs passed; 8 deliberately false controls rejected. This website checked the recorded source identities; it does not run Lean. P versus NP remains open.

03 / The research journey

A question changes shape.

Follow the formulations, discoveries and corrections.
A smaller formula. A recovered witness. A faster-looking method that ran slower.

Follow the recorded journey

Follow the connections.

A shared map is useful when every connection says what it means.

Some paths are formal dependencies. Others are analogies, open questions or a future field of inquiry.

8 ideas

  • Backdoor

    Formal definition

    A set whose every assignment leaves the whole instance in one common target class: Horn, affine or bijunctive. The class may vary with the assignment.

    Formal dependency → Factor-nine uses this exact definition.

    Explore backdoor

  • Factor-nine

    Formal result

    The specified selector returns a valid set with |B| ≤ 9κ(F), for explicit Boolean tables of arity at most three. A set-size bound, not a runtime bound.

    Formal dependency ← Whole-instance backdoor definition.

    Explore factor-nine

  • Protected projection

    Equivalence under assumptions

    Original and residual model sets have equal projections on the protected variables along permitted deletion traces. Their full model sets may differ.

    Equivalence under assumptions ↔ Original / residual protected models. Analogy → suffix preservation, not a shared proof dependency.

    Explore protected projection

  • Horn solver

    Formal result

    A correct restricted decision core with a guarded encoded-CNF bridge. Admitted non-Horn inputs can remain UNKNOWN; malformed input is rejected.

    Formal dependency: encoded-input claims rely on the guarded bridge. No dependency on the factor-nine implementation is asserted.

    Explore horn solver

  • Output suffix

    Formal result

    Adding output suffixes commutes with fixed-step execution under no-read/no-pop and closed-label support in the specified TM2 semantics.

    Analogy ← Protected projection: both make preservation conditions explicit. This is not a proof edge.

    Explore output suffix

  • Meta

    Organizing lens

    Reasoning about the inquiry itself: what is assumed, how it is checked and which correction changes the next question. Not a universal discovery theorem.

    Analogy → Multiverse as branching contexts. Conjecture → whether reviewed shared reuse saves total effort.

    Explore meta

  • Multiverse

    Disambiguation · analogy

    Do you mean alternative mathematical contexts, branches of inquiry, or physical cosmology? Here it is only a metaphor for declared contexts; no cosmological theorem is asserted.

    Analogy ← Meta. Changing axioms does not automatically transfer results.

    Explore multiverse

  • Stoichiometry

    Future domain · illustration

    Balancing 2H₂ + O₂ → 2H₂O gives linear conservation equations. A useful future connection, not demonstrated transfer of the research engine.

    Future domain → Linear algebra through atom conservation. No formal edge to the Boolean results.

    Explore stoichiometry
Formal dependency — a result uses a definition or theoremConditional equivalence — same specified propertyAnalogy · Conjecture · Future domain — no proof transfer

Continue the inquiry

Bring a question.
Take a new perspective.

Explore the programme. Read the evidence.
Take the companion into your own AI conversation.

Take the companion ↗Inside the programme