Bounded game tables in Tau Language

This tutorial is about a Tau Language enhancement experiment: bounded game tables.

The proposed feature is not “Tau solves all of game theory.” The proposed feature is smaller and more useful: Tau gets a table-shaped way to classify a finite strategic surface, and the table lowers to ordinary Tau guarded-choice terms.

The Tau enhancement

The enhancement is a table expression:

post_agi_tokenomics_table(
  contribute,extract,exit,reward,tax,quarantine,
  safe_nash,unsafe_extract,nash_but_not_desired,not_nash,invalid_profile
) : tau :=
  table {
    when profile_contribute_reward(...) => safe_nash;
    when profile_extract_reward(...) => unsafe_extract;
    when profile_contribute_tax(...) => nash_but_not_desired;
    else => invalid_profile
  }.

This is the Tau-language object the tutorial is about.

The table is not magic. It is compiled to a raw guarded-choice expression:

Standard reading. The table expression with ordered guards $G_1,\ldots,G_n$, row values $A_1,\ldots,A_n$, and default value $D$ is equivalent to the nested guarded-choice expression that selects the first matching row and otherwise selects $D$.

Plain English. Earlier rows win. If no row guard holds, the default value is used.

Trap. This is ordered priority-table semantics, not an unordered set of cases. If two guards overlap, the earlier row controls the overlapping region.

The patched Tau demo checks:

solve --tau (post_agi_tokenomics_table(...) != post_agi_tokenomics_raw(...))

The result is:

no solution

That means Tau cannot find an assignment where the table form and the raw guarded-choice form differ.

How to run it

There are two runnable layers, and they should not be confused.

The main Tau-native layer lives in:

TauLang-Experiments

The public reproduction path is:

git clone https://github.com/TheDarkLightX/TauLang-Experiments.git
cd TauLang-Experiments
./scripts/run_game_table_demo.sh --accept-tau-license

That command downloads official Tau Language from the IDNI repository, applies the community research patches locally, regenerates Tau’s parser, builds Tau, enables TAU_ENABLE_SAFE_TABLES=1, and runs the game-table equivalence check.

Inside an existing checkout, run:

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

The fast fallback layer in this site uses ordinary Tau with no patch:

examples/tau/post_agi_tokenomics_game_gate_v1.tau

Generate the checked trace with:

python3 scripts/generate_game_table_tau_artifacts.py

The generated artifact is:

assets/data/game_table_tau_traces.json

The current trace reports:

profiles checked:                 9
profiles after pruning:           3
safe profile:                     contribute/reward
Tau output matches Python model:  true
finite checker proof:             builds

The fallback exists for speed and pedagogy. It is not the feature. The feature is the Tau-native table syntax in the patch repo.

What the table classifies

The demo classifies a bounded listed game. A bounded listed game contains:

• a finite list of players,
• a finite list of candidate profiles,
• for each player and profile, a finite list of unilateral deviations,
• an admissibility predicate,
• a payoff function.

The best-response predicate is:

Standard reading. The best-response predicate for player $i$ and profile $p$ holds exactly when every listed unilateral deviation $q$ from $p$ has this property: if $q$ is allowed, then player $i$’s payoff at $q$ is less than or equal to player $i$’s payoff at $p$.

Plain English. Player $i$ has no listed allowed unilateral move from $p$ that improves player $i$’s payoff.

Trap. The word “listed” is part of the theorem. If a deviation is missing from the list, the checker does not infer it.

The Nash predicate is:

Standard reading. The Nash predicate for profile $p$ holds exactly when $p$ is admissible and, for every listed player $i$, the best-response predicate for player $i$ and profile $p$ holds.

Plain English. The profile is allowed, and no listed player has a listed allowed profitable deviation.

The safe target predicate is:

Standard reading. The safe-Nash predicate for profile $p$ holds exactly when $p$ is Nash, $p$ satisfies the safety predicate, and $p$ satisfies the desired-outcome predicate.

Plain English. The profile is strategically stable inside the bounded model, passes the safety gate, and is one of the intended outcomes.

The Tau game gate

The table syntax classifies the symbolic profile surface. The ordinary-Tau fallback checks the same relationships as Boolean flags.

For a profile $p$, the gate computes:

Standard reading. The Tau gate for Nash status at profile $p$ is defined as the conjunction of three predicates: $p$ is well formed, $p$ is allowed, and $p$ is a best response in the finite listed game.

Plain English. Tau accepts the Nash flag only when the profile is well formed, allowed, and a best response in the finite listed game.

The safe profile flag is:

Standard reading. The Tau gate for safe-Nash status at profile $p$ is defined as the conjunction of the Tau Nash gate at $p$ and the desired-outcome predicate at $p$.

Plain English. The profile is accepted as the target outcome only if it is stable and desired.

The profitable-deviation consistency check is:

Standard reading. The consistency predicate for profile $p$ is defined as the disjunction of two claims: there is no profitable-deviation certificate for $p$, or $p$ is not a best response.

Plain English. If there is certified profitable-deviation evidence, the same profile cannot also be accepted as a best response.

Trap. Tau is checking the symbolic classification layer. Payoff enumeration and coverage of the bounded game are separate obligations.

The classification code is:

Standard reading. The classification function sends profile $p$ to code $1$ in the safe-Nash case, code $2$ in the unsafe-extract case, code $3$ in the Nash-but-not-desired case, code $4$ in the allowed-but-not-Nash case, and code $0$ in all remaining cases.

Plain English. The demo turns each bounded profile into one audit label.

The pruning theorem

The optimization law starts with profitable-deviation evidence:

Standard reading. The profitable-deviation predicate for profile $p$ holds exactly when there is a listed player $i$ and a listed unilateral deviation $q$ from $p$ such that $q$ is allowed and player $i$’s payoff at $q$ is strictly greater than player $i$’s payoff at $p$.

Plain English. Some listed player has an allowed move that pays more.

The first pruning theorem is:

Standard reading. The pruning theorem says that profitable-deviation evidence for profile $p$ entails that $p$ is not Nash.

Plain English. A profile with certified profitable-deviation evidence cannot be Nash.

The search-preservation theorem is:

Standard reading. The search-preservation theorem says that the pruned candidate-profile set contains a safe Nash profile exactly when the original candidate-profile set contains a safe Nash profile, under the condition that pruning removes only profiles with profitable-deviation evidence.

Plain English. Removing profiles that cannot be Nash does not remove any safe Nash solution.

Trap. This is not permission to prune by intuition. Each removed profile needs the profitable-deviation certificate.

Verification layer

This tutorial is Tau-first, but the experiment still needs a proof receipt. The proof layer checks the finite search theorem:

Standard reading. The finite-search theorem says that the Boolean checker returns true exactly when there exists a profile $p$ in the listed candidate-profile set $P$ such that $p$ satisfies the safe-Nash predicate for game $g$ together with the declared safety and desired-outcome predicates.

Plain English. The finite checker finds exactly the safe Nash profiles that are present in the finite candidate list.

Boundary. This proof is not the tutorial’s main feature. It is the evidence layer that keeps the Tau enhancement honest.

The post-AGI tokenomics demo

The demo uses one agent action and one protocol action.

Agent actions:

contribute, extract, exit

Protocol actions:

reward, tax, quarantine

The target outcome is:

contribute/reward

The model checks all nine profiles. Six have profitable-deviation evidence and can be pruned. The remaining three are the contribute profiles:

contribute/reward
contribute/tax
contribute/quarantine

Only contribute/reward is both Nash and desired.

What this gives Tau

This is useful because many protocol questions can be reduced to small bounded games:

• Can an agent profit by extracting instead of contributing?
• Does quarantine remove the profitable deviation?
• Which profiles are stable and still safe?
• Which candidate mechanisms can be pruned before solving?

The feature does not make Tau a general game-theory engine. It gives Tau a proof-backed finite strategic-profile checker, a local Boolean gate that runs in ordinary Tau, and a pruning law that reduces candidate profiles when profitable-deviation evidence is available.