/-
  SPDX-License-Identifier: Apache-2.0
  © 2026 Lutar, Stephen P. — SZL Holdings · ORCID 0009-0001-0110-4173 · Doctrine v11 LOCKED 749/14/163

  Lutar Anchor A36 — DualStreamRoutingAxiom  (axis: Hickok · status: ts-only)

  ┌─────────────────────────────────────────────────────────────────────────┐
  │ CITATION                                                                  │
  │   Hickok, G. & Poeppel, D. (2007). "The cortical organization of speech  │
  │   processing." Nature Reviews Neuroscience 8, 393–402.                    │
  │   DOI: 10.1038/nrn2113   https://doi.org/10.1038/nrn2113                  │
  │                                                                           │
  │ CLAIM (the dual-stream model)                                             │
  │   Speech processing is organised into two largely segregated cortical    │
  │   streams: a DORSAL stream (sensorimotor / action — mapping sound onto    │
  │   articulatory representations) and a VENTRAL stream (meaning /           │
  │   comprehension — mapping sound onto conceptual representations).         │
  │                                                                           │
  │ A11OY MAPPING                                                             │
  │   Every Amaru tick MUST route through EXACTLY ONE of {dorsal, ventral}:   │
  │   never both, never neither. Dorsal = action/repetition (imperatives);   │
  │   ventral = meaning/comprehension (questions/explanations). A request     │
  │   the rule-based classifier cannot disambiguate is marked `dual` and      │
  │   the gate FAILS — A36 says exactly one stream.                           │
  └─────────────────────────────────────────────────────────────────────────┘

  STATUS: ts-only. This Lean anchor is the formal statement of the runtime
  TypeScript gate (packages/policy/src/gates/dualStreamRouting_gate.ts). The
  proof is `sorry` (honest) — the operational guarantee is provided by the
  TS gate + the dual-stream router middleware, not yet by a closed Lean proof.
-/

namespace Lutar.Gate.DualStreamRouting

/-- The two cortical processing streams of the Hickok–Poeppel dual-stream model. -/
inductive Stream where
  | dorsal   -- action / sensorimotor (repetition, imperatives)
  | ventral  -- meaning / comprehension (questions, explanations)
  deriving DecidableEq, Repr

/-- An Amaru routing decision for a single tick. -/
structure Tick where
  stream : Stream

/-- Exclusive-or over the two routing predicates: a tick is dorsal XOR ventral. -/
def routesExactlyOne (t : Tick) : Prop :=
  (t.stream = Stream.dorsal) ≠ (t.stream = Stream.ventral)

/--
  A36 — DualStreamRoutingAxiom.

  Every tick routes through exactly one of {dorsal, ventral} — never both,
  never neither. This is stated as an `axiom` (the Hickok–Poeppel architecture
  is taken as a modelling primitive, matching leanStatus = "axiom").
-/
axiom dual_stream_routing_axiom : ∀ (t : Tick), routesExactlyOne t

/--
  Soundness companion (theorem form, ts-only): a tick that the classifier could
  resolve to a single stream satisfies the exactly-one routing property.
  Proof deferred (`sorry`) — honest ts-only status; the runtime guarantee is the
  TS gate + router middleware.
-/
theorem dual_stream_routing_sound (t : Tick) : routesExactlyOne t := by
  sorry

end Lutar.Gate.DualStreamRouting