Spaces:
Running
Running
File size: 2,953 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 | -- Lutar/Gate/InternalFeedback.lean
-- A37 InternalFeedbackIntegrity
-- Citation: Hickok, Houde, Rong (2011). Sensorimotor integration in speech processing:
-- Computational basis and neural organization. Neuron 69, 407-422.
-- DOI: 10.1016/j.neuron.2011.01.019
--
-- Authored by Yachay (CTO), SZL Holdings. Co-Authored-By: Perplexity Computer Agent.
-- Doctrine v11 LOCKED 749/14/163 · Λ Conjecture 1 · SLSA L1 honest · ADDITIVE only
--
-- Interpretation:
-- Hickok's state feedback control architecture requires that an agent's
-- internal feedback loop checks the *predicted* sensory consequence of a planned
-- action against the *sensory target* before the action executes.
-- When this loop is damaged (conduction aphasia), motor plans and outputs can
-- appear intact while the checking mechanism is broken.
--
-- In SZL a11oy: SafeToExecute holds iff the PAC-Bayes Governance Head's
-- predicted sensory consequence is within epsilon of the observed actual consequence.
-- The Conduction-Aphasia Detector (conduction_aphasia.py) provides the LIVE
-- evaluator for this anchor (status: live, severity: enforced).
--
-- Proof status: ts-only (TypeScript + Python evaluator live; Lean proof scheduled
-- for Doctrine v12). The `sorry` is honest: this stub documents the INTENT.
namespace Lutar.Gate
-- Abstract types (concrete implementations live in conduction_aphasia.py)
opaque Sensory : Type
opaque SafeToExecute : Prop
opaque dist : Sensory → Sensory → Float
-- A37 InternalFeedbackIntegrity (live, enforced)
-- An action may execute only when dist(predicted, target) <= epsilon.
theorem internal_feedback_intact
(predicted target : Sensory) (ε : Float) (h : dist predicted target ≤ ε) :
SafeToExecute := by
sorry -- ts-only; proof scheduled for Doctrine v12
-- A36 DualStreamRoutingAxiom (ts-only, advisory)
-- Every a11oy tick routes through exactly one of {dorsal, ventral}, never both, never neither.
-- Citation: Hickok & Poeppel 2007, Nat Rev Neurosci 8:393-402. DOI 10.1038/nrn2113
inductive Stream : Type where
| dorsal : Stream -- action / repetition / sensorimotor
| ventral : Stream -- meaning / comprehension / lexical
deriving DecidableEq
opaque Tick : Type
opaque stream_of : Tick → Stream
axiom dual_stream_routing : ∀ (t : Tick),
(stream_of t = Stream.dorsal ∧ ¬(stream_of t = Stream.ventral)) ∨
(stream_of t = Stream.ventral ∧ ¬(stream_of t = Stream.dorsal))
-- A38 HierarchicalLinearizationRoundTrip (ts-only, advisory)
-- Receipt chain linearization is lossless: recover(linearize(h)) = h
-- Citation: Hickok 2025, Wired for Words (MIT Press); C-STAR lecture 2026
opaque Hierarchy : Type
opaque linearize : Hierarchy → List Hierarchy
opaque recover : List Hierarchy → Hierarchy
theorem hier_linearization_round_trip
(h : Hierarchy) : recover (linearize h) = h := by
sorry -- ts-only; proof scheduled for Doctrine v12
end Lutar.Gate
|