Military Strategy via Topology: A Corpus Course

A four-unit curriculum reading warfare, logistics, and command structures as the discrete routing and manifold-computation problems the Gnosis corpus already certifies.

Companion formal surface: the Lean course modules in gnosis-math/Gnosis/MilitaryStrategy/ (SupplyLineLogistics.lean, SiegeSeverance.lean, OodaRacingPipeline.lean, CoalitionTreatyTopology.lean), registered through Gnosis/Ledger/MilitaryStrategy.lean. Canonical proof claims live in the Lean modules and the root ledgers, not in this manuscript.

0. Doctrine of the course

This course replaces subjective military theory with a ledger of structural identities. Three commitments follow from the corpus's Rustic Church doctrine, and they shape every unit:

1. Finite, decidable topologies only. The math kernel closes theorems by definitional unfolding and Init-level Nat lemmas — no classical-real continuous math, no Mathlib. Supply networks are finite graphs, contraction rates are Nat-rationals n/d < 1, quorums are subtractions. What a green build certifies is local: the finite carrier bears the weight its name claims. Nothing here claims to integrate a battlefield over ℝ.

2. Subsume, don't restate. Each unit is a corollary layer. The military vocabulary (depots, corridors, sieges, quorums, OODA menus, treaties) is new; the load-bearing inequalities are imported from the existing theorem families — the mycelial ordering package, the spiderweb surfaces, the Byzantine pair, codec racing, compositional ergodicity, finite Nash, semiotic deficit, causal mediation. If a claimed strategic law cannot be discharged against one of those carriers, it stays prose, labeled.

3. Every protection ships its red-team theorem. Each unit ends with an adversarial dual (Gnosis/Adversarial/AdversarialDual.lean): a witnessed input class its protective gate wrongly admits, plus the patched gate proved sound. A defense whose failure boundary is unnamed is Sardis-mode — a name that liveth and is dead.

A mapping disclaimer, stated once and meant everywhere: these are structural mappings, not identity claims. mycelial_network_capacity n = 15·n is a calibrated corpus constant, not a measurement of any army. The value of the course is the shape of each law — which quantities bound which, what breaks at the boundary, and which observation would falsify the claim — not the particular constants the finite carriers wear.

Unit I — Logistics, supply lines, and route dominance

Lean module: Gnosis/MilitaryStrategy/SupplyLineLogistics.lean Reuses: CrossDomain/CrossDomainMycelialTopologicalOrdering.lean, AnarchyJacksonQueueBridge.lean

A force is only as effective as its supply chain, so the course starts where the corpus is strongest: scheduling work over a network. A theater is a SupplyNetwork (depots as nodes, corridors as edges); a campaign plan is a CampaignLogistics witness carrying its march-order obligation, route cost, forage budget, peak staged materiel, provisioned corridor capacity, and rear-guard debt. The plan is admissible exactly when its reading as a MycelialOrderingWitness satisfies mycelialScheduleValid.

Five bounds fall out as corollaries (supply_doctrine_bundle):

The dominance law is the unit's headline: at any positive depot count the distributed (mycelial) capacity strictly exceeds the FIFO queue capacity — the corpus's mycology_dominates_queueing wearing a quartermaster's coat. This is the formal floor under "throughput under pressure favors the network over the column."

Staging depots are Jackson control queues (AnarchyJacksonQueueBridge): local requisitions plus command directives arrive against depot throughput. The stability law is an equivalence, which makes it a field metric:

• zero_backlog_iff_depot_stable — a depot's backlog is zero iff throughput covers arrivals. Observe a positive backlog and the stability claim is refuted; no narrative survives the ledger.
• reinforcement_never_worsens_backlog — throughput is antitone in backlog: reinforcing a depot can never make its queue worse.

Adversarial dual. Campaign validity does not certify that the route fits any single corridor: corridor_fit_blindspot exhibits a fully valid plan routing cost 5 through a corridor provisioned at 3. The quartermaster's green checkmark is a network-level statement; the patched gate (corridor_fit_patched_sound) is what a corridor-level claim requires.

Exercise. Take a historical two-corridor advance (e.g., a pincer) and assign the witness fields. Which of the five bounds fails first as the advance outruns its railhead — and is that the corridor bound or the network bound? The distinction is exactly the blindspot theorem.

Unit II — Siege, severance, and fault tolerance

Lean module: Gnosis/MilitaryStrategy/SiegeSeverance.lean Reuses: SpiderwebTopology.lean, SpiderwebMeshNetwork.lean, SpiderwebBFT.lean, ReynoldsBFT.lean

A defender's communications-and-supply web is a connected spiderweb: V nodes, E strands, first Betti number β₁ = E + 1 − V. The course renames β₁ the severance budget — the number of strands interdiction can cut before connectivity itself is at stake — and proves the interdiction ledger in both directions:

• severance_spends_one_cycle — cutting a strand spends exactly one cycle of the budget (the inverse of add_strand_adds_cycle, which prices reinforcement at exactly one cycle gained).
• acyclic_web_cannot_lose_a_strand — a tree-shaped web (budget zero) has no spare strand: any cut disconnects. Hub-and-spoke command is one interdiction away from silence.
• severance_budget_le_strands — the budget never exceeds E; redundancy is bounded by what was actually strung.

Encirclements are spiderweb meshes: besieging corps as peer rings, picket depth as hops, β₁ = corps × depth independent routes (encirclement_redundancy). The deepening law (deepening_adds_one_route_per_corps) prices siege depth exactly: one more hop buys one route per corps, so protocol adequacy — required ≤ β₁ — is monotone under deepening (adequacy_survives_deepening). The accounting theorems keep V, E, and routing honest: routes never outrun wires, and posts always outnumber routes.

Degraded chain-of-command is the corpus's Byzantine pair. A CommandNet of n officers with up to f subverted, provisioned at the doctrine bound n ≥ 3f + 1 (the THM-REYNOLDS-BFT family), certifies three guarantees:

• orders_still_issue — the action quorum plus the compromised officers is the whole staff: silence never blocks the quorum;
• loyal_majority — the quorum holds 2f + 1 loyal officers;
• two_orders_share_a_loyal_officer — any two quorums intersect in a loyal officer, so contradictory orders cannot both carry a quorum.

Relay echelons inherit the Reynolds fork/race/fold thresholds: echelon_quorumSafe_implies_majoritySafe (chunks covering stages implies N < 2C) and saturated_echelons_never_idle (enough dispatches keep every relay busy) — the pipeline-idle reading of Re = N/C.

Adversarial dual — the tightness antitheorem. The sloppy gate 3f ≤ n, one officer short of doctrine, admits the witness (n, f) = (3, 1) whose two-officer action quorums fail to share a loyal member (sloppy_provisioning_blindspot). The strict gate is proved sound for every configuration (strict_provisioning_sound). The missing officer is load-bearing; that is what "the threshold is tight" means, and it is a theorem, not a slogan.

Exercise. Compute the severance budget of a ring-of-outposts web versus a hub-and-spoke web at equal E. The ring survives β₁ cuts; the hub survives none. Then price the reinforcement plan that raises the hub's budget to the ring's, strand by strand, using the two one-cycle ledger entries.

Unit III — OODA loops and tactical racing

Lean module: Gnosis/MilitaryStrategy/OodaRacingPipeline.lean Reuses: CodecRacing.lean (THM-TOPO-RACE-SUBSUMPTION family), CompositionalErgodicity.lean (THM-ERGODICITY-MONOTONE-IN-STAGES, THM-PIPELINE-CERTIFICATE)

One OODA cycle is a codec race: fork every course of action on the menu, race them to the cheapest executed cost, fold the winner. The subsumption family is the tempo doctrine:

• ooda_race_subsumes_fixed_doctrine — the raced cost never exceeds any fixed doctrine on the menu (THM-TOPO-RACE-SUBSUMPTION: the racing wire is ≤ any fixed codec wire). An adaptive decision race cannot lose to a static strategy it forked.
• campaign_race_subsumes_standing_orders — summed across engagements, racing beats any standing orders fixed in advance.
• reserve_option_never_hurts / decisive_option_forces_improvement — keeping a reserve option is free; a genuinely better option forces strict improvement.
• adaptive_command_zero_tempo_deficit — the racer pays zero deficit above its own optimum, by construction.
• no_doctrine_beats_attrition_floor — the entropy floor caps the story from below: tempo optimizes within the attrition bound, never below it. Together with subsumption this sandwiches the fork/race/fold gain.

Staged operations are ergodic pipelines. Each stage of a layered defense or phased offensive carries a contraction certificate — the Nat-rational n/d < 1 of the geometric-ergodicity surface — and composition is automatic:

• layering_never_worsens_contraction (THM-ERGODICITY-MONOTONE-IN-STAGES): adding a stage can only improve the per-step contraction rate. A deeper defense settles faster, never slower.
• two_stage_operation_certificate (THM-PIPELINE-CERTIFICATE) and the course's new three_stage_operation_certificate: per-stage certificates compose through two and three echelons (n₁n₂n₃ < d₁d₂d₃) with no new analysis.
• parallel_axes_certificate (THM-PARALLEL-ERGODICITY): simultaneous axes of advance contract at the max rate, which stays sub-unit — simultaneity costs no stability.

Adversarial dual — the vacuity boundary. The tempo gate "raced cost fits the budget" admits the empty menu, which races to cost 0 under any budget while commanding nothing (empty_menu_blindspot). A tempo dashboard with no options behind it is a green status over a dead capability; the patched gate (tempo_gate_patched_sound) demands a non-empty menu. Fast decision cycles over an empty decision space are the OODA reading of the Sardis warning.

Exercise. Encode two doctrines and a menu of four courses of action for one engagement; verify by computation that the race beats both doctrines, then delete every option and watch the gate still pass — the blindspot in action.

Unit IV — Game theory, conflict, and alliance topology

Lean module: Gnosis/MilitaryStrategy/CoalitionTreatyTopology.lean Reuses: FiniteMatrixNash.lean, SemioticDeficit.lean, CausalMediation.lean, plus Unit II's severance calculus

Adversarial strategy proper. The corpus's finite game surface carries four closed, kernel-checked results, each with a doctrine reading:

• arms_race_equilibrium_exists / arms_race_equilibrium_unique — the 3×3 escalation game has exactly one pure equilibrium: mutual maximal escalation. The arms race has a stable point, and it is the bad one.
• restraint_is_never_self_enforcing — unilateral restraint appears in no equilibrium. De-escalation must be imposed by changing the game (treaty structure, repeated play, external enforcement), not by recommending better play inside it.
• feint_standoff_has_no_pure_equilibrium — the matching-pennies antitheorem: some confrontations admit no stable pure posture at all. Proved non-existence is as load-bearing as any equilibrium witness.
• coalition_selects_among_ranked_equilibria — the stag hunt carries two payoff-ranked equilibria; an alliance's job is equilibrium selection.

Honest deferral, inherited from the corpus: mixed strategies are not formalized (Nat cannot carry probability weights), so "Nash convergence" here means pure-equilibrium certificates and proved non-existence, not fixed-point convergence. The complement-distribution/BATNA-as-void-walking reading lives in NegotiationEquilibrium.lean and Void/VoidWalking.lean and is cited as the negotiation-side continuation of this unit.

Treaty negotiation is a semiotic channel — disputed dimensions against negotiation tracks — and the deficit calculus becomes diplomacy:

• understaffed_talks_carry_deficit — more disputes than tracks forces a positive diplomatic deficit;
• single_track_diplomacy_max_deficit — one track carries the maximal deficit disputes − 1;
• adding_track_weakly_reduces_deficit — opening a track never hurts;
• confidence_building_reduces_deficit / sufficient_context_clears_deficit — accumulated context can clear the working deficit;
• full_spectrum_talks_deficit_free — matching every dispute with a track leaves nothing uncarried.

Alliance topology reuses Unit II verbatim: a coalition is a pact web, redundancy is its severance budget, a hub-and-spoke coalition has zero redundancy (hub_and_spoke_coalition_no_redundancy) and cannot survive one abrogated pact (fragile_coalition_cannot_lose_a_pact), while each cross-pact buys exactly one severable cycle. Coalition warfare's fragility is a Betti number.

Mediation between belligerents is the causal-mediation ledger: mediated_settlement_decomposes (the settlement decomposes additively), mediator_toll_irreducible (every mediator loses at least one unit — there is no lossless honest broker), mediation_strictly_attenuates, shuttle_diplomacy_accumulates_toll (two mediators lose at least two), and exhausted_mediation_chain (a chain as long as its substance consumes all of it — the heat death of shuttle diplomacy).

Adversarial dual — the paper peace. The closure gate "accumulated context has driven the working deficit to zero" admits the witness (3 disputes, 1 track, 2 rounds of context): the counter reads zero while the structural mismatch persists (paper_peace_blindspot). Rotate the envoys — lose the context — and the deficit returns. The patched gate (paper_peace_patched_sound) demands the matched channel itself, not a talked-out counter. A zero working deficit is not a peace certificate.

Exercise. Model a three-party dispute as both a semiotic channel and a pact web. Show that adding a mediator adds an irreducible toll (mediator_toll_irreducible) while adding a direct track reduces the deficit for free (adding_track_weakly_reduces_deficit) — then name the condition under which the mediator is still worth the toll (hint: it is not in this ledger, and that is the point of naming deferrals).

5. Ledger crosswalk

Existing THM families the course discharges against, as registered in THEOREM_LEDGER.md and the Lean modules:

New course theorems (THM-MILSTRAT-* banners in the Lean modules): supply bounds and FIFO dominance (Unit I), severance cost and tree fragility, encirclement redundancy, command quorum and BFT tightness (Unit II), OODA subsumption, stage monotonicity, three-echelon certificate, empty-menu vacuity (Unit III), unique escalation equilibrium, treaty deficit and track monotonicity, coalition tree fragility, mediation toll, paper-peace blindspot (Unit IV).

MCP ownership note: per scripts/ledger-mcp-ownership.ts, the reused families are owned by topology-mcp (Spiderweb), quorum-mcp (Reynolds BFT), queueing-mcp (queueing/Jackson), race-mcp/ergodicity-mcp (racing, pipelines), negotiation-mcp and conflict-mcp (negotiation, semiotic deficit and peace), and void-walking-mcp (void walking). There is no dedicated game-theory or diplomacy server; those doctrines route through the owners above.

6. What would falsify this course

In keeping with the anti-theory manifesto: each unit names its observable. A depot with covered arrivals showing persistent backlog falsifies the stability equivalence's applicability to that depot (the model, not the theorem). A web surviving more cuts than its Betti number falsifies the graph reading. A three-officer, one-traitor staff that never forks orders under adversarial scheduling falsifies nothing — the blindspot theorem only says forking is possible — but a 3f+1-provisioned staff that forks orders falsifies the mapping of "compromised" onto Byzantine faults. A fixed doctrine that consistently beats the race over the same menu falsifies the cost accounting. These are the course's exit criteria: the mappings earn their keep only at the granularity where the finite carriers still bear weight.