Safe infinite-recursive tables in Tau Language

TABA tables are designed as infinite updateable objects: one symbolic rule, revised a region at a time. Most of that language is still out of reach for execution. This tutorial walks through the fragment that is safe to run today.

“Safe” is the load-bearing word. The fragment implements pointwise revision under a Kleene-style recurrence whose update has been proved monotone and omega-continuous, so the supremum of its finite approximants really is a fixed point. The fragment deliberately excludes everything that could break that proof: same-stratum prime, current-state-dependent guards, unrestricted recursive common, full NSO, and full Guarded Successor.

Current status

Four objects carry the evidence here. Each one stands on its own, and they do not combine into a single claim:

• The Tau demo runs a feature-gated safe table surface behind TAU_ENABLE_SAFE_TABLES=1.
• The semantic proof artifact establishes the safe recursive update shape over a completed Boolean-algebra setting.
• The finite CBF and priority-table proofs collapse finite table syntax down to ordinary Boolean-function terms and explicit minterm trees with $2^n$ leaves.
• The lowering proof establishes that the safe priority-table source layer and pointwise revision lower into a Tau-helper IR without changing denotation.

The current evidence supports this formula:

Standard reading. If the finite Tau demo runs, the safe-recursive proof artifact holds, the finite CBF evidence holds, and the lowering evidence holds, then the supported conclusion is a runnable safe table fragment.

Plain English. Each conjunct is a separate artifact, and each one has been checked. Together they support a runnable safe table fragment whose safe source layer has a checked helper-IR lowering. They do not support unrestricted TABA.

The table update

Think of a table state as a function:

Standard reading. The symbol $s$ is a function from table keys in $I$ to Boolean-algebra values in $\alpha$.

Plain English. A table assigns one Boolean region to each key.

Trap. This is not a spreadsheet cell containing an ordinary number. The value $s(i)$ is a Boolean-algebra element, so it can be joined, met, split, complemented, and compared by the Boolean order.

The safe table body denotes an update function:

Standard reading. $U_T$ maps a current table state to the next table state.

Plain English. One table-update pass computes every next entry from the current entries and fixed lower-stratum data.

Trap. The update may read the current recursive state only positively. It may not use same-stratum prime or current-state-dependent guards. Those forms can break monotonicity.

The safe operations

The first safe operation is fixed-guard selection:

Standard reading. $\mathrm{select}_G(x)$ is defined as the meet of the fixed guard $G$ and the value $x$.

Plain English. Keep the part of $x$ that lies under $G$, and remove the rest.

Trap. This is not arbitrary selection by any predicate. The predicate is specifically a fixed Boolean-algebra guard. The checked boundary proof gives a counterexample for arbitrary value-predicate selection.

The second safe operation is fixed-guard revision:

Standard reading. Inside $G$, use replacement value $a$. Inside $G^{\prime}$, use the old value $x$. Then join the two regions.

Plain English. Overwrite the guarded region and leave everything outside the guard unchanged.

Trap. The prime in $G^{\prime}$ is the Boolean-algebra prime of the lower-stratum guard. It is allowed here because $G$ is fixed relative to the current recurrence. This is not permission to use $x^{\prime}$ on the same recursive stratum.

The table-level implementation law is pointwise revision:

Standard reading. For every table key $i$, $\operatorname{Rev}_{G,A}(T)(i)$ is obtained by using replacement entry $A(i)$ inside guard entry $G(i)$, and using old entry $T(i)$ inside $G(i)^{\prime}$.

Plain English. Revise each table entry locally: replace the guarded part and preserve the rest.

Trap. This is pointwise over keys. It does not mean the runtime stores infinitely many concrete cells. It means the runtime stores a finite symbolic rule whose denotation can be read at any key.

Visualize the update

Before the recurrence formulas get abstract, the visualizer below shows one pointwise revision step at a time, over four sampled regions. Every row is a sampled region; the symbolic table is the rule behind the rows.

The visualizer is meant to connect four ideas at once:

• A table entry is a Boolean region, not a scalar cell.
• Fixed-guard revision updates only the part selected by $G(i)$.
• Atomlessness says every live nonzero region can be split again, so there is no final smallest live cell.
• In the NSO picture, formulas themselves denote Boolean-algebra values, so a sentence can act as a guard or splitter in the semantic model.

Trap. This is a teaching model. It does not implement full NSO, unrestricted recurrence, or full TABA tables. It shows only the safe pointwise update shape and the mental picture behind atomless splitting.

The recurrence meaning

The recurrence starts from bottom and advances one update at a time:

Standard reading. The zeroth approximant $s_0$ is the bottom table state, and the next approximant $s_{n+1}$ is obtained by applying the update function $U_T$ to the current approximant $s_n$.

Plain English. Start with the empty table meaning. Each step applies one safe table-update pass to the previous approximant.

For this sequence to converge to something that deserves to be called a fixed point, two properties of $\operatorname{Rev}_{G,A}$ need to hold. The first says the approximants stay ordered:

Standard reading. If table $T$ is pointwise below table $U$, then revising $T$ with fixed guard $G$ and fixed replacement $A$ is pointwise below revising $U$ with the same $G$ and $A$.

Plain English. Pointwise revision is monotone. If $T$ is pointwise below $U$, revising $T$ lands pointwise below revising $U$.

The second says the limit passes through the update:

Standard reading. For an increasing omega-chain of tables $T_n$, revision of the countable join equals the countable join of the revised tables.

Plain English. Pointwise revision commutes with the infinite join. Revising first and then taking the supremum gives the same table as taking the supremum first and then revising.

Together, monotonicity and omega-continuity let the approximants close up. The infinite-recursive meaning is the supremum:

Standard reading. The value $\mu U_T$ is defined as the countable join of all approximants $s_n$ for natural numbers $n < \omega$.

Plain English. The limit collects everything that appears at any finite stage: the countable join of all approximants.

Trap. This is where finite clopens alone are not enough in the general case. A finite executable carrier, meaning a concrete runtime representation with finitely many visible cells, can run examples and stabilized fragments. The full semantic statement needs a completed Boolean-algebra reference layer, meaning a mathematical universe where the countable join is defined.

The checked fixed-point proof artifact is:

Standard reading. Applying the update to the recursively defined value $\mu U_T$ returns $\mu U_T$ again.

Plain English. The limit is stable under one more update.

What Tau runs

The public reproduction path now lives in the TauLang-Experiments repo.

The smooth public demo command is:

./scripts/run_public_demos.sh --accept-tau-license

That command runs the safe table demo and the qelim-backed policy-shape demo. To run only the safe table syntax and solver-equivalence demo, use:

./scripts/run_table_demos.sh --accept-tau-license

That repo does not redistribute Tau Language. The scripts download Tau from the official IDNI repository, check out the tested commit, apply the experiment patch locally, regenerate Tau’s parser, build Tau, and run the demos. The default runner uses the compound equivalence check for the table-vs-raw obligations. The older one-check-at-a-time audit path is still available with TABLE_DEMO_EQUIV_MODE=individual. There is also an audit-friendly batched path with TABLE_DEMO_EQUIV_MODE=batched, which keeps one solver result per obligation while running the checks in one Tau process.

The latest smooth run used TABLE_DEMO_EQUIV_MODE=compound, checked the fifteen table-vs-raw mismatch obligations as one compound query, and passed. The compound-equivalence step took 54939.340 ms on that local check. This timing is descriptive, not a cross-machine performance claim.

The latest batched audit run checked the same fifteen obligations, returned fifteen no solution results, reduced Tau process count from 15 to 1, and reduced elapsed time by about 50.877% against the separate-process audit path. It also exercised the opt-in command-file path behind TAU_CLI_FILE_MODE=1. This is a demo-harness optimization, not a solver speedup claim.

There is also a newer internal solver-path experiment: TAU_RR_SKIP_VALUE_INFER=1. It skips a redundant second type-inference pass for non-spec, ref-valued command arguments that already passed parser-time type inference. On the current safe-table solver corpus, the three-repetition local receipt preserved all checked no solution results, reduced internal solve-command time by 76.963%, and reduced measured get_rr time by 97.804%. The same receipt did not improve whole-process elapsed time, because the wrapper still spends most of its wall-clock time launching Tau processes and loading sources. This is an opt-in internal optimization candidate, not a default Tau behavior. A separate audit run also checked that all five skipped RR branches were structurally equal to the full-inference branch. In the batched one-process table-check path, the same shortcut passed all fifteen obligations, reduced measured get_rr time by 99.266%, reduced internal solve-command time by 75.435%, and reduced wall-clock elapsed time by 3.186% on the local demo corpus.

A separate ordinary reference-definition corpus checks the same shortcut without safe-table syntax. It uses nine named :tau definition cases, including commutativity, absorption, double prime, De Morgan laws, and guarded choice. The local receipt passed all nine cases, checked nine structurally equal audit rows, reduced measured get_rr time by 79.109%, and reduced internal solve-command time by 55.564%. This is broader evidence for the shortcut, but it is still a synthetic corpus, not a default Tau optimization claim.

Two later internal RR experiments target the formula-application path left after that shortcut. TAU_RR_TRANSFORM_DEFS_CACHE=1 caches transformed definition lists inside one Tau process. With the RR skip held fixed, the batched local receipt saw 14 cache hits over 15 formula applications, reduced RR formula-transform time by 91.860%, and reduced internal solve-command time by 35.339%. TAU_RR_ACTIVE_RULES=1 then filters the rewrite rules by the reference signatures currently visible in the term. With both earlier RR flags held fixed, the three-repetition batched receipt skipped 6570 of 6750 candidate rule applications, reduced RR formula-rewrite time by 88.821%, reduced internal solve-command time by 73.402%, and reduced whole-process elapsed time by 3.625%. These are internal-path optimization candidates. They are not default Tau behavior, because the active-rule filter still needs a proof or code invariant for the delayed rewrite schedule. The audit flag TAU_RR_ACTIVE_RULES_AUDIT=1 checks the final active repeated-rewrite result against the full repeated-rewrite result. The current batched audit has 15 / 15 structurally equal rows.

The public demo checks:

• safe symbolic table update idempotence,
• finite four-cell carrier update behavior,
• finite-carrier pointwise revision behavior,
• Tau-native table syntax equals the raw guarded-choice expansion,
• a protocol-firewall priority table equals its raw expansion,
• priority slices prove that earlier rows win when guards overlap,
• a collateral-admission reason table returns the first failed reason,
• an incident-memory table applies state-transforming rows correctly,
• pointwise revision preserves old values outside the guard,
• pointwise revision uses replacement values inside the guard,
• pointwise revision is idempotent for the same guard and replacement,
• table syntax is rejected when TAU_ENABLE_SAFE_TABLES is absent.

The visible breakthroughs are:

• parser-level table syntax, not just JSON-side lowering,
• a raw-formula equivalence check, not just a successful parse,
• compound mismatch checking, where one unsatisfiable disjunction proves all table-vs-raw checks at once,
• an opt-in RR extraction shortcut that removes a redundant inference pass on the checked safe-table solver corpus,
• priority-table behavior with overlapping guards,
• explanation-carrying table rows, not just admit-or-deny formulas,
• state-transforming rows that read the old symbolic state positively,
• pointwise revision as an explicit table-update law,
• feature-flag rejection when the syntax is not enabled,
• official-Tau download plus local patching, rather than redistribution of a modified Tau fork.

The standalone demo gallery is documented in docs/demo-gallery.md.

The compound check uses this proof obligation:

Standard reading. If the disjunction of all mismatch predicates has no satisfying assignment, then every individual mismatch predicate has no satisfying assignment.

Plain English. Instead of asking Tau to restart and check each table-vs-raw mismatch separately, the demo asks one larger question: does any mismatch exist? If the answer is no, all checked table equivalences pass.

Boundary. This is an optimization of the demo proof obligation. It does not add a new table operator, and it does not prove unrestricted TABA tables.

The Tau experiment uses the feature flag:

TAU_ENABLE_SAFE_TABLES=1

In TauLang-Experiments, the example file is:

examples/tau/safe_table_kernel_builtins_v1.tau

The runtime prelude exposes these finite-carrier helpers:

st_select4(x,g)
st_choice4(g,then_value,else_value)
st_revise4(old,g,replacement)
st_update4(old,base,g,replacement)

It also exposes symbolic tau helpers:

st_select_tau(x,g)
st_choice_tau(g,then_value,else_value)
st_revise_tau(x,g,a)
st_update_tau(x,b,g,a)

The symbolic helpers are closer to the infinite-recursive semantic target than the four-cell demo helpers. They operate over Tau’s symbolic Boolean-algebra type, not merely over the finite ft4 carrier.

The executable update is:

Standard reading. The next value is the join of a fixed base value and the fixed-guard revision of the current value.

Plain English. Keep the required base cells, then apply the guarded overwrite.

The Tau example checks that one more update does not change the result for this particular update shape:

Standard reading. Applying $U$ twice gives the same value as applying $U$ once.

Plain English. This concrete update stabilizes after one Tau step.

Trap. This one-step stabilization is a property of this example update shape. It is not a theorem that every safe table recurrence stabilizes after one step.

Replay the finite-carrier trace from the TauLang-Experiments repo root:

python3 scripts/generate_safe_table_tau_artifacts.py

The generated proof report is:

assets/data/safe_table_tau_traces.json

Replay the symbolic tau solver checks from the TauLang-Experiments repo root:

python3 scripts/generate_safe_symbolic_tau_artifacts.py

The generated symbolic proof report is:

assets/data/safe_symbolic_tau_traces.json

Demo: source table compiler

The next demo starts from a small source table AST in TauLang-Experiments:

examples/tau/safe_table_source_examples.json

The compiler emits two expressions:

• the raw Boolean-algebra denotation of the source table,
• the Tau-helper expression using st_choice_tau, st_select_tau, and st_revise_tau.

It then asks Tau whether the two expressions can differ. The expected answer is no solution.

Replay it from the TauLang-Experiments repo root:

python3 scripts/generate_safe_table_compiler_artifacts.py

The generated proof report is:

assets/data/safe_table_compiler_tau_traces.json

This is still useful as a compiler-smoke test, but it is no longer the main Tau native demo. It starts from JSON, so it checks the semantic lowering shape outside Tau’s parser.

The corresponding Lean theorem is:

Standard reading. For a safe key-indexed table program $P$, evaluating the compiled Tau-helper program gives the same Boolean-algebra value as evaluating the source table program.

Plain English. The JSON compiler demo is backed by a checked denotational theorem: the helper IR has the same meaning as the safe source table.

Trap. This proves the semantic compiler contract for the helper IR. It is still not a proof of Tau’s C++ parser, Tau’s full runtime, unrestricted recurrence, full NSO, or Guarded Successor.

Demo: Tau-native table syntax

The next demo uses Tau’s own parser. In TauLang-Experiments, the feature-gated source file is:

examples/tau/full_style_taba_demo_v1.tau

It includes:

• a parser-level table form,
• priority rows through row order,
• CBF-style conditional values through nested guarded table choice,
• safe fixed-guard select,
• safe fixed-guard revision.

The syntax is:

table {
  when G1 => V1;
  when G2 => V2;
  else => D
}

The parser production is guarded by TAU_ENABLE_SAFE_TABLES=1. Without that feature flag, the table syntax is rejected. The replay also runs Tau with --charvar false, so a name like riskgate is one variable rather than a product of character variables.

Replay it from the TauLang-Experiments repo root:

python3 scripts/generate_full_style_taba_demo_artifacts.py

The generated proof report is:

assets/data/full_style_taba_demo_traces.json

The same check is the centerpiece of the standalone experiment repo. Its public-facing equation is:

Standard reading. The Tau-native table { when ... else ... } definition is parsed, lowered to nested guarded choice, and checked against an explicit raw Boolean-algebra denotation. Tau is asked whether the two denotations can differ. The expected answer is no solution.

Plain English. Tau itself now accepts the safe table syntax when the feature flag is on, and the checked symbolic query confirms the parsed table means the same thing as the expanded formula. The syntax is not just accepted; it is checked.

Trap. This is a syntax-and-lowering breakthrough for safe guarded choice. The table form is safe guarded choice only: it does not add unrestricted recurrence, same-stratum prime, NSO, or Guarded Successor to Tau, and it is not a claim that the official full TABA table language has been implemented.

New proof bridge: finite minterms

The latest proof does not finish full TABA tables, but it removes one local assumption from the Skolem/minterm side of the search.

First define guarded choice:

Standard reading. $C_g(a,b)$ is the join of the part of $a$ under guard $g$ and the part of $b$ under the prime of $g$.

Plain English. Use $a$ inside $g$, and use $b$ outside $g$.

Trap. This is a Boolean-algebra merge. It is not a procedural if-statement in a program, and $g^{\prime}$ is the Boolean prime of the guard.

For two variables $x$ and $y$, a four-coefficient minterm form is:

The same expression expands to:

Standard reading. The value of $M_{\vec a}(x,y)$ is the join of four guarded coefficients, one for each truth corner of $x$ and $y$.

Plain English. The formula splits the Boolean space into the four cases $(x,y)=(1,1),(1,0),(0,1),(0,0)$, assigns one coefficient to each case, and joins the four guarded pieces.

The checked compiler theorem is:

Standard reading. Every binary Boolean-polynomial term $t$ built from constants, $x$, $y$, meet, join, and prime has a four-coefficient minterm representation with the same denotation for every $x$ and $y$.

Plain English. For this binary term fragment, the proof assistant can compile the expression into a complete four-case table without changing its meaning.

The next checked step generalizes the compiler from two variables to any finite number of variables. Instead of four coefficients, the target is a full minterm tree:

It also proves:

Standard reading. For every finite arity $n$, every Boolean-polynomial term over variables indexed by $\mathrm{Fin}(n)$ compiles to a minterm tree with the same denotation under every assignment $\rho$, and that tree has $2^n$ leaves.

Plain English. The proof is no longer limited to four cases. With $n$ Boolean variables, it builds the $2^n$-case table and proves that the table means the same thing as the original expression.

Trap. This is still Boolean-polynomial syntax. It does not prove full quantifier elimination, full NSO, full recurrence, full TABA table syntax, or Tau runtime lowering.

New proof bridge: CBF and table collapse

The next proof checks a larger syntax layer. It adds CBF-style conditionals and priority table rows, then proves that this finite Boolean-valued syntax can be collapsed back into an ordinary Boolean-function term.

The key constructor is still guarded choice:

Standard reading. $C_g(t,e)$ is the join of $t$ met with guard $g$ and $e$ met with the prime of $g$.

Plain English. Inside the guard, keep the then-branch. Outside the guard, keep the else-branch. Then join the two disjoint pieces.

Trap. This is not an operational if-statement. It is a Boolean-algebra identity. The word “then” is only a reading aid for the guarded split.

For a CBF expression $c$, the compiler theorem is:

Standard reading. For every finite-arity CBF expression $c$ and every assignment $\rho$, the ordinary Boolean-function term produced by $\operatorname{cbfToBF}$ has the same denotation as $c$.

Plain English. The conditional syntax does not add a new meaning layer in this fragment. It can be expanded into ordinary Boolean meet, join, and prime without changing what it denotes.

For a priority table $T$, the table compiler theorem is:

Standard reading. For every finite-arity priority table $T$ and every assignment $\rho$, the Boolean-function term produced by $\operatorname{tableToBF}$ has the same denotation as the table.

Plain English. A finite priority table with CBF-style values can be compiled into one ordinary Boolean formula, and the proof says the compiled formula means exactly the same thing as the table.

Trap. This is a finite Boolean-valued table result. It does not yet prove first-class NSO, Guarded Successor, unrestricted recurrence, or production Tau lowering.

The next bridge compiles the table all the way to an explicit minterm tree. Define:

The semantic theorem is:

The size theorem is:

Standard reading. For every finite-arity priority table $T$, the compiled minterm tree $m_T$ has the same denotation as $T$ under every assignment $\rho$, and the tree has exactly $2^n$ leaves.

Plain English. The finite table can be expanded into the complete case tree over its $n$ Boolean inputs. No case is missing, and no case changes meaning.

Trap. This is an explicit finite case tree. It is not yet recurrence, NSO, Guarded Successor, or full infinite TABA.

The same proof also marks the unsafe boundary:

Standard reading. For the prime-step function $F(x)=x^{\prime}$, it is not true that every ordered pair $a\le b$ is sent to an ordered pair $F(a)\le F(b)$.

Plain English. Prime reverses order. That is why same-stratum prime cannot be placed inside the monotone least-fixed-point lane.

Trap. This is not merely an implementation limitation. It is a semantic limitation of the monotone proof method.

The certified fallback rule is:

Standard reading. If the resolver returns the result $\operatorname{fixed}(x)$, then $x$ is a fixed point of $F$.

Plain English. When the checker accepts a loop certificate as a fixed point, the reported state really is stable under one more application of the update rule.

Trap. This proves soundness of accepted fixed-point certificates. It does not prove that every recurrence has a certificate, and it does not make nonmonotone recurrence monotone.

Demo: quarantine closure

The app-style demo is a collateral quarantine closure rule. It is intentionally small: four toy assets, with dependency flow:

asset 0 -> asset 1 -> asset 2 -> asset 3

The one-hop dependency operator is written $D$. For a quarantine set $Q_n$ and a newly discovered seed set $\mathrm{Seed}_{n+1}$, the recursive update is:

Standard reading. The next quarantine set is obtained by joining the previous quarantine set with the newly seeded risk set, then applying the dependency-propagation operator $D$.

Plain English. Keep everything already quarantined, add new direct risk, then quarantine every asset reached by one dependency edge.

Trap. This is not a static lookup table. The meaning is recursive because the output $Q_{n+1}$ becomes the next input $Q_n$.

The fixed-point reading is:

Standard reading. $Q_\infty$ is the least fixed point of the function $Q \mapsto D(Q \vee \mathrm{Seed})$.

Plain English. It is the smallest quarantine set closed under the dependency rule.

The Tau demo uses a host loop. The host computes a candidate next state, feeds it to Tau, and Tau checks the claim. This is the same architecture as many production policy engines: the host proposes, the policy checker accepts or rejects.

Replay it from the TauLang-Experiments repo root:

python3 scripts/generate_quarantine_closure_tau_artifacts.py

The generated proof report is:

assets/data/quarantine_closure_tau_traces.json

The demo includes a bad host claim. The expected result is that Tau rejects that step.

Does this prove tables work?

It proves a scoped fragment, not full TABA tables.

The evidence supports this claim:

Standard reading. Given the safe helper definitions, the Tau transition checks, and the Lean semantic proof artifact, the supported conclusion is that a safe recursive table fragment is runnable.

Plain English. The demo has enough evidence to teach and test the safe fragment. It is not enough evidence to claim full official TABA tables are implemented.

What has been proved

The local Lean proof artifacts establish the semantic shape behind the feature:

• v552 proves safe table expressions denote monotone omega-continuous simultaneous updates.
• v553 proves fixed-guard selection and fixed-guard revision are safe, and gives counterexamples for unsafe variants.
• v554 puts safe selection and safe revision into the table grammar itself.
• v555 proves that the safe table grammar lowers into an abstract Tau-helper target language without changing its denotation; the later Aristotle-audited lowering packet rebuilds the same source-to-helper-IR contract for safe priority tables and pointwise revision.
• v556 proves that binary Boolean-polynomial terms compile to four-coefficient minterm form without changing their denotation.
• v557 generalizes the minterm compiler to arbitrary finite arity, using a minterm tree with $2^n$ leaves.
• v558 proves that finite Boolean-valued CBF and priority-table syntax collapses to an ordinary Boolean-function kernel, and proves that same-stratum prime is outside the monotone Kleene lane.
• v559 proves that finite Boolean-valued CBF priority tables compile to explicit minterm trees with $2^n$ leaves and denotation preservation.
• tau_compound_table_check_2026_04_15 proves the finite-list law behind the compound demo check: unsatisfiability of the compound mismatch predicate is equivalent to unsatisfiability of every listed mismatch predicate.

The research log keeps the detailed evidence ladder:

Read the detailed research log

What has not been proved

The current feature does not include:

• unrestricted same-stratum prime,
• current-state-dependent row guards,
• arbitrary value-predicate selection,
• unrestricted recursive common,
• full NSO syntax,
• full Guarded Successor syntax,
• full official TABA table semantics,
• a flat packed Fin (2^n) Skolem/minterm coefficient vector,
• production parser and runtime lowering correctness for the whole Tau feature.

Route to full TABA

The target is clearer now. Full TABA cannot live in a single unrestricted least-fixed-point universe. It needs a split semantic architecture, one lane for each kind of recurrence:

Standard reading. An expression $e$ receives least-fixed-point semantics when it belongs to the monotone fragment $\mathcal L_{\mathrm{mono}}$. It receives certified resolver semantics when it belongs to the certificate fragment $\mathcal L_{\mathrm{cert}}$. Otherwise it is rejected.

Plain English. Safe recursive expressions use the monotone fixed-point rule. Nonmonotone expressions need a checked certificate path. Expressions that fit neither path do not get silently accepted.

Trap. This is the feasibility shape, not a finished implementation of full TABA. The proof stack still has to connect the official language to each lane.

To claim full TABA tables, these pieces still need to line up:

• official table, CBF, NSO, recurrence, and Guarded Successor syntax,
• a compiler from that syntax into a checked semantic kernel,
• a monotone lane for safe recurrence, plus a certificate lane for nonmonotone recurrence,
• an executable representation of the carrier or a verified lowering into Tau’s runtime primitives,
• demos that exercise the official syntax path rather than only hand-written helper expressions.

The current work has checked meaningful pieces of that ladder. It has not closed the ladder.

This boundary is not a weakness of the tutorial. It is the point. The safe fragment earns its usefulness by making both sides of the line explicit: why the included forms work, and why each excluded form would break the proof.