Spaces:
Running
Running
File size: 3,749 Bytes
4ee7081 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 | /-
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
|