Cortex

Cortex

Research wiki
  • Cortex
  • Glossary
  • Map
  • Style
  • Taxonomy
  • 01. Quickstart
  • 02. First Wire workflow
  • 03. Running Pulse
  • 04. Deploying Pulse
  • 05. Integrating from Haskell
  • 06. Troubleshooting
  • 01. Overview active
  • 02. Ownership and boundaries active
  • 03. Algebraic foundations active
  • 04. Graph and Circuit active
  • 05. Wire language active
  • 06. Pulse runtime active
  • 07. Rewrites and materialization active
  • 08. Artifacts and provenance active
  • Wire
  • Proof status active
  • Development
  • Pulse accepted
  • Rewrites accepted
  • Cortex Terminology accepted
    • Pulse schema accepted
    • Pulse types accepted
    • Pulse service API accepted
    • Pulse host actions accepted
    • Pulse signals accepted
    • Pulse run events accepted
    • Grammar accepted
    • Modules and imports draft
    • Style accepted
    • Contracts and ports draft
    • Configured executors draft
    • Executors draft
    • Pure execution draft
    • Conditionality draft
  • 0001. Structured Document IR superseded
  • 0002. Ownership boundary accepted
  • 0003. Pulse boundary accepted
  • 0004. Graph-native execution accepted
  • 0005. Rewrite admission accepted
  • 0006. Workflow artifact accepted
  • 0007. Conditional lowering accepted
  • 0008. Operator visibility accepted
  • 0009. Graph integrity accepted
  • 0010. Wire authority accepted
  • 0011. Compatibility barriers accepted
  • 0012. Topological memory accepted
  • 0013. Artifact provenance accepted
  • 0014. Model vs external call proposed
  • 0015. Logos archetypes proposed
  • 0016. Cortex roots proposed
  • 0017. Executor and ports proposed
  • 0018. Haskell tree proposed
  • 0019. Executor binding proposed
  • 0020. Pure output equations accepted
  • 0021. Source elaboration proposed
  • 0022. Node clause grammar proposed
  • 0023. CorePure surface proposed
  • 0024. Typed executors proposed
  • 0025. Configured executors proposed
  • 0026. Wire failures proposed
  • 0027. Typed LLM output proposed
  • 0028. Topology composition proposed
  • 0029. CorePure serialization proposed
  • 0030. Node implementation forms proposed
  • 0031. Binding forms and where proposed
  • 0032. Boundary resources proposed
  • 0033. Guarded collapse proposed
  • 0034. Pure select authority proposed
  • 0035. Rewrite forms proposed
  • 0036. Latent branch budget proposed
  • 0037. Latent control proposed
  • 0038. Proof ledger proposed
  • 0039. Node boundary normal form proposed
  • 0040. Logos reasoning surfaces accepted
  • 0041. Wire CLI command proposed
  • 0042. Standard effect executors proposed
  • 0043. Pulse in-memory runner proposed
  • 0044. Namespace use imports proposed
  • 0045. Node-body kinds proposed
  • 0046. Graph forms proposed
  • 0047. Frontier linearity and precedence proposed
  • 0048. Make proposed
  • 0049. Fan phantom adapter proposed
  • 0050. CorePure residue proposed
  • 0051. Source includes proposed
  • 0052. Indexed products proposed
  • 0053. Executor catalog bindings proposed
  • 0054. Wire packages and host bindings proposed
  • Logos
  • Portman
  • Quantum draft
    • Reasoning library active
  • Paper 1 draft
  • Roadmap active
  • Paper 2 draft
  • Paper 3 draft
  • Paper 4 draft
  • Paper 6 draft
  • Publication Notes research
    • Deterministic Multi-Rewrite Admission draft
    • Ideas
    • Typeset PDF
    • Paper 1 — Lean 4 Mechanization Plan draft
    • Paper 1 — Lean-Haskell Pulse Boundary draft
    • Paper 1 Figures draft
    • Staged Reduction for Durable Workflow Execution draft
    • Typeset PDF
    • Paper 2 Figure Inventory draft
    • Paper 2: Algebraic Foundations draft
    • Typeset PDF
    • Paper 3 Figure Inventory draft
    • Paper 3: Graph Substitution Semantics draft
    • Typeset PDF
    • Paper 4 Figures draft
    • Wire: Closed Alphabets, Open Composition for Typed Workflow Graphs draft
    • Causal Programming: Temporal Honesty as a Foundation for Verified Distributed Systems draft
    • Figures draft
    • Typeset PDF
    • Executable Causal Diagrams with Typed Linear Frontiers draft
  • Epics
  • Plans
  • Completed
  • Archive
    • Substrate soundness active
    • Lean mechanization proposed
    • Rewrite materialization proposed
  • Foundation
  • Runtime
  • Wire
  • Applications
    • Research Memo: Stage-Structured Causal Pipelines research
    • Research Memo: Linear Port Graph Layer research
    • Research Memo: CALM and Coordination Boundaries on Evolving Graphs active
    • Research Memo: Cortex Formalism Stack Synthesis
    • Topological Memory — Iteration Synthesis
    • Wire Admission Correspondence After PR 189 research
    • Wire Frontier Binding Syntax research
    • Wire Composition Sugar: Operators, Templates, Lambdas, Combinator Executors research
    • Module Index
    • Cortex
    • Cortex.Graph.Core
    • Cortex.Graph.Laws proofs
    • Cortex.Graph.Quotient proofs
    • Cortex.Graph.Relation proofs
    • Cortex.Graph.Safety proofs
    • Cortex.Pulse.Classify proofs
    • Cortex.Pulse.Closure proofs
    • Cortex.Pulse.DAG proofs
    • Cortex.Pulse.Fact proofs
    • Cortex.Pulse.Frontier proofs
    • Cortex.Pulse.Recovery proofs
    • Cortex.Pulse.RunSafety proofs
    • Cortex.Pulse.State proofs
    • Cortex.Pulse.Validity proofs
    • Cortex.Wire.ActualizedBridge proofs
    • Cortex.Wire.Admission proofs
    • Cortex.Wire.AdmissionArtifact
    • Cortex.Wire.AdmissionArtifact.Boundary proofs
    • Cortex.Wire.AdmissionArtifact.Check proofs
    • Cortex.Wire.AdmissionArtifact.Generated proofs
    • Cortex.Wire.AdmissionArtifact.GeneratedReconstruction proofs
    • Cortex.Wire.AdmissionArtifact.Phantom proofs
    • Cortex.Wire.AdmissionArtifact.PhantomReconstruction proofs
    • Cortex.Wire.AdmissionArtifact.Primitive proofs
    • Cortex.Wire.AdmissionArtifact.PrimitiveReconstruction proofs
    • Cortex.Wire.AdmissionArtifact.PrimitiveTraceCheck proofs
    • Cortex.Wire.AdmissionArtifact.ReadyGeneral proofs
    • Cortex.Wire.AdmissionArtifact.ReadyGenerated proofs
    • Cortex.Wire.AdmissionArtifact.ReadyPhantom proofs
    • Cortex.Wire.AdmissionArtifact.ReadyPhantomBridge proofs
    • Cortex.Wire.AdmissionArtifact.ReadyPrimitive
    • Cortex.Wire.AdmissionArtifact.ReadyPrimitiveRows proofs
    • Cortex.Wire.AdmissionArtifact.ReadySelect proofs
    • Cortex.Wire.AdmissionArtifact.ReadySelectBridge proofs
    • Cortex.Wire.AdmissionArtifact.ReadySummary proofs
    • Cortex.Wire.AdmissionArtifact.Select proofs
    • Cortex.Wire.AdmissionArtifact.SelectReconstruction proofs
    • Cortex.Wire.AdmissionArtifact.Sound proofs
    • Cortex.Wire.AdmissionArtifact.StaticValue proofs
    • Cortex.Wire.AdmissionArtifact.Validator
    • Cortex.Wire.AdmissionArtifact.ValidatorCore proofs
    • Cortex.Wire.AdmissionArtifact.ValidatorCoreCheck proofs
    • Cortex.Wire.BoundaryResource proofs
    • Cortex.Wire.ElaborationIR proofs
    • Cortex.Wire.FrontierReclaim proofs
    • Cortex.Wire.GeneratedForms proofs
    • Cortex.Wire.GraphElaboration proofs
    • Cortex.Wire.Make proofs
    • Cortex.Wire.NodeBoundary proofs
    • Cortex.Wire.PhantomAdapter proofs
    • Cortex.Wire.Planner proofs
    • Cortex.Wire.Planner.Chain proofs
    • Cortex.Wire.Planner.Construction proofs
    • Cortex.Wire.PortLinearity proofs
    • Cortex.Wire.PulseSafety proofs
    • Cortex.Wire.Pure proofs
    • Cortex.Wire.Registry proofs
    • Cortex.Wire.Rewrite proofs
    • Cortex.Wire.RunTrace proofs
    • Cortex.Wire.Select proofs
    • Cortex.Wire.SelectAdmission proofs
    • Cortex.Wire.SelectRecovery proofs
    • Packages
    • cortex
    • Cortex
    • Cortex.Algebra
    • Cortex.Algebra.Graph
    • Cortex.Algebra.Graph.Core
    • Cortex.Algebra.Graph.Decompose
    • Cortex.Algebra.Graph.Influence
    • Cortex.Algebra.Graph.Modify
    • Cortex.Algebra.Graph.Mokhov
    • Cortex.Algebra.Graph.Search
    • Cortex.Algebra.Graph.Validate
    • Cortex.Capability
    • Cortex.Capability.Executor
    • Cortex.Capability.Executor.Pure
    • Cortex.Pulse
    • Cortex.Pulse.Attempt
    • Cortex.Pulse.Checkpoint
    • Cortex.Pulse.Database
    • Cortex.Pulse.Event
    • Cortex.Pulse.Executor
    • Cortex.Pulse.Executor.Attempt
    • Cortex.Pulse.Executor.Events
    • Cortex.Pulse.Executor.Frontier
    • Cortex.Pulse.Executor.Loop
    • Cortex.Pulse.Executor.Outcome
    • Cortex.Pulse.Executor.Persistence
    • Cortex.Pulse.Executor.ReplayPolicy
    • Cortex.Pulse.Executor.Resume
    • Cortex.Pulse.Executor.Types
    • Cortex.Pulse.Frontier
    • Cortex.Pulse.GraphRuntime
    • Cortex.Pulse.GraphStateRevision
    • Cortex.Pulse.Health
    • Cortex.Pulse.Hydrate
    • Cortex.Pulse.Materialization
    • Cortex.Pulse.Materialize
    • Cortex.Pulse.Memory
    • Cortex.Pulse.Memory.Query
    • Cortex.Pulse.Memory.Score
    • Cortex.Pulse.Memory.Tool
    • Cortex.Pulse.Memory.Types
    • Cortex.Pulse.Memory.Walk
    • Cortex.Pulse.Node
    • Cortex.Pulse.Outcome
    • Cortex.Pulse.Persistence
    • Cortex.Pulse.Plan
    • Cortex.Pulse.PlanHydration
    • Cortex.Pulse.Query
    • Cortex.Pulse.Replay
    • Cortex.Pulse.Resume
    • Cortex.Pulse.Rewrite
    • Cortex.Pulse.Runtime
    • Cortex.Pulse.Scheduler
    • Cortex.Pulse.Schema
    • Cortex.Pulse.Signal
    • Cortex.Pulse.Types
    • Cortex.Wire
    • Cortex.Wire.AdmissionArtifact
    • Cortex.Wire.Circuit
    • Cortex.Wire.Circuit.Artifact
    • Cortex.Wire.Circuit.Compile
    • Cortex.Wire.Circuit.Compiled
    • Cortex.Wire.Circuit.Compiler
    • Cortex.Wire.Circuit.IR
    • Cortex.Wire.Circuit.Lower
    • Cortex.Wire.Circuit.Lowering
    • Cortex.Wire.Circuit.Node
    • Cortex.Wire.Circuit.NodeKind
    • Cortex.Wire.Compile
    • Cortex.Wire.Contract
    • Cortex.Wire.Executor
    • Cortex.Wire.Format
    • Cortex.Wire.Include
    • Cortex.Wire.Parser
    • Cortex.Wire.Pure
    • Cortex.Wire.Std
    • Cortex.Wire.Syntax
    • Cortex.Wire.Use
    github.com/Digimuoto/cortex

    © 2026 Cortex

    Tags / lean

    Lean

    5 documents tagged lean.

    • Cortex
    • Cortex.Graph.Core
    • Cortex.Wire.AdmissionArtifact
    • Cortex.Wire.AdmissionArtifact.ReadyPrimitive
    • Cortex.Wire.AdmissionArtifact.Validator