Establish RED-4: observation-blind realization checking

STATUS.md

@@ -55,7 +55,7 @@ They should not be copied into new semantic-continuity modules.
 
 See `docs/TERMINOLOGY_AUDIT.md`.
 
-## Active formal milestone — GREEN-3
+## Active formal milestone — RED-4
 
 RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate.
 
@@ -87,7 +87,15 @@ GREEN-3 adds a generic target-specific \`ProtocolModel(State, Step)\` with an ex
 
 See \`docs/research/GREEN3_PROTOCOL_TRANSITION_CHECK.md\`.
 
-This closes the RED-3 protocol-sequencing gap relative to the stated model. Concrete observations/effects, persistence, timing, and simulator/physical-device conformance remain open.
+This closes the RED-3 protocol-sequencing gap relative to the stated model.
+
+RED-4 now freezes the GREEN-3-valid binding, representation, and protocol execution and mutates only the post-execution observation. A machine-checked witness shows that both outcomes pass GREEN-3 because observed semantic effect is outside its model.
+
+See \`docs/research/RED4_OBSERVATION_BLINDNESS.md\`.
+
+This establishes the next narrow gap: **a valid modeled realization is not the same thing as an observed semantic effect**.
+
+Observation provenance, payload-to-trace linkage, persistence, timing, and simulator/physical-device conformance remain open.
 
 The motivating case is:
 

docs/research/RED4_OBSERVATION_BLINDNESS.md

@@ -0,0 +1,147 @@
+# RED-4 — Observation-Blind Realization Check
+
+**Branch:** `research/semantic-continuity-red4`  
+**Baseline:** `fdba805e5d58113622851c52f68e96735d83c5d1`
+
+## Research question
+
+After GREEN-3, can PSL distinguish two outcomes that contain the **same valid
+modeled execution** but differ in whether the intended effect was observed?
+
+At this baseline, the answer is **no**.
+
+## What RED-4 freezes
+
+RED-1 changed the resource.
+
+RED-2 changed the representation.
+
+RED-3 changed the protocol trace.
+
+RED-4 changes none of those.
+
+Both outcomes contain the exact same GREEN-3-valid execution:
+
+```text
+resource       = 0x20
+raw write      = 250
+protocol trace = enter-config
+                 issue-write
+                 observe-ACK
+                 exit-config
+```
+
+The only mutation is the post-execution observation:
+
+```text
+reference observation = some 250
+mutated observation   = none
+```
+
+## Machine-checked negative result
+
+`lean/PSL/SemanticContinuityRed4.lean` introduces:
+
+```text
+CandidateOutcome(Resource, RawObservation)
+  execution
+  observation
+```
+
+and proves:
+
+```text
+reference.execution = mutated.execution
+reference.observation != mutated.observation
+
+GREEN3(reference) = true
+GREEN3(mutated)   = true
+```
+
+This establishes the next narrow gap:
+
+> **A valid modeled realization is not the same thing as an observed semantic effect.**
+
+## Important claim boundary
+
+RED-4 does **not** yet prove that raw observation `250` demonstrates the
+intended semantic effect.
+
+At this stage `some 250` is only the reference fixture for the next
+falsification step.
+
+The current theory has no independent relation connecting:
+
+```text
+semantic intent
+    ->
+executed realization
+    ->
+observable target state
+```
+
+That missing relation is the RED-4 result.
+
+## Why GREEN-3 accepts both
+
+GREEN-3 checks:
+
+```text
+semantic identity
+    -> target resource
+
+semantic value
+    -> target representation
+
+target trace
+    -> protocol transition model
+```
+
+The two RED-4 outcomes are identical on all three dimensions.
+
+GREEN-3 never inspects the post-execution observation, so absence of an
+observation is invisible to it.
+
+## GREEN-4 obligation
+
+GREEN-4 should add the **minimum** observation/effect semantics required to
+distinguish the outcomes.
+
+The acceptance target is:
+
+```text
+same binding
+same representation
+same valid protocol trace
+
+reference observed effect -> ACCEPT
+missing observed effect   -> REJECT
+```
+
+without:
+
+- trusting a realization-generated success flag;
+- treating ACK alone as proof of semantic effect;
+- embedding PVM32 observation details into the target-neutral semantic intent;
+- claiming simulator or physical-device conformance prematurely.
+
+A likely next object is an independent target-specific observation model that
+relates concrete observable state back to the semantic value.
+
+## Still-open boundary
+
+GREEN-3's abstract `issueWrite` protocol marker is not yet parameterized by
+the concrete payload. Resource/representation correctness and protocol
+correctness are checked separately.
+
+RED-4 does not silently solve that issue. It remains an explicit future attack
+surface alongside observation provenance, persistence, timing, and target
+conformance.
+
+## Kill condition
+
+If proof of semantic effect requires target-specific observations to be copied
+into the target-neutral contract, the continuity boundary has failed.
+
+The semantic contract should state the intended effect; target-specific
+observation semantics should justify that effect independently.

lean/Audit.lean

@@ -6,6 +6,7 @@ import PSL.SemanticContinuityRed2
 import PSL.SemanticContinuityGreen2
 import PSL.SemanticContinuityRed3
 import PSL.SemanticContinuityGreen3
+import PSL.SemanticContinuityRed4
 
 #print axioms validateIRClosed_sound
 #print axioms validateWords_execution
@@ -34,3 +35,6 @@ import PSL.SemanticContinuityGreen3
 #print axioms PSL.checkProtocol_true_iff
 #print axioms PSL.green3_separates_red3_witness
 #print axioms PSL.green3_checked_protocol_is_model_faithful
+
+#print axioms PSL.red4_executions_are_identical
+#print axioms PSL.red4_green3_is_observation_blind

lean/PSL/SemanticContinuityRed4.lean

@@ -0,0 +1,151 @@
+import PSL.SemanticContinuityGreen3
+
+namespace PSL
+
+/-
+  Semantic Continuity RED-4
+  -------------------------
+
+  GREEN-3 established:
+    * binding correctness relative to a DeviceModel,
+    * representation correctness relative to a RepresentationModel, and
+    * protocol-sequence correctness relative to a ProtocolModel.
+
+  RED-4 asks whether that is enough to establish that the intended device
+  effect was actually observed.
+
+  It is not.
+
+  Two candidate outcomes may contain the exact same GREEN-3-valid execution
+  while differing only in externally reported observation. GREEN-3 has no
+  observation/effect relation, so both outcomes pass its strongest current
+  gate.
+
+  This file deliberately does NOT introduce observation semantics. It records
+  the next missing relation.
+-/
+
+/--
+A minimal post-execution outcome.
+
+The execution is the object already checked by GREEN-3. The observation is kept
+separate so RED-4 can show that GREEN-3 does not inspect it.
+
+RawObservation is generic because different targets may expose different
+observable state.
+-/
+structure CandidateOutcome (Resource RawObservation : Type) where
+  execution   : CandidateExecution Resource
+  observation : Option RawObservation
+  deriving Repr, BEq, DecidableEq
+
+/--
+Lift the strongest GREEN-3 gate to an outcome.
+
+The observation is intentionally ignored because GREEN-3 has no observation or
+effect model. That omission is the property RED-4 is testing.
+-/
+def green3OutcomeGate
+    {Resource SemanticValue State Step RawObservation : Type}
+    (device : DeviceModel Resource)
+    (representation : RepresentationModel SemanticValue Nat)
+    (protocol : ProtocolModel State Step)
+    (semanticId : SemanticId)
+    (semanticValue : SemanticValue)
+    (traceOf : CandidateExecution Resource → List Step)
+    (outcome : CandidateOutcome Resource RawObservation) : Bool :=
+  green3ExecutionGate
+    device
+    representation
+    protocol
+    semanticId
+    semanticValue
+    outcome.execution
+    traceOf
+
+/--
+Reference outcome for the RED-4 witness.
+
+The raw observation 250 is only an experiment fixture at RED-4. The current
+theory does not yet state why this observation demonstrates the intended
+semantic effect.
+-/
+def referenceObservedOutcome : CandidateOutcome (Fin 256) Nat :=
+  { execution := referenceSetpointExecution
+  , observation := some 250 }
+
+/--
+Mutation that keeps the exact same GREEN-3-valid execution but provides no
+post-execution observation.
+-/
+def missingObservationOutcome : CandidateOutcome (Fin 256) Nat :=
+  { execution := referenceSetpointExecution
+  , observation := none }
+
+theorem red4_executions_are_identical :
+    referenceObservedOutcome.execution =
+      missingObservationOutcome.execution := by
+  native_decide
+
+theorem red4_observations_are_distinct :
+    referenceObservedOutcome.observation ≠
+      missingObservationOutcome.observation := by
+  native_decide
+
+theorem red4_reference_outcome_passes_green3 :
+    green3OutcomeGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      pvm32SetpointProtocol
+      statusIdentity
+      setpoint25C
+      red3ProtocolTrace
+      referenceObservedOutcome = true := by
+  native_decide
+
+theorem red4_missing_observation_also_passes_green3 :
+    green3OutcomeGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      pvm32SetpointProtocol
+      statusIdentity
+      setpoint25C
+      red3ProtocolTrace
+      missingObservationOutcome = true := by
+  native_decide
+
+/--
+RED-4 result.
+
+The two outcomes contain the same GREEN-3-valid execution but differ in
+post-execution observation. Since GREEN-3 has no observation/effect semantics,
+both pass.
+
+The theorem deliberately does not assert that raw 250 proves the intended
+semantic effect. That relation is exactly what is missing and what GREEN-4 must
+add.
+-/
+theorem red4_green3_is_observation_blind :
+    referenceObservedOutcome.execution =
+      missingObservationOutcome.execution ∧
+    referenceObservedOutcome.observation ≠
+      missingObservationOutcome.observation ∧
+    green3OutcomeGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      pvm32SetpointProtocol
+      statusIdentity
+      setpoint25C
+      red3ProtocolTrace
+      referenceObservedOutcome = true ∧
+    green3OutcomeGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      pvm32SetpointProtocol
+      statusIdentity
+      setpoint25C
+      red3ProtocolTrace
+      missingObservationOutcome = true := by
+  native_decide
+
+end PSL

lean/lakefile.lean

@@ -5,4 +5,4 @@ package «PSL»
 
 @[default_target]
 lean_lib «PSL» where
-  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2, `PSL.SemanticContinuityGreen2, `PSL.SemanticContinuityRed3, `PSL.SemanticContinuityGreen3]
+  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2, `PSL.SemanticContinuityGreen2, `PSL.SemanticContinuityRed3, `PSL.SemanticContinuityGreen3, `PSL.SemanticContinuityRed4]