Stochasticity.lean

View source on GitHub

same_state_same_input_same_output

The property that determinism means: same state + same input always produces the same output. This is exactly what stochasticity breaks — a stochastic system in the same state with the same input can produce different outputs. The Stoch category in the formal backbone makes this distinction structural.

theorem same_state_same_input_same_output
    {N : Nat} {I O : Type}
    (t : BoundedTransducer N I O)
    (env : Nat → I) (s0 : Fin N) (i j : Nat)
    (hstate : t.stateTraj env s0 i = t.stateTraj env s0 j)
    (hinput : env i = env j)
    : t.output env s0 i = t.output env s0 j

The proof is a direct rewrite: substitute equal states and equal inputs into the step function.

state_collision

Pigeonhole gives a state collision: N+1 steps through Fin N states means two time steps must share the same state. This is where capacity_bound feeds in — finite energy means finite states.

must_err_at_confusion

The core limitation. If two times have the same state and same input but the environment requires different outputs, the transducer gives the wrong answer at one of them. Determinism forces identical output; the environment demands different output; contradiction at one endpoint.

theorem must_err_at_confusion
    {N : Nat} {I O : Type}
    (t : BoundedTransducer N I O)
    (env : Nat → I) (s0 : Fin N) (required : Nat → O)
    (i j : Nat)
    (hstate : t.stateTraj env s0 i = t.stateTraj env s0 j)
    (hinput : env i = env j)
    (hdiff : required i ≠ required j)
    : t.output env s0 i ≠ required i ∨
      t.output env s0 j ≠ required j

The proof first derives that the outputs are equal (from same_state_same_input_same_output), then checks: if output matches required at i, it must mismatch at j (since required differs). Otherwise, it already mismatches at i.

# A deterministic transducer with N states MUST cycle.
# When it cycles on the same input but needs different
# outputs, it's wrong at least once.

class DetTransducer:
    def __init__(self, n_states):
        self.n = n_states
        self.state = 0
    def step(self, inp):
        out = (self.state + inp) % 10
        self.state = (self.state + 1) % self.n  # deterministic
        return out

t = DetTransducer(n_states=3)
env =    [1, 1, 1, 1]  # same input every time
needed = [1, 2, 3, 4]  # but environment needs different outputs

results = []
for i, inp in enumerate(env):
    out = t.step(inp)
    ok = "ok" if out == needed[i] else "WRONG"
    results.append((i, out, needed[i], ok))

print(f"3 states, 4 steps — pigeonhole forces a state repeat")
for i, out, need, ok in results:
    print(f"  t={i}: state cycles, out={out}, need={need} [{ok}]")
print("\nDeterminism + finite states + varied demands = error.")
print("Stochasticity breaks the 'same state => same output' chain.")

finite_discrimination

Given a state collision where the environment requires different outputs, some time step k exists where the transducer errs. Existential packaging of must_err_at_confusion.

deterministic_limitation

Three independently proved facts bundled together: (1) capacity_bound gives finite states, (2) determinism means same state + same input gives same output, (3) confusion forces error. The chain is: finite states → collision → confusion → error.

Connections

• Axioms.lean — imported; provides BoundedTransducer and capacity_bound
• Pigeonhole.lean — imported; provides the state collision
• Removal.lean — A3 (attend must be stochastic) and Co1 use this argument