<_HOME/>ROSETTA

One Proof, Many Lenses

Like the Rosetta Stone enabled translation between scripts, our lens bridges transform verified proofs through multiple mathematical representations. Each lens preserves semantic content while revealing different structural aspects.

LoF→Heyting→TensorCliffordGraphGeometricModalCausalFCANoneism

>SELECT_THEOREM

THEOREM #1

Reentry.idempotent

Applying the nucleus twice equals applying it once

R (R a) = R a

LoF

(( a ) ) = ( a )

((a))=(a)

Heyting

R (R a) = R a

Tensor

proj(proj(v)) = proj(v)

Clifford

P(P(x)) = P(x)

Graph

reach(reach(S)) = reach(S)

Geometric

cl(cl(X)) = cl(X)

Modal

[][]p <-> []p

Causal

Hull(Hull(S)) = Hull(S)

FCA

J(J(X)) = J(X)

Noneism

Stab(Stab(p)) = Stab(p)

>LENS_REFERENCE

LoF

Laws of Form

Primordial calculus with mark/unmark

Heyting

Fixed-Point Algebra

Intuitionistic lattice of fixed points

Tensor

32D Morphological Vectors

High-dimensional embeddings

Clifford

Bivector Geometry

Geometric algebra with projections

Graph

Adjacency Network

Dependency structure as directed edges

Geometric

Simplicial Complexes

Topological nerve constructions

Modal

Kripke Frames

Possible worlds semantics

Causal

Ancestral Hull

DAG reachability closure

FCA

Formal Concept Analysis

Attribute closure operators

Noneism

Paraconsistent Logic

Contradictions without explosion

>ROUND_TRIP_CONTRACT

Verified Lens Contracts

Each lens transformation is backed by a machine-verified round-trip contract. The decode/encode pair guarantees lossless translation: what goes in comes out unchanged.

RT-1: decode (encode a) = a

RT-2: shadow (encode a) = R a

/-- HeytingLean/Contracts/RoundTrip.lean --/

structure RoundTrip (R : Reentry α) (Obj : Type v) where
  encode : R.Omega → Obj
  decode : Obj → R.Omega
  round  : ∀ a, decode (encode a) = a

def interiorized (C : RoundTrip R Obj) : Obj → α :=
  fun x => R (C.decode x)

theorem interiorized_id (C : RoundTrip R Obj) (a : R.Omega) :
    interiorized C (C.encode a) = R a := by simp

>CODE_GENERATION

Verified Compilation: Proofs to Programs

The Rosetta principle extends beyond mathematical lenses to executable code. Via the Curry-Howard correspondence, proofs are programs and propositions are types. Our verified compilation pipeline transforms Lean specifications into executable C while preserving semantic correctness at each stage.

BAEZ-STAY CORRESPONDENCE

LOGIC

Propositions

Proofs

TYPES

Types

Terms

CATEGORY

Objects

Morphisms

PHYSICS

Systems

Processes

All four columns collapse to a single structure in the Heyting core Omega_R

VERIFIED PIPELINE

Lean 4

Specification

→

LambdaIR

Typed Lambda

→

MiniC

Imperative IR

→

Executable

END-TO-END SPECIFICATION

EndToEndNatSpec funName paramName leanF term

Compiled C function produces identical results to Lean specification for all inputs

STAGE CORRECTNESS

runCFunFrag fn n = evalClosed (app t n)

Each compilation stage preserves semantic equivalence

/-- HeytingLean/LambdaIR/ToMiniC.lean --/

/-- Compile a closed nat -> nat LambdaIR term into MiniC. -/
def compileNatFun (funName paramName : String)
    (t : LambdaIR.Term [] (Ty.arrow Ty.nat Ty.nat))
    : Except String Fun :=
  match t with
  | .lam body => .ok {
      name := funName
      params := [paramName]
      body := compileNatBody paramName body }
  | _ => .error "expected lambda"

/-- Specification: compiled code equals Lean semantics. -/
def NatFunSpec (funName paramName : String)
    (t : LambdaIR.Term [] (Ty.arrow Ty.nat Ty.nat)) : Prop :=
  forall fn, compileNatFun funName paramName t = Except.ok fn ->
    forall n, runNatFunFrag fn paramName n =
      some (LambdaIR.evalClosed (Term.app t (Term.constNat n)))

TARGET LANGUAGES

Verified pipeline with end-to-end correctness proofs

IMPLEMENTED

Rust

Memory-safe systems target with ownership semantics

PLANNED

WASM

Browser and edge deployment via WebAssembly

PLANNED

Solidity

Smart contract deployment with verified execution

RESEARCH

Minimal Trust Principle: Each stage of compilation is independently verified. The trusted computing base is minimized to the Lean kernel and C compiler semantics.

Read Full Paper: Verified Compilation from Lean to C →

>COMPARISON_NUCLEUS

Cross-ATP Proof Translation

The Comparison Nucleus provides a verified semantic core for translating proofs between theorem provers. Via Galois connections between complete lattices, we establish round-trip identities that preserve logical content across ATP boundaries.

GALOIS CONNECTION

Source Lattice

f→

f ⊥ g

←g

Target Lattice

→

Ω_R

Fixed Points

RT1: ROUND-TRIP IDENTITY

dec (enc a) = a

Translation to target and back yields the original proof

CLOSURE OPERATOR

R := g ∘ f : L → L

Nucleus on source lattice with idempotent, extensive, meet-preserving

PROOF ASSISTANT TARGETS

Lean 4

Primary development with dependent types and tactics

SOURCE

Coq

Verified translation via Comparison Nucleus RT1

VERIFIED

Isabelle/HOL

Higher-order logic with Isar proof scripts

PLANNED

Agda

Dependently-typed functional programming bridge

RESEARCH

/-- HeytingLean/LoF/ComparisonNucleus/RTTRI.lean --/

/-- Core data: a Galois connection f ⊣ g between lattices. -/
structure CompSpec (L : Type u) (Ω : Type v)
    [CompleteLattice L] [CompleteLattice Ω] where
  f : L → Ω
  g : Ω → L
  gc : GaloisConnection f g

/-- Fixed points of R := g ∘ f form the translation core. -/
def ΩR (S : CompSpec L Ω) : Type u := {x : L // act S x = x}

/-- Round-trip identity: decode ∘ encode = id on fixed points. -/
theorem RT1 (S : CompSpec L Ω) :
  (fun a : ΩR S => dec S (enc S a)) = id

Semantic Foundation: The Comparison Nucleus establishes that fixed points Ω_R of the closure operator form the universal translation core. Any proof in Ω_R can be faithfully represented in any target system sharing the same lattice structure.

Read Full Paper: The Comparison Nucleus →

>COLLABORATIVE_PROVING

Human / AI Collaborative Theorem Proving

Bridge the gap between human intuition and machine precision. Our proof2vec embedding system extracts proof structures into vector space, enabling AI-assisted proof search, automated lemma suggestion, and human-in-the-loop verification workflows.

Explore Collaborative Proving→

Lean Blueprint →CAB Certification →Proof Explorer →