Corpus v3 · Axiom cid000014AXM0001activev1

Bridge Functor Exists

Project-local axiom assumed without proof: a bridge functor F: τ-Cat → Orth-Cat exists, mapping τ-side constructions to their orthodox counterparts. Used as a named gate in conditional proofs.

Payload

Bridge Functor Exists (AXM0001). There exists a functor F: tau-Cat → Orth-Cat from the τ-side category to an orthodox-side category, preserving the substrate-aligned structure.

This is a project-local assumption: it is not derived inside the τ-Kernel construction. It is used as a named gate in conditional proofs (notably the Riemann hypothesis Challenge Response).

Formalization

lean_axiom_freesorries: 0project axioms: 1

ModuleTauLib.Bridge.Functor
Declarationbridge_functor_exists

#print axioms

bridge_functor_exists

Identifiers

Corpus ID cid000014
Primary alias AXM0001
Type Axiom
Status active
Visibility public
Version v1

Aliases & legacy IDs

bridge-functor-exists

Release lines

corpus_v3_working

Version & History

v1 · 2026-05-10 initial corpus item seed

Status disclaimer

A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.

Save or share this page for inspection

Download a portable dossier, copy a reviewer note, or send this page to someone who can inspect it.

Email to expert