A few useful invariants

The arithmetic and bounded arguments behind cash checks, replay, policy windows, and eligibility.

These notes explain specific checks. Each argument has assumptions; none is a formal proof of the entire simulator or a causal model of a real company.

Cash, earnings, and obligations

For an episode with opening cash $C_0$ , let $I_t$ be settled cash inflows and $O_t$ be cash outflows recorded at transition $t$ . Reconciliation requires:

C_T = C_0 + \sum_{t=1}^{T} I_t - \sum_{t=1}^{T} O_t.

All amounts in this equation are integer cents within the declared safe bounds. Each underlying payment must have a valid identity, amount, and timing. A duplicated payment record is not another legitimate inflow merely because the final sum adds up.

Collected cash and earned revenue are different quantities. An annual prepayment brings cash forward while leaving paid-through service to deliver. The verifier reconstructs invoice periods, collections, earned revenue, and remaining obligations separately.

For the disclosed direct effect of a financing contract, proceeds $P$ , repayment liability $L$ , and fee $F$ imply:

\Delta A_{\mathrm{contract}} = P - L - F.

If principal and liability are equal, the direct net-asset effect is the negative fee. This says nothing about the profit a player might later generate with that cash. The simulator’s contract-adjusted outcome measures are also distinct from statutory financial statements.

The money bounds define exact-integer handling. The source package’s src/engine/business/financial-verifier.ts reconstructs the financial position. The calendar-boundary arithmetic tests use public synthetic fixtures. Counterfactual assessments explains the contractual requirement.

A policy applies over its entire window

Suppose cash must remain at or above $C_{\min}$ throughout the declared set of checked times $W$ . The requirement is:

\min_{t \in W} C_t \ge C_{\min}.

Checking only $C_T$ would allow a later recovery to hide an earlier breach. The same principle applies to declared customer continuity and service windows. The task must specify what is measured and when; this equation does not invent requirements for other times.

The source package’s tests/mutation-oracles.test.ts includes a cash-floor control that breaches a floor and then recovers. The ordinary verifier must still reject that policy outcome. Quality controls explains how to run the mutation suite.

Why replay can be deterministic

Write one accepted transition as:

s_{t+1} = F(s_t, a_t, U).

Here $s_t$ is the complete simulator state, $a_t$ is an accepted command, and $U$ supplies random draws addressed by their cause. With the same initial state, transition implementation, command sequence, and draw function, equal states at step $t$ produce equal states at step $t+1$ . Induction therefore gives equal states for the complete replay.

The assumptions matter. The execution identity binds actual code and runtime inputs. Draw addresses use semantic fields such as domain, entity, day, and index, rather than a mutable global random-stream cursor. Unrelated reads should not consume another customer’s future randomness.

A counterfactual comparison adds a separate requirement: both branches inherit the same factual prefix and exogenous context, changing only the declared intervention. That establishes a comparison inside this model. It does not identify an effect in a real business from observational anecdotes.

Implementation: addressed randomness. The generated causal-history tests check draw stability; counterfactual assessments documents the branch contract.

Every required predicate must hold

Once independent verification is complete, let $P_1,\ldots,P_n$ be the declared mandatory predicates, including the gameplay budget. Eligibility is:

E = \bigwedge_{i=1}^{n} P_i.

A high financial score cannot make a false required predicate true. Required supported conclusions are checked separately from probability scores. If the available evidence supports an equivalence class of causes, the hard answer concerns that class rather than an unknowable hidden member.

If verification cannot complete, the system does not evaluate this expression as a participant failure. Finalization is inconclusive and eligibility is unset. A completed but incorrect mandatory answer instead produces an ineligible result.

See Assessment requirements for conclusion equivalence and Private instances for the finalization workflow and its input bindings.

What the bounded lifecycle check covers

The lifecycle test compares the engine with an independently authored small model. Its parameter combinations cover two commitments with work in $\{0,1,2\}$ , lead times in $\{0,1\}$ , an optional dependency, capacity in $\{0,1,2\}$ , and initial cash in $\{0,1,2\}$ :

3^2 \times 2^2 \times 2 \times 3 \times 3 = 648

The explorer checks the declared abstract traces through six transitions and compares state projections after each transition. A separate regression checks a shared-dependency diamond and funded progress. Exceeding the exploration cap fails verification rather than reporting a partial search as complete.

This is bounded executable verification. It does not prove behavior for arbitrary dependency graphs, larger states, or every possible horizon. The release record and quality-control guide describe the complementary tests.