Decidable Medical Machines Lab

One calculator, one kidney workflow, five equivalent views.

The left side behaves like a small machine. The right side keeps the math, logic, decision-tree, finite-state, and Tau views aligned. The calorie lane fits directly inside bounded integer arithmetic. The kidney lane uses the official adult eGFR equation in host-side computation, then passes a bounded flag surface into a Tau-shaped follow-up gate.

Max calorie deficit as a total arithmetic function

This lane keeps the machine tiny: read two inputs, compute one derived quantity, then check whether a claimed result matches the formula exactly.

Formula, logic, tree, machine, Tau

The notation changes, but the object does not. This panel shows the same bounded decision shape through several lenses at once.

These cards come from real local Tau runs. They are evidence that the public teaching specs execute and return the expected bounded verdicts.