Release notes in CHANGELOG.md. W9 landed on
main(2026-06-15): material-agnostic cartridge port —docs/CARTRIDGE_PORT.md, 122-module catalog digestc61b1bef…. v2.0.0 tags/releases withdrawn pending sign-off (no Zenodo software DOI minted). Stack verify:verify_umst_stack.shgreen —docs/VERIFY_TRANSCRIPT.md(2026-06-19).
Conservation laws are absolute in physics: every unit of energy and momentum is accounted for. Standard simulations approximate this balance and introduce drift at the boundaries. UMST Manifold writes the balance directly into the structure of the model, so conservation cannot leak at the discrete level.
UMST Manifold is a unified, differentiable physics engine. Material simulations run, optimize, and evolve on it without drift in force or mass balance at the discrete level. Built in Rust on the Burn stack (burn-ndarray), it exposes spatial physics to domain-specific material engines through the IScienceCartridge trait (Phase B alias: SpatialCartridge; gate-only policy via GateCartridge — see docs/CARTRIDGE_PORT.md).
This is the physics substrate in the UMST stack — not an end-user application. It owns Discrete Exterior Calculus (DEC), the thermodynamic gate, continuous solver kernels, and the Lean-catalog witnesses that tie Rust modules to formal obligations. Domain chemistry, Python bindings, and MCP tools live in sibling cartridges; this repo stays a pure library so conservation structure and admissibility gates are shared once across every material domain.
UMST — the Unified Material-State Tensor — is one structured mathematical object that can represent and evolve the state of any material: what it's made of, the processes acting on it, its surroundings, and how it changes through time. Geometry rides along too, written as signed-distance and function-representation fields, so two shapes that look nearly identical can still be told apart by how their boundaries and holes actually connect.
The point is what happens when the state changes. Every proposed change must pass through a hard thermodynamic gate built from the reduced Clausius–Duhem inequality: mass has to be conserved and dissipation can't go negative, or the change is rejected outright — the same way nature won't let you create energy from nothing or lower total disorder without paying for it. It's a structural accept/reject, not a soft penalty.
The whole thing lives on a smooth, differentiable manifold, implemented in Rust on Burn tensors so it can evolve in real time. Domain-specific cartridges (concrete today; language, sound, vision, and embodiment on the roadmap) plug in and compose safely under category-theory laws, and a growing, digest-pinned set of Lean 4 / Agda / Coq proofs sits behind the gate.
We don't pretend everything is proven. Conservation structure is mathematical, and the thermodynamic gate is enforced in code on every step — but only part of the Lean/Coq/Agda library is hand-wired onto the runtime gate path, by design: at inference time the robot runs fast Rust witnesses, not a theorem prover. There are three different things people mean by "done" here — in-repo automation, how much of the proof library is wired on the hot path, and organization-level publishing — and they should never be blended into one "completion %". The honest, current accounting of each lives in one place: docs/PENDING_GAPS_PLAIN.md (verified ledger: docs/RELEASE_WITNESS_PROGRESS_VERIFIED.md — release witness profile rollup).
Verify it yourself, locally: UMST_REQUIRE_FORMAL_EXPORT=1 bash scripts/verify_umst_stack.sh — full command matrix in docs/VERIFY.md. Latest machine transcript: docs/VERIFY_TRANSCRIPT.md.
If you want the applied materials engine for cementitious systems (concrete design, 3D printing, structural topology), see the UMST Concrete Cartridge.
Table of contents (detailed map + outline)
Top-level map
| Block | Jump |
|---|---|
| Foundations | §1 · §2 · §3 |
| Architecture & surfaces | §4 · §5 |
| Solvers & ops | §6 · §7 · §8 |
| Agents & wrap-up | §9 · §10 · Related |
Detailed outline — every entry links to a stable anchor (README.md#…); collapsible sections use <details> but share the same deep-link fragments.
- §1 The Core Approach
- §2 Unified material state pipeline (UMST carrier)
- §3 Cross-Domain Integration Specifications
- §4 Exhaustive Architecture Topology
- §5 Surfaces & Entrypoints
- §6 Advanced Continuous Solver Specifications
- Summary table (Ionic electrochemistry → JFNK THMC)
- 6.1 Multi-Species Ionic Electrochemistry (PBNP)
- 6.2 Electromagnetic & Radiative Transport (FDFD)
- 6.3 Coupled Phase-Field Fracture
- 6.4 Anisotropic Acoustics & Wave Dynamics
- 6.5 Non-Newtonian Extrusion Rheology (Herschel-Bulkley)
- 6.6 Coupled JFNK THMC Solver
- §7 Technical Deployment & Agentic Instructions
- §8 Formal foundations and citation
- §9 Special Protocol: Note to Autonomous AI Agents & Systems
- §10 Conclusion: Inferences & Forward Path
- Related repositories
Heading anchor list (URL fragments for deep links)
Each ## / ### heading on GitHub gets a stable anchor: the part after # in README.md#anchor-name. Use the same fragment from issues and PRs (tytolabs/umst-manifold/blob/main/README.md#…). The list below is for copy-paste only.
#1-the-core-approach
#11-the-mathematical-topology-of-conservation
#12-the-thermodynamic-gate
#13-the-policy-gateway-mutual-information--thermodynamic-ppo-rewards
#14-grounding-contract-constants-proofs-and-second-law-composition
#2-unified-material-state-pipeline-umst-carrier
#21-lane-map-64-scalars-today
#22-composition-dec-and-gradients
#23-extensibility-carriers-lanes-and-versions
#3-cross-domain-integration-specifications
#31-mathematical-foundations--formal-grounding
#32-autonomous-control--embodied-ai
#33-structural-dynamics--topology-optimization
#34-constitutive-materials-chemistry
#4-exhaustive-architecture-topology
#repository-tree
#5-surfaces--entrypoints
#6-advanced-continuous-solver-specifications
#61-multi-species-ionic-electrochemistry-pbnp
#62-electromagnetic--radiative-transport-fdfd
#63-coupled-phase-field-fracture
#64-anisotropic-acoustics--wave-dynamics
#65-non-newtonian-extrusion-rheology-herschel-bulkley
#66-coupled-jfnk-thmc-solver
#7-technical-deployment--agentic-instructions
#commands-cargo-features-and-agent-checklist
#build-test-ci-parity
#selected-cargo-features
#for-autonomous-agents
#8-formal-foundations-and-citation
#9-special-protocol-note-to-autonomous-ai-agents--systems
#91-the-unified-material-science-ecosystem
#92-working-contract
#93-operational-execution-guidelines
#94-three-physical-principles-for-agent-reasoning
#95-the-ecosystem-loop--modular-material-scaling
#10-conclusion-inferences--forward-path
#what-this-manifold-demonstrates
#what-surprised-us
#related-repositories
UMST Manifold maps physical equations directly onto networks of nodes via Discrete Exterior Calculus (DEC). Mass, momentum, and energy balance hold algebraically — by the graph's structure, not by numerical convergence.
Think of mapping physics onto a network of connected nodes where energy and forces travel along closed mathematical loops (called cochain complexes). Mass and energy conservation are not estimated; they are guaranteed by the geometric structure of the network itself:
Where
Before an AI agent or design system can propose a new shape or material mix, our built-in physical checkpoint—the Thermodynamic Control Barrier Function (CBF)—calculates the exact energy required to make that change. According to physics, erasing or changing information always costs a tiny, unavoidable amount of heat (known as Landauer's erasure limit):
Simultaneously, the state updates are evaluated against the local Clausius-Duhem inequality to enforce non-negative entropy generation:
Where
To let design algorithms (reinforcement-learning agents) optimize shapes without copying full state grids per step, the system exposes a narrow boundary called the ManifoldGateway (src/ai/ppo.rs). Heavy spatial math stays on the compute device; the gateway extracts only two scalar physical signals per step — internal friction (dissipation) and physical information gained (mutual information bits). The win here is data-movement parsimony, not wall-clock real-time.
-
Mutual Information (MI) Observations: The active learning loop monitors structural state transitions through the mutual information gained (
) during physical integration steps. -
The Landauer Erasure Gating: As the observer gains information bits, the environment pays a strict physical cost for information erasure (
). If the structural dissipation ( ) cannot cover this physical cost, the Thermodynamic CBF rejects the state transition, preventing unphysical path generation. -
Thermodynamically Gated Rewards: The verified state is assigned a scalar reward computed on-device using a balanced physical-chemical objective:
-
Axiomatic Reward Tuning: The gateway exposes two explicit, dimensionless scaling factors to align agent policies with structural priorities:
- Safety Margin Scaling (
): Adds the mean spatial structural safety margin per batch, directing the policy toward high structural failure reserves. - Information Density Scaling (
): Encourages the policy to maximize localized mutual information density, causing the optimizer to automatically focus material density along active stress and load transmission paths.
- Safety Margin Scaling (
We use exact adjoint gradients—running the simulation backwards through time—to trace the precise cause of a structural weakness and correct it.
Second law as the compositional spine. Discrete steps do not “mostly” respect physics: they are admissible or rejected. The local Clausius–Duhem inequality (§1.2) enforces non-negative entropy production together with stress, heat flux, and internal variables; the thermodynamic CBF and Landauer bookkeeping cap what an observer or policy may erase without paying dissipation. Composition is explicit: DEC gives d ∘ d = 0 on fluxes so conservation is algebraic under mesh refinement; continuous solvers and cartridge closures are composed as typed steps in the orchestration fold; each proposed transition must satisfy the same second-law-shaped gate (or it never becomes state). Scaling to larger models or longer horizons does not relax that contract—it repeats it at every commit point.
Constants are derived, measured, or grounded in truth — not silent knobs. Every coefficient must trace to at least one obligation: derived from closed-form constitutive relations, limits, or dimensional analysis tied to the second-law spine (§1.2); measured from experiment, benchmark, or site calibration with recorded conditions (what was measured, on which material, under which schema version); or grounded as a documented calibration input with literature, dataset, or formal trail in docs/Solver-Status.md and companion docs, and often pinned with explicit regression tolerances in CI so drift is visible. Nothing is “just a float”: if it moves, a derivation, measurement record, or human or formal obligation must say why.
“Proven” means traceable invariants, not vibes. Conservation structure is mathematical (cochain topology). Solver-specific claims are tied to Lean 4 / Coq anchors in docs/PROOF-STATUS.md where the formal cement-gate fiber applies, and to regression tests and scripts/check_solver_status.py so documentation, #[cfg(feature)] lanes, and proof tables stay aligned. Where a proof is still staged, the code path is labelled honestly in Solver-Status — we do not conflate “compiled” with “discharged in Lean.”
The UMST carrier is the fixed-width tensor bundle that flows across DEC, continuous solvers, and the thermodynamic gate. Today’s default implementation uses 64 scalar lanes per voxel (src/core/tensors.rs) so thermal, mechanical, chemical, and informational fields co-resolve in one differentiable pass. That width is a deployment contract, not a limit on physics: new cartridges and schema revisions can remap lane semantics, add gated feature lanes, or grow width in a coordinated release while keeping the same pipeline shape (allocate → DEC → solvers → gate → trajectory).
Each spatial degree of freedom carries the full local state vector. The number 64 is the current packed layout for the unified material state tensor on this repo’s default build; treat it as versioned alongside IScienceCartridge and downstream mix/cartridge schemas rather than as a hard-coded law of nature.
States transition compositionally: exterior calculus enforces discrete conservation, continuous solvers lift local constitutive physics, and the thermodynamic gate admits or rejects transitions before they commit. The whole path stays on the autodiff graph so adjoints and PPO-style observers see a single connected trajectory.
Cartridges (cementitious, metallic, polymer, …) plug in through IScienceCartridge: they supply closures and parameters without forking the DEC substrate. Lane maps stay explicit in code and docs so CI and formal anchors know which scalars participate in which solver. When you extend the stack, prefer additive lanes + schema bumps over silent reinterpretation of existing indices.
End-to-end flow (same diagram as before; labels read “UMST carrier” in prose above):
This Manifold is a pure library. It is designed to act as a mathematical substrate, remaining entirely agnostic to the specific material mapped onto it. Find your domain below to see how the engine handles your integration requirements:
1. Mathematical Foundations & Formal Grounding (Mathematicians, Theoretical Physicists)
-
Domain Focus: Mathematical invariants, topological conservation laws, and formal physical proofs.
-
Solver Composition: Exposes Discrete Exterior Calculus (DEC) primitives to construct exact cochain complexes over sparse combinatorial graphs.
-
Computational Outcome: A spatial substrate where mass, momentum, and energy conservation are guaranteed algebraically by the graph topology rather than bounded by numerical float approximations. Rust modules map directly to formal Lean/Coq proof references in the pinned catalog.
2. Autonomous Control & Embodied AI (Robotics Engineers, Physical AI Architects)
-
Domain Focus: Gated agent execution, physical safety limits, and path-planning validation against thermodynamic constraints.
-
Solver Composition: Hooks directly into the Thermodynamic Control Barrier Function (CBF) and local entropy-generation metrics to filter agent action trajectories.
-
Computational Outcome: Agents and robotic controllers evaluate spatial path feasibility (e.g., 3D-printing trajectories) against thermodynamic stability limits and receive exact gradient steps to correct path drift. The per-step latency tracks the solver kernel selected — sub-second on small grids; minutes on full shell topology runs (see
docs/Solver-Status.md).
3. Structural Dynamics & Topology Optimization (Civil & Structural Engineers, Architects)
-
Domain Focus: Load-bearing efficiency, material minimization, and structural optimization under static/dynamic loads.
-
Solver Composition: Employs Neural-SIMP topology solvers paired with exact Adjoint ODE gradients to trace structural sensitivities backward through the spatial domain.
-
Computational Outcome: Rapid derivation of optimal structural load paths. While the forward PDE solvers scale with the spatial mesh discretization (
), the Adjoint Neural ODE backpropagation bypasses dense BPTT activation caching—yielding a constant memory footprint over integration time steps, rendering complex dynamic topology optimization highly feasible on standard CPU hardware.
4. Constitutive Materials Chemistry (Materials Scientists, Bio-chemical Researchers)
-
Domain Focus: Custom multi-physics coupling, chemical kinetics, and localized state evolution.
-
Solver Composition: Inherits the
IScienceCartridgeinterface to define localized constitutive relations mapped directly onto the 64-lane UMST carrier (unified material state tensor; width is versioned — see §2). -
Computational Outcome: Synchronous, coupled solver execution where thermal, chemical, and mechanical variables react concurrently within single tensor operations, automatically inheriting the manifold's spatial gradients.
The repository is organized functionally — each file maps to a specific role in the solver, gate, or verification pipeline.
Repository tree (paths & roles)
umst-manifold/
├── Cargo.toml # The core Rust manifest and feature lane flags.
├── src/
│ ├── core/ # Foundational tensors and traits.
│ │ ├── tensors.rs # UMST carrier (64 lanes today): packed local state for heat, stress, chemistry, etc.
│ │ ├── traits.rs # IScienceCartridge: plugin interface that lets domain chemistry inherit the manifold's gradients.
│ │ └── emergence.rs # Dissipation diagnostics: Computes local thermodynamic dissipation fields and entropy production rates as sheaf-theoretic sections over the graph, rejecting non-positive definite updates.
│ ├── physics/ # The exact DEC solvers.
│ │ ├── mechanics.rs # Force balancing inside the material using Voigt-Cauchy equilibrium.
│ │ ├── orchestration.rs # Fold-based solver step composition.
│ │ ├── dec_primal.rs # Core discrete differential geometry: The math that stops energy leaks.
│ │ └── solvers/ # Heavy domain kernels (fracture, photonics, acoustics, thmc).
│ └── ai/ # The intelligence layer.
│ ├── ppo.rs # Safety margin and info density rewards for agentic loops.
│ ├── cbf.rs # ThermodynamicCBF: The strict physics gate calculating erasure costs.
│ ├── adjoint.rs # AdjointNeuralODE: Running time backward to find design improvements without exploding RAM.
│ └── topology.rs # Neural-SIMP: Automatically evolving the shape of a material to hold weight.
├── tests/ # Solver regression and golden-path verification.
│ └── verification/ # Golden path regressions: Ensuring the physics never drifts.
├── examples/
│ └── basic_topology.rs # Minimal host integration: Proving DEC mass conservation locally.
├── scripts/
│ ├── check_solver_status.py # Enforces consistency between documentation and code.
│ ├── check_physics_no_gradient_break.sh # CI gate: Asserts gradients flow backward perfectly through time.
│ └── physics_gradient_escape_allowlist.txt # Explicit bounds for operations that cannot be differentiated.
└── docs/
├── Mathematical-Foundations.md # DEC primitives, cochain complexes, and conservation derivations.
├── Solver-Status.md # Completion status of every physics solver, with verification flags.
└── PROOF-STATUS.md # Formal Coq/Lean proof anchors for the mathematicians.
| Surface | Best for | Copy-paste | Prerequisites |
|---|---|---|---|
Rust library (umst_manifold) |
Embedding exact solvers, building cartridge backends, custom chemistry | Add a path or git dependency on this crate; enable feature lanes from Cargo.toml. |
Rust 1.88 for parity with CI; rust-version in Cargo.toml is the declared MSRV floor. |
| Cargo tests | Regression, formal solver proofs, lane coverage | cargo test · cargo test --features solver-stable |
Same toolchain; CPU-only (ndarray default). |
| Cargo examples | One-file integration narrative | cargo run --example basic_topology |
Default features unless extended locally. |
| Python / MCP / End-user CLI | Notebooks, robotic agent tools, industrial dataset calibration | Not shipped here — use umst-concrete-cartridge. |
That workspace pins the same Rust 1.88 line for CI alignment. |
To bridge the gap between microscopic physics and macroscopic design, the manifold embeds a suite of high-fidelity, native tensor solvers (src/physics/solvers/). These run directly on Burn's differentiable GPU/CPU graphs.
| Continuous Solver | Governing Physical Equations | Active Crate Module | Spatial / Design Output | Formal Verification Anchor |
|---|---|---|---|---|
| 1. Ionic Electrochemistry | Poisson-Boltzmann-Nernst-Planck (PBNP) | solvers/electrochemistry.rs |
Local multi-species ionic concentration fields ( |
Lean 4 Theorem PBNP_Conserves |
| 2. Photonics / EM Waves | Frequency-Domain Maxwell Curl (FDFD) | solvers/photonics.rs |
Steady-state electric field distribution ( |
Coq Lemma Maxwell_Curl_Nil |
| 3. Phase-Field Fracture | Coupled Elastic Strain Energy & Damage Phase | solvers/fracture_field.rs |
Continuous damage field ( |
Lean 4 Theorem Fracture_Energy_Bounded |
| 4. Acoustics & Vibration | Anisotropic Elastic Wave (Vlasov-Cauchy) | solvers/acoustics.rs |
Dynamic spatial sound pressure displacement ( |
Coq Lemma Wave_Conservation_Invariant |
| 5. Non-Newtonian Flow | Herschel-Bulkley Viscoplastic Fluid Yield | solvers/rheology_flow.rs |
Yield stress front velocity vectors ( |
Lean 4 Theorem Bingham_Flow_Stable |
| 6. Coupled THMC Residual | Jacobian-Free Newton-Krylov Matrix-Free GMRES | solvers/thmc.rs & solvers/thmc_residual.rs |
Interlinked heat ( |
Coq Lemma JFNK_THMC_Residual_Bounded |
1. Multi-Species Ionic Electrochemistry (Nernst-Planck-Poisson)
-
Physical Concept: Durability in porous structures depends on how ions (like dissolved chloride salts) move through water-filled pores. The solver calculates this movement by tracking chemical concentration gradients, fluid velocities, and microscopic electric fields.
-
Exact Tensor Formulation: Solves the coupled Poisson-Boltzmann-Nernst-Planck (PBNP) system:
Where
is ion concentration, is diffusivity, is valence, is the electrostatic potential, and is pore fluid velocity.
2. Electromagnetic & Radiative Transport (Photonics FDFD)
-
Physical Concept: Active thermal management requires tracking how light, radiation, and heat propagate through heterogeneous material grains. The solver calculates this by simulating how high-frequency electromagnetic waves scatter, absorb, or reflect inside the microstructure.
-
Exact Tensor Formulation: Implements a Finite-Difference Frequency-Domain (FDFD) formulation of Maxwell’s curl equations:
Where
is the electric field tensor, is complex relative permittivity, and is the free-space wavenumber.
3. Coupled Phase-Field Fracture (Cracking Dynamics)
-
Physical Concept: Cracks do not just appear; they grow by minimizing the structural energy. The solver tracks cracking by introducing a continuous damage field (
) where is solid material and is a fully broken crack, avoiding the need to track complex individual crack edges. -
Exact Tensor Formulation: Solves the coupled mechanical displacement and crack phase-field equations:
Where
is critical energy release rate, is the length scale of crack width, and is the history variable of tensile strain energy density.
4. Anisotropic Acoustics & Wave Dynamics (Sound Propagation)
-
Physical Concept: Mechanical noise, vibrations, and shock waves travel differently depending on the grain orientation of a structure. The solver simulates how acoustic waves travel and dissolve within anisotropic media.
-
Exact Tensor Formulation: Solves the dynamic elastic wave equation:
Where
is displacement, is local density, and is the 4th-order anisotropic stiffness tensor.
5. Non-Newtonian Extrusion Rheology (Herschel-Bulkley Flows)
-
Physical Concept: During fabrication processes like 3D printing, the wet material must flow through a nozzle but stay rigid once deposited. The solver tracks this transition by modeling the material as a fluid that only flows when pushed beyond a specific "yield stress."
-
Exact Tensor Formulation: Solves Herschel-Bulkley fluid dynamics where effective viscosity
scales with shear rate :Where
is yield stress, is consistency index, and is the flow behavior index.
6. Coupled Jacobian-Free Newton-Krylov (JFNK) THMC Solver (Multi-Physics Convergence)
-
Physical Concept: Temperature, water pressure, mechanical load, and chemical hydration react to each other simultaneously. Instead of calculating them one by one (which leads to errors), the solver groups them into a single continuous equation and balances them together in an iterative loop.
-
Exact Tensor Formulation: Implements a fully coupled residual function
solved via a Jacobian-Free Newton-Krylov solver (thmc_residual.rs/krylov_host.rs):Enabling matrix-free GMRES iterations to reach full coupled Thermo-Hydro-Mechanical-Chemical convergence without computing or storing large Jacobian matrices.
If you are an application engineer, architect, or data scientist looking for Python bindings, MCP servers, or JSON/CSV contracts, the deployed engine lives in the UMST Concrete Cartridge repository.
If you are building atop the Manifold, here is the technical deployment reference:
Commands, Cargo features, and agent checklist
cd umst-manifold
cargo build
cargo test- Solver integration tests:
cargo test --features solver-tests(same feature graph assolver-experimental). - Gate HTTP shim (
gate_server):cargo test -p umst-manifold --features gate-server-bin --test gate_server_http(also builds the--bin gate_servertarget via the same flag;gate-serverforwards togate-server-bin). - GPU (
wgpu): The optionalwgpufeature is not part of the default CI matrix; CPU builds withndarrayare the portable reference path. On Apple Silicon,mac-fast(ndarray+blas-accelerate) is the supported high-throughput local configuration.
We group solvers into explicit feature lanes to manage compile times and dependencies.
| Feature | Purpose |
|---|---|
ndarray (default) |
CPU tensors via burn-ndarray. |
blas-accelerate |
vecLib/Accelerate-backed matmul on macOS (forwarded to burn-ndarray). |
mac-fast |
ndarray + blas-accelerate convenience bundle. |
solver-stable, solver-research, solver-experimental, solver-tests |
Solver lane umbrellas. |
| Granular solver flags | fracture-at2, acoustics-newmark, thmc-coupled, electrochemistry-pnp, mechanics-adjoint — single kernel pulls in Cargo.toml. |
gate-server-bin (+ alias gate-server) |
Enables cargo run … --bin gate_server (POST /gate JSON); Powers/Parrott mix gate lives in crate::gate::http_manifest. |
manifest-bridge |
Downstream hook for cartridges re-exporting umst_manifold::manifest::* (declare-only; verify on sibling cartridge). |
manifold-manifest |
Typed manifest façade (UmstManifest, catalog hash advisory). |
manifold-gate |
Transition gate trait surface for host/cartridge parity (pairs with manifest-bridge on concrete). |
From the crate root, gate parity and optional Lean export digest checks:
bash scripts/verify_umst_stack.sh
export UMST_REQUIRE_FORMAL_EXPORT=1 # fail if umst-formal-double-slit export missing
bash scripts/verify_umst_stack.shMonorepo layout: sibling ../umst-formal-double-slit or UMST_FORMAL_ROOT. Full command matrix: docs/VERIFY.md. Workspace root shortcut: VERIFY.md (multi-repo workspace).
- Repo root: treat the checkout directory of this repository as the working root for all
cargo/python3commands. - Safe, no-GPU commands:
cargo build,cargo test,cargo test --features solver-stable,cargo run --example basic_topology,python3 scripts/check_solver_status.py --check-paths --check-memo-links --check-statmech-verification-set. - Before editing: scan
docs/Solver-Status.mdand runcheck_solver_status.pybefore changing solver feature tables or#[cfg(feature = "...")]blocks.
We maintain strict formal proof anchors (formal_status) mapping our Rust implementations to Lean/Coq theorems in the umst-formal repository.
- Notation and foundations:
docs/Mathematical-Foundations.md - Solver lanes, verification paths:
docs/Solver-Status.md - Formal proof index:
docs/PROOF-STATUS.md - Developer verify matrix (CI parity):
docs/VERIFY.md - Claims vs proofs ledger (Lean ↔
catalog_id↔ Rust):docs/claims-vs-proofs.md - Formal integration status (module buckets, release witness gaps):
docs/FORMAL_INTEGRATION_STATUS.md - Catalog ↔ Rust coverage audit:
docs/CATALOG_COVERAGE_AUDIT.md - Compositional inference / gateway audit:
docs/CATALOG_COVERAGE_AUDIT.md(catalog ↔ Rust witness coverage) - Release witness ladder:
docs/RELEASE_WITNESS_LADDER.md— philosophy § Proof library · gate law · MI envelope · no Rust axioms - Formal export scope (sibling):
../umst-formal-double-slit/Docs/EXPORT_COVERAGE.md - Two-repo formal alignment (sibling):
../umst-formal-double-slit/Docs/UMST_FORMAL_REPOS_ALIGNMENT.md - Supercap formal scaling (sibling):
../umst-supercap-cartridge/docs/FORMAL_SCALING.md
Production pin: digest 0697014fb5b90a3a… · 119 modules · cross_repo_merge: true — see docs/RELEASE_WITNESS_PROGRESS_VERIFIED.md.
CI catalog lock: digest c61b1bef… · 122 modules — enforced by umst-catalog-drift.yml and catalog_lock_module_count_matches_upstream_export_122 (current unified export after PrimeSpectral fiber).
Historical primary-only pin: digest c1d9ba2aa402… · 69 modules — pre–formal-fiber-merge rollback only (docs/W9_PLAN.md · docs/DUAL_PIN_ARCHITECTURE.md).
The manifold pins the exported Lean inventory from umst-formal-double-slit in artifacts/catalog.lock.json. Digest is enforced at build via build.rs → UMST_CATALOG_LOCK_SHA256_HEX. Canonical export: umst-formal-double-slit/artifacts/catalog.json (make lean-catalog-export). Override at build: UMST_CATALOG=/path/to/lock.json. Handoffs: docs/AGENT_STATUS.md.
This repository is one component of a four-repo material-science stack. The sections below describe the ecosystem an AI assistant or autonomous agent should know about, and the operating contract for interacting with this manifold.
Four active repositories make up the stack:
umst-manifold(This Repository): Exposes the core Discrete Exterior Calculus (DEC) primal grid, the differentiable Burn tensor graph, and the high-fidelity continuous solvers.umst-concrete-cartridge: The applied engineering interface exposing Python/PyO3 bindings, headless MCP tools, and 26 chemical-physical closures (e.g. hydration kinetics, viscoelastic creep).umst-formal: The formal mathematical verification database holding the Lean 4 & Coq proof anchors for the cement gate fiber. This repository mathematically proves that the DEC cochain complexes satisfy exact conservation laws ( ).umst-formal-double-slit: The quantum-information proof suite (Lean 4 + Mathlib). Machine-checked proofs of the Landauer cost of measurement, the Englert visibility / which-path bound, Lindblad dephasing limits, and Klein relative-entropy nonnegativity — anchoring the manifold's Thermodynamic CBF in formally verified quantum-mechanical foundations.
- No statistical interpolation of physics. Material stress, deformation, and hydration states come from the solvers — not from heuristics or regression.
- Second law + composition are non-negotiable. Treat every integration step as subject to the same entropy-balance and admissibility story as in §1.4: compose operators, do not stack hacks that bypass the gate.
- Use the exact gradients. Query
AdjointNeuralODE(src/ai/adjoint.rs) for -memory backpropagation; run the continuous solvers for state profiles. - Validate against proof anchors. Any solver-kernel change is checked against
docs/PROOF-STATUS.mdviacheck_solver_status.py.
- Local Execution: Run
cargo test --workspaceor execute single examples likecargo run --example basic_topologyto verify changes. - Out-of-Process Scaling: Use the Model Context Protocol (MCP) server inside
umst-mcpto stream physical voxel states to remote compute over WebSockets. Remote deployments today assume the same CPUndarrayexecution path as CI unless you explicitly enable and validate optional GPU features locally.
Design and solver edits read cleaner when held to three principles:
- Continuity of flow (category & graph theory). Treat physical equations as composed, not patched. Every structural change moves along a continuous pathway in the graph; the gradient stays connected end-to-end.
- Physics-as-types (type theory). Conservation laws and material limits act as structural types. A design that violates
or the entropy gate fails at the type level, not as a runtime exception. - Information cost (information theory & MI). Each design change is an informational change with a Landauer cost. Use mutual information
as the metric for whether a proposed design stays inside the physically admissible envelope.
The four repos form a closed loop: the manifold supplies conservation laws and gating, applied cartridges supply domain chemistry and operational tools, the formal repos anchor the invariants.
New physical domains plug in by implementing IScienceCartridge — no manifold changes required. A cartridge (aerospace metals, smart polymers, acoustic metamaterials) inherits the DEC grid, thermodynamic CBF checkpoints, and the on-device mutual-information observer for free:
- Conservation by construction, not by tuning. Mapping physics onto a discrete exterior calculus complex makes the boundary-of-a-boundary identity (
) a structural property of the data, not a convergence target. Drift that traditional FEM accumulates over long simulations is algebraically absent here. - A single 64-lane UMST carrier is enough. Thermal, mechanical, chemical, and informational variables co-resolve in one tensor pass instead of brittle staggered couplings. The downstream gain is gradient continuity end-to-end, which is what makes the adjoint loop tractable on commodity CPUs.
- Safety as a runtime gate, not a post-hoc audit. The Clausius–Duhem inequality and Landauer cost are evaluated before a state transition commits. A policy that violates them does not produce a logged warning; it does not produce a state at all.
- Formal anchoring closes the loop. Each solver carries a Lean 4 / Coq theorem reference in
docs/PROOF-STATUS.md, so a kernel change is invalid until the corresponding proof obligation is discharged inumst-formal.
- Architects can author a physics substrate. Discrete Exterior Calculus has a reputation as a graduate-numerical-analysis specialty. It isn't. Once you stop fighting tensor-index notation and start thinking in cochains, the manifold reads like a parametric modifier graph — the same mental model architects already use. Two architects wrote and trained the kernel.
- Rust was the discipline we needed, not the speed. Earlier prototypes in Python and JAX leaked gradients silently through monkey-patched operators; nothing alerted us until convergence quietly stopped meaning what we thought. Moving to Burn + Rust forced every kernel to declare its differentiability contract at the type level. Most of the reliability we ship is downstream of compiler-checked variance and DEC admissibility, not algorithmic novelty.
- The hard part was orchestration, not the math. 25 engines coexisting under
IScienceCartridgeonly works because solver composition is a fold over a typed step graph, not a chain of side-effects. The largest single kernel diff of 2025 wasn't a new solver — it was rewriting orchestration. - The CBF earned its keep as semantics, not certification. Adding the thermodynamic gate to the runtime — rather than only to a post-hoc proof — changed what the program does, which proved more valuable than what it can prove. Rejected transitions don't become logged warnings; they cease to exist as state.
- Formal proofs anchor; they do not block. Lean obligations live in
umst-formaland document the kernel's invariants. Day-to-day kernel work doesn't wait on a Lean discharge — but the moment a kernel change breaks a proven invariant, the next CI run catches it. Anchor, not gate, turned out to be the productive pattern.
The manifold is a substrate. Its value shows up in what gets built on top of it.
- UMST Concrete Cartridge — applied cementitious physics mounted on this manifold
- UMST-UCRS — Universal Calendar Resolution Spine; constitutional time and
UcrsObservedAtstamps on durable logs - UMST Supercap Cartridge — structural supercap electrochemistry cartridge (monorepo sibling)
- UMST Formal — Lean 4 / Coq proof anchors for the conservation laws
- UMST Formal Double-Slit — quantum-information proofs anchoring the Thermodynamic CBF
Development processes and safety guidelines are maintained in CONTRIBUTING.md, CODE_OF_CONDUCT.md, and SECURITY.md.
Released under the MIT License. © 2026 Santhosh Shyamsundar, Santosh Prabhu Shenbagamoorthy — Studio TYTO.

