diff --git a/src/simulator/crates/mc-turn/src/processor_invariants.rs b/src/simulator/crates/mc-turn/src/processor_invariants.rs
new file mode 100644
index 00000000..f9ac6301
--- /dev/null
+++ b/src/simulator/crates/mc-turn/src/processor_invariants.rs
@@ -0,0 +1,326 @@
+//! Proptest invariants over `TurnProcessor::step()`.
+//!
+//! These are "for any valid input X, property Y holds" checks, complementing
+//! the deterministic seed/scenario tests in `processor::tests`. Each invariant
+//! targets a specific contract of the bench processor.
+//!
+//! If an invariant regresses, the correct response is to either fix the
+//! invariant (if the assumption was wrong) or fix the processor (if a real
+//! bug surfaced). Commenting out or `#[ignore]`-ing a failing invariant is
+//! not acceptable.
+
+#![allow(clippy::unwrap_used)]
+
+use crate::game_state::{CityEcology, GameState, MapUnit, PlayerState};
+use crate::processor::{LairCombatConfig, TurnProcessor};
+use mc_ai::evaluator::ScoringWeights;
+use mc_city::CityState;
+use mc_core::grid::GridState;
+use proptest::prelude::*;
+use std::collections::HashMap;
+
+// Keep runtime bounded: default 256 * 5 invariants was fine in development,
+// but one invariant runs 1000 turns per case so we trim it locally.
+const LONG_RUN_CASES: u32 = 64;
+const DEFAULT_CASES: u32 = 128;
+
+// ── Generators ─────────────────────────────────────────────────────────────
+
+prop_compose! {
+    /// Produce a `LairCombatConfig` whose fields stay in the "sane" range the
+    /// balance team actually tunes over. This intentionally does NOT explore
+    /// degenerate values (negative slopes, huge radii) — those aren't part of
+    /// the processor's contract.
+    fn arb_lair_combat_config()(
+        encounter_radius_t1_t3 in 1i32..=3,
+        encounter_radius_t4_t6 in 1i32..=4,
+        encounter_radius_t7_t9 in 2i32..=5,
+        encounter_radius_t10 in 3i32..=6,
+        base_kill_rate in 0.0f32..=0.5,
+        tier_kill_slope in 0.0f32..=0.2,
+        tier_kill_exponent in 0.5f32..=3.0,
+        fortify_divisor in 1.0f32..=4.0,
+        encounter_probability_per_turn in 0.0f32..=0.2,
+        gold_per_wealth_per_city in 0i32..=10,
+        prod_per_axis_per_city in 0u32..=10,
+        expansion_per_axis_per_turn in 0u32..=5,
+        city_founding_cost in 10u32..=60,
+        unit_spawn_cost in 1u32..=40,
+        max_cities_per_player_base in 2u8..=25,
+    ) -> LairCombatConfig {
+        LairCombatConfig {
+            encounter_radius_t1_t3,
+            encounter_radius_t4_t6,
+            encounter_radius_t7_t9,
+            encounter_radius_t10,
+            base_kill_rate,
+            tier_kill_slope,
+            tier_kill_exponent,
+            fortify_divisor,
+            encounter_probability_per_turn,
+            gold_per_wealth_per_city,
+            prod_per_axis_per_city,
+            expansion_per_axis_per_turn,
+            city_founding_cost,
+            unit_spawn_cost,
+            max_cities_per_player_base,
+        }
+    }
+}
+
+prop_compose! {
+    /// A strategic-axis map with `expansion`, `production`, `wealth`, `culture`
+    /// all in 0..=10 (the canonical axis range).
+    fn arb_strategic_axes()(
+        expansion in 0u8..=10,
+        production in 0u8..=10,
+        wealth in 0u8..=10,
+        culture in 0u8..=10,
+    ) -> HashMap<String, u8> {
+        let mut m = HashMap::new();
+        m.insert("expansion".to_string(), expansion);
+        m.insert("production".to_string(), production);
+        m.insert("wealth".to_string(), wealth);
+        m.insert("culture".to_string(), culture);
+        m
+    }
+}
+
+prop_compose! {
+    /// A single unit placed inside a map of side `map_size`.
+    fn arb_map_unit(map_size: i32)(
+        col in 0i32..map_size,
+        row in 0i32..map_size,
+        hp in 1i32..=80,
+        fortified in any::<bool>(),
+    ) -> MapUnit {
+        MapUnit {
+            col,
+            row,
+            hp,
+            max_hp: 80,
+            attack: 12,
+            defense: 1,
+            is_fortified: fortified,
+            unit_id: "dwarf_warrior".to_string(),
+        }
+    }
+}
+
+prop_compose! {
+    /// A `PlayerState` with `n_cities` starter cities and 0..=`max_units`
+    /// units placed on a map of side `map_size`.
+    fn arb_player_state(n_cities: usize, max_units: usize, map_size: i32)(
+        gold in 0i32..=10_000,
+        axes in arb_strategic_axes(),
+        units in prop::collection::vec(arb_map_unit(map_size), 0..=max_units),
+    ) -> PlayerState {
+        let cities: Vec<CityState> = (0..n_cities).map(|_| CityState::starter()).collect();
+        let city_buildings: Vec<Vec<String>> = (0..n_cities).map(|_| Vec::new()).collect();
+        let city_ecology: Vec<CityEcology> = (0..n_cities).map(|_| CityEcology::default()).collect();
+        // Place cities on a simple diagonal inside the map so positions stay
+        // in-bounds. Clamp to map_size-1 so tiny maps still work.
+        let city_positions: Vec<(i32, i32)> = (0..n_cities)
+            .map(|i| {
+                let x = ((i as i32 * 2) + 1).min(map_size - 1).max(0);
+                let y = ((i as i32 * 2) + 1).min(map_size - 1).max(0);
+                (x, y)
+            })
+            .collect();
+        let unit_upkeep = vec![0i32; units.len()];
+        PlayerState {
+            player_index: 0,
+            gold,
+            cities,
+            unit_upkeep,
+            strategic_axes: axes,
+            scoring_weights: ScoringWeights::default(),
+            expansion_points: 0,
+            city_buildings,
+            city_ecology,
+            tech_state: None,
+            science_yield: 0,
+            units,
+            city_positions,
+            arcane_lore_pop_deducted: false,
+        }
+    }
+}
+
+prop_compose! {
+    /// A full `GameState` with one player and a lair-stamped grid. Follows the
+    /// same shape as `make_bench_state` in `processor::tests` but with random
+    /// lair placement and tiers.
+    fn arb_game_state(map_size: i32, n_lairs: usize)(
+        player in arb_player_state(1, 6, map_size),
+        lair_positions in prop::collection::vec(
+            (0i32..map_size, 0i32..map_size, 1i32..=10),
+            0..=n_lairs,
+        ),
+    ) -> GameState {
+        let mut grid = GridState::new(map_size, map_size);
+        for (col, row, tier) in lair_positions {
+            let idx = (row * map_size + col) as usize;
+            if idx < grid.tiles.len() {
+                grid.tiles[idx].lair_tier = tier;
+                grid.tiles[idx].lair_population = 10.0;
+                grid.tiles[idx].lair_species_id = (idx as u32).wrapping_add(1).max(1);
+            }
+        }
+        GameState {
+            turn: 0,
+            players: vec![player],
+            grid: Some(grid),
+        }
+    }
+}
+
+// ── Helpers ────────────────────────────────────────────────────────────────
+
+fn count_active_lairs(state: &GameState) -> usize {
+    match &state.grid {
+        Some(g) => g
+            .tiles
+            .iter()
+            .filter(|t| t.lair_tier > 0 && t.lair_population > 0.1)
+            .count(),
+        None => 0,
+    }
+}
+
+fn make_processor_with(cfg: LairCombatConfig) -> TurnProcessor {
+    let mut p = TurnProcessor::new(500);
+    p.lair_combat_config = cfg;
+    p
+}
+
+// ── Invariants ─────────────────────────────────────────────────────────────
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(DEFAULT_CASES))]
+
+    /// Invariant 1 — `gold` is never negative after a `step()` call.
+    ///
+    /// The processor's economy phase explicitly clamps insolvent treasuries to
+    /// zero (and disbands a unit as punishment). This invariant pins that
+    /// contract across 100 turns of random-axis play.
+    #[test]
+    fn gold_never_negative_after_step(
+        cfg in arb_lair_combat_config(),
+        mut state in arb_game_state(12, 10),
+    ) {
+        let processor = make_processor_with(cfg);
+        for _ in 0..100 {
+            processor.step(&mut state);
+            for p in &state.players {
+                prop_assert!(
+                    p.gold >= 0,
+                    "gold went negative after step: {} (turn {})",
+                    p.gold, state.turn
+                );
+            }
+        }
+    }
+
+    /// Invariant 2 — one `step()` cannot add more units than there are cities.
+    ///
+    /// Each city produces at most one unit per turn (`try_spawn_unit`), so the
+    /// upper bound is `prev_units + cities.len()`. Fauna combat can REMOVE
+    /// units, so the bound is asymmetric (only the upper side holds).
+    #[test]
+    fn unit_count_bounded_by_production(
+        cfg in arb_lair_combat_config(),
+        mut state in arb_game_state(10, 6),
+    ) {
+        let processor = make_processor_with(cfg);
+        // Run a few turns to let production accumulate, then re-check each step.
+        for _ in 0..20 {
+            let prev_units: Vec<usize> = state.players.iter().map(|p| p.units.len()).collect();
+            let prev_cities: Vec<usize> = state.players.iter().map(|p| p.cities.len()).collect();
+            processor.step(&mut state);
+            for (pi, p) in state.players.iter().enumerate() {
+                let upper = prev_units[pi] + prev_cities[pi];
+                prop_assert!(
+                    p.units.len() <= upper,
+                    "player {pi}: units grew from {} to {} in one step (cities={}) — max was {}",
+                    prev_units[pi], p.units.len(), prev_cities[pi], upper
+                );
+            }
+        }
+    }
+
+    /// Invariant 3 — city count never exceeds the soft cap formula.
+    ///
+    /// `try_found_city` caps the per-player city count at
+    /// `max_cities_per_player_base + expansion_axis * 3` (via `saturating_add`).
+    /// After any number of turns, that bound must hold.
+    #[test]
+    fn city_count_respects_soft_cap(
+        cfg in arb_lair_combat_config(),
+        mut state in arb_game_state(16, 8),
+    ) {
+        // Compute cap per player up-front — axes don't change mid-run.
+        let caps: Vec<u32> = state
+            .players
+            .iter()
+            .map(|p| {
+                let exp = *p.strategic_axes.get("expansion").unwrap_or(&3) as u32;
+                cfg.max_cities_per_player_base as u32 + exp * 3
+            })
+            .collect();
+        let processor = make_processor_with(cfg);
+        for _ in 0..300 {
+            processor.step(&mut state);
+        }
+        for (pi, p) in state.players.iter().enumerate() {
+            prop_assert!(
+                (p.cities.len() as u32) <= caps[pi],
+                "player {pi}: {} cities exceeds cap {} after {} turns",
+                p.cities.len(), caps[pi], state.turn
+            );
+        }
+    }
+}
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(LONG_RUN_CASES))]
+
+    /// Invariant 4 — the lair count is monotonically non-increasing.
+    ///
+    /// Lairs can die (population decayed below the 0.1 activity floor) but can
+    /// never spontaneously appear — the processor never writes to `lair_tier`,
+    /// it only decays `lair_population`.
+    #[test]
+    fn lair_count_monotone_non_increasing(
+        cfg in arb_lair_combat_config(),
+        mut state in arb_game_state(14, 20),
+    ) {
+        let processor = make_processor_with(cfg);
+        let mut prev = count_active_lairs(&state);
+        for _ in 0..100 {
+            processor.step(&mut state);
+            let now = count_active_lairs(&state);
+            prop_assert!(
+                now <= prev,
+                "active lair count increased from {prev} to {now} in one step"
+            );
+            prev = now;
+        }
+    }
+
+    /// Invariant 5 — `step()` is total over the valid input domain.
+    ///
+    /// For any well-formed state produced by the generators (positions in
+    /// bounds, aligned per-city Vecs, valid tier range), calling `step()` many
+    /// times must not panic, unwrap-fail, overflow, or go out of bounds.
+    #[test]
+    fn step_is_total_for_valid_inputs(
+        cfg in arb_lair_combat_config(),
+        mut state in arb_game_state(10, 25),
+    ) {
+        let processor = make_processor_with(cfg);
+        for _ in 0..50 {
+            let _ = processor.step(&mut state);
+        }
+    }
+}