THE DISCRETE JACOBIAN PROGRAM

Local data can be complete.
Global history can still be lost.

The newest result separates two notions of reversibility. On the full unbounded two-vertex sector, at most one predecessor class for any target can coexist with non-isomorphic complete causal histories.

Explore
the new result↓

Lean-checked cores Working draft Not peer reviewed 27.07.2026 — 05.08.2026

01 / The local–global question

If every application of a rewrite can be uniquely reversed from its local output data, must the induced evolution on graph isomorphism classes be injective?

No. A rewrite can preserve vertex and edge counts, admit local undo data, and still erase which match produced the result.

The project isolates this gap for finite directed graph rewriting and asks which stronger local conditions recover global rigidity.

02 / The splice collision

Four matches.
One successor class.

Choose a source and one of its two matches. Apply the rule, inspect the named successor, then quotient by vertex relabeling.

{(a,a), (b,c)}→{(a,b), (c,a)}

a, b, c distinct · injective matching

Choose matched edge

loop match fixed at (0,0)

INPUT / S₁LOOP ⊔ OUT-STAR

{(0,0), (1,2), (1,3)}

replace the matched pair

OUTPUT / TAWAITING STEP

—

The loop fixes a = 0. The out-star’s branching direction distinguishes S₁ from S₂.

Canonical class reached

S₁ → [P₄]S₂ → [P₄]

Test both sources

The named successors are not literally equal. After relabeling, all four are isomorphic to the displayed canonical representative [P₄].

01DISTINCT SOURCES

S₁ ≄ S₂

S₁ has a vertex of out-degree 2; S₂ has none. Out-degree is invariant under isomorphism.

02SHARED CLASS

Succ(S₁)/≅ = Succ(S₂)/≅ = [P₄]

Each source has two valid matches. Every one of the four successors is a directed four-path.

03TERMINAL IMAGE

No loop, no next step

The rule requires a loop. Every successor is loop-free, giving unconditional mutual unreachability of the sources.

NEW RESULT / AI+ · CI−

At most one past class.
Two causal histories.

On the unbounded sector 𝒟₂ of finite directed multigraphs supported on at most two vertices, exactly three rules in the declared 3→3 grammar have at most one bare predecessor class for every target. Every one still admits complete chain and antichain histories with the same source and endpoint. Here 𝒟₂ names a domain, distinct from the project’s D2 closure condition below.

PROVED / UNBOUNDED 𝒟₂ LEAN FORM-3 CORE EXACT OCCURRENCE REPLAY

AI+

Ancestral injectivity

Fix a target. Its one-step predecessor fiber in 𝒟₂ contains at most one isomorphism class.

YES

CI−

Causal-poset invariance

Fix a source and endpoint. Complete schedules can induce non-isomorphic event orders.

LAB 01 / THE MULTIPLICITY TEST

Why exactly three rules survive

SELECTED CANONICAL RULE binary-00053

[00] + [01] + [10]→2[00] + [11]

One loop and both orientations become three loops.

Δ = RHS − LHS

+1−1−1+1

σ ↕

+1−1−1+1

UNBOUNDED 𝒟₂ CRITERION Δ = σΔ

Both injective bindings subtract the same change vector from a target, so they reconstruct the same predecessor vector.

PASSES FOR EVERY EDGE MULTIPLICITY

136canonical 3→3 rules in the declared grammar

3and only three satisfy Δ = σΔ

∞no edge-multiplicity bound in the theorem

Declared grammar: untyped binary directed 3→3 rules; at most two variables; loops and multiplicity up to three allowed; same variable set on both sides; connected LHS; changed rules only; quotient by shared variable exchange and edge-slot symmetry.

LAB 02 / EXACT OCCURRENCE CAUSALITY

Same endpoints, different causal order

ROOT OCCURRENCES / S = 2[00] + 2[01] + 2[10]

000100201301410510

e₀(0, 2, 4) → (6, 7, 8)

e₁(1, 3, 5) → (9, 10, 11)

600700811

90010001111

e₀consumes roots 0, 2, 4

e₁consumes disjoint roots 1, 3, 5

CAUSAL RELATION ∅

Neither event consumes output from the other; the two-event poset is an antichain.

SOURCES = 2[00] + 2[01] + 2[10]→ 2 × R₅₃ →TERMINAL ENDPOINTT = 4[00] + 2[11]

Exact enumeration has layers [1, 8, 28]: four complete antichain history classes and twenty-four complete chain history classes. Two events and six live edges are sharp minima for this family.

LAB 03 / THE DOMAIN BOUNDARY

Why a third vertex breaks injectivity

TWO VERTICES / ONE GLOBAL SWAP

Every inverse match uses the same unordered pair {0,1}.

The only two bindings are related by σ. When Δ = σΔ, both return t − Δ, so every nonempty bare predecessor fiber in the unbounded sector 𝒟₂ contains one class.

AT MOST ONE PREDECESSOR CLASS

GLOBAL OBSTRUCTION / HAND PROOF

Bare global injectivity fails when arbitrary positive context is allowed.

Place two rigidly tagged copies of the RHS inside one target Q. Reversing the left or right copy produces two predecessors. The tags pin every boundary role, so an isomorphism between those predecessors would force L = R—contradicting a genuinely state-changing rule.

same persistent boundary
positive exact matching
untouched arbitrary context
unrestricted untyped finite domain
bare target observation
genuine change, L ≠ R

P₀(L₀ + tags₀) ⊔ (R₁ + tags₁)

→

Q(R₀ + tags₀) ⊔ (R₁ + tags₁)

←

P₁(R₀ + tags₀) ⊔ (L₁ + tags₁)

WHERE TO LOOK NEXT

Six escape routes change a hypothesis, not the conclusion by fiat.

Typed rules

Let types prevent the duplicated comatches used by the obstruction.

Negative or induced matching

Allow context to disable a match rather than remaining purely positive.

Whole-state rules

Match the complete state, eliminating arbitrary untouched context.

Exact-support provenance

Observe the target together with the exact RHS occurrence support.

Vertex-changing interfaces

Leave the same-persistent-boundary setting of the theorem.

Context-restricted sectors

Work in a natural invariant domain, such as 𝒟₂, that excludes arbitrary tags.

WHAT IS ESTABLISHED

The unbounded 𝒟₂ delta criterion; the complete three-rule classification under explicit grammar caps; exact R₅₃ chain/antichain histories and sharp six-edge threshold; explicit three-vertex collisions; and the decorated-context obstruction under six stated hypotheses.

WHAT LEAN FORM-3 CHECKS

Lean checks the delta criterion, supported natural inverse reconstruction, the three distinct count-rule orbits, and the exact R₅₃ chain/antichain causal-poset witness. The generic ambient graph-match lift, six-edge width bound, R₇₇/R₁₂₄ fixtures, and global decorated-context obstruction remain outside Lean.

WHAT IS NOT CLAIMED

No theorem about physical spacetime, the polynomial Jacobian conjecture, every graph-rewriting formalism, or any continuum limit. The work remains a non-peer-reviewed research draft; the public archival theorem and certificate release for this newest result is pending.

03 / Definitions and scope

What “locally invertible”
means here.

A state is a finite multiset of ordered edges, considered up to vertex relabeling. Matches are injective; application uses DPO-style submultiset replacement.

D1 / SYNTACTICNECESSARY

No matched vertex is forgotten

Every variable on the left also occurs on the right: vars(L) ⊆ vars(R).

D1 / SEMANTICPRIMARY

Reverse readings agree at the comatch

For an application, every reverse match supported on exactly the comatch edge instances reconstructs the same predecessor up to isomorphism.

D2 / CLOSURESYSTEM

The reverse rule is legal too

A rule set is D2-closed when it contains the reverse of each rule and both directions satisfy D1.

D3 / CENSUSANALOGY

The signature action is unimodular

The induced integer action on selected local counts has determinant ±1. The splice rule preserves vertex and edge counts exactly.

04 / Formal evidence

One result.
Four evidence levels.

The site separates machine-checked facts from hand arguments, bounded experiments, and open questions.

LEAN-CHECKED HAND PROOF BOUNDED COMPUTATION OPEN

LEAN-CHECKED

SpliceCollision.lean

The concrete model proves that both sources step, the sources are not isomorphic, and every successor of S₁ is isomorphic to every successor of S₂. It also proves terminality for successors of S₁. The file contains no sorry.

Inspect the Lean file ↗

theorem splice_collision :
  (∃ t, RStep S1 t) ∧ (∃ t, RStep S2 t) ∧
  (∀ t₁ t₂, RStep S1 t₁ → RStep S2 t₂ →
    IsoTo t₁ t₂) ∧
  ¬ IsoTo S1 S2 := ...

IN LEAN

Concrete splice step relation
Non-isomorphism of S₁ and S₂
One shared successor isomorphism class
Terminality of S₁ successors

OUTSIDE THE LEAN FILE

Generic semantic-D1 infrastructure
The general rigidity theorem
The full computational search pipeline
External peer review

Technical note: Lean uses Finset (ℕ × ℕ); the search engine uses edge multisets. The flagship lies in their common no-parallel-edge fragment. The repository does not currently pin a Lean/Mathlib version.

05 / Bounded computation

A finite census,
with explicit limits.

The search enumerates a fixed universe of small binary-edge rules and states. Every number below is tier-stamped.

489candidate rules

Classes A, B, and B+

238probe survivors

Non-identity rules passing both D1 gates at ≤4V, ≤3E

52stage-1 candidates at ≤4V, ≤3E

50 independent; 2 downstream-only

182candidates at ≤4V, ≤4E

Mutual-orbit filtered; pair split not computed

Reported search tiers
Tier	Population	Result	Qualifier
≤4V, ≤3E	238 probe survivors	50 rules with ≥1 bounded-INDEPENDENT pair; 2 additional DOWNSTREAM-only candidates	86 independent pairs detected; 77 examples serialized
Census-preserving subset	105	16 independent + 2 downstream-only	12 of the 18 are policy-independent at their colliding states
≤4V, ≤4E	Same 238 survivors	182 min-successor collision candidates	Mutual-orbit filtered; INDEPENDENT/DOWNSTREAM split not computed
R2 / multiway	Archived selection of 226 one-rule systems	87 show merges	Exploratory run: seeds ≤4V/≤3E, depth ≤3, 300-state/seed and 6-vertex caps; current runner selection order is nondeterministic

These are finite-search results inside the stated rule universe—not asymptotic frequencies and not claims about graph-rewrite rules in general.

Enumerate

Generate canonical rule representatives in classes A/B/B+.

Gate

Apply syntactic and semantic-D1 probes to the bounded state set.

Classify

Canonicalize states and reject relabeling, orbit, and downstream artifacts.

Verify

Replay certificates with an independently implemented, self-tested verifier.

06 / Rigidity and open questions

History ambiguity is the exact obstruction
in one direction.

HAND PROOF

Rigidity theorem

If a rule is semantically D1 and history-unambiguous at every application, its one-step successor relation is injective on isomorphism classes, under every updating policy.

Elementary proof in PROOF_rigidity.md; not yet externally reviewed or Lean-formalized. Read the proof ↗

OPEN

The converse

Does a suitably independent form of history ambiguity force an eventual collision?

OPEN

Dynamic Garden of Eden

For an appropriate reverse-closed class of topology-changing systems, is surjectivity equivalent to pre-injectivity?

07 / Positioning

Adjacent to reversible dynamics.
Outside its protected class.

The contribution is a boundary example, not a claim to subsume existing graph-dynamics frameworks.

ARRIGHI · COSTES · MAIGNAN / 2025

Space-time reversible graph rewriting

They give sufficient local conditions in a context-preserving DAG/port-graph setting. The splice lies outside that class and demonstrates a failure mode when those protections are absent.

arXiv:2510.03296 ↗

ARRIGHI · MARTIEL · PERDRIX / 2015

Reversible causal graph dynamics

They assume global bijectivity and derive structural consequences for bounded-degree, time-varying graph dynamics—the converse direction from this project’s question.

arXiv:1502.04368 ↗

GORARD · NAMUDURI · ARSIWALLA / 2020

DPO-style Wolfram-model semantics

Their categorical treatment supplies the adhesive-category and double-pushout setting used as the project’s reference semantics.

arXiv:2010.02752 ↗

08 / Original release artifacts

The original result has
a public trail.

The links below reproduce the original splice and rigidity release. The newest AI+/CI− theorem and FORM-3 source are not represented by that DOI or repository and remain pending public archival release.

REPRODUCE.sh

$ cd phase1
$ python test_sanity.py
$ python verify_independent.py cert_flagship.json
$ python maxsweep.py

The Python checks require no third-party package. The repository publishes the zero-sorry Lean source, but does not pin lean-toolchain, lakefile, or a manifest; exact Lean replay from a clean clone is currently unavailable.

01 / MD

Citation / original release

Cite the registered original release only.

The DOI below does not yet archive the newest AI+/CI− theorem or FORM-3. Archived v1.0.0 also predates the rigidity theorem; cite its pinned source commit where relevant.

Rosero, Edwin. (2026). walkthroughwonder/discrete-jacobian: v1.0.0 — the splice collision (v1.0.0). Zenodo. https://doi.org/10.5281/zenodo.21630927
Concept DOI (all versions): https://doi.org/10.5281/zenodo.21630926
Rigidity source: https://github.com/walkthroughwonder/discrete-jacobian/tree/37302ea1feee5d86d30bc57f42dba0051597188d

Open pinned source commit ↗