Establish semantic-continuity RED-1: binding-blind realization gate

STATUS.md

@@ -55,11 +55,17 @@ They should not be copied into new semantic-continuity modules.
 
 See `docs/TERMINOLOGY_AUDIT.md`.
 
-## Next formal milestone
+## Active formal milestone — RED-1
 
-The next research milestone should establish a RED case where the current
-system cannot distinguish a declared capability from a semantically correct
-realization.
+RED-1 now targets the precise gap between declared capability and realization correctness. The branch \`research/semantic-continuity-red1\` adds a machine-checked counterexample showing that two distinct target bindings for the same semantic script both pass the current capability-plus-lowering gate.
+
+The experiment is intentionally narrower than a device-correctness theorem: the current model cannot yet state why one binding is semantically faithful. That inability is the RED result.
+
+See \`docs/research/RED1_DISHONEST_BINDING.md\`.
+
+The next GREEN step must distinguish correct from adversarial realization without hard-coding a physical address into the target-neutral semantic contract.
+
+The motivating case remains:
 
 Example:
 

docs/research/RED1_DISHONEST_BINDING.md

@@ -0,0 +1,161 @@
+# RED-1 — Binding-Blind Realization Gate
+
+**Branch:** `research/semantic-continuity-red1`  
+**Baseline:** `7317e0a6a1bb8c888dd52f1feed2c23074b4938e`
+
+## Research question
+
+Can the current PSL realization boundary distinguish a target that merely
+provides a usable binding from a target binding that is semantically justified?
+
+The answer at this baseline is **no**.
+
+This is the first controlled RED result for the semantic-continuity research
+line.
+
+## Existing mechanism
+
+The current PVM32 path has two independent pieces:
+
+```text
+DriverContract.supports
+        │
+        ▼
+required capability gate
+
+PVM32Bindings.targetOf
+        │
+        ▼
+target-specific lowering
+```
+
+For `statusScript`, the reference mapping is:
+
+```text
+SemanticId(1001) -> 0x20
+```
+
+Nothing in the current formal model states why `0x20` is the semantically
+correct resource.
+
+## Adversarial witness
+
+RED-1 introduces a second binding:
+
+```text
+SemanticId(1001) -> 0x21
+```
+
+The two mappings are different.
+
+Yet both:
+
+1. satisfy the same capability declaration;
+2. provide a target for lowering;
+3. produce a valid PVM32 word stream.
+
+The resulting words differ:
+
+```text
+reference:   0x200520F0
+adversarial: 0x200521F0
+```
+
+The current architecture has no formal object that can say which target
+behavior actually realizes the semantic identity.
+
+## Machine-checked negative result
+
+`lean/PSL/SemanticContinuityRed1.lean` proves:
+
+```text
+reference binding ≠ adversarial binding
+
+currentRealizationGate(reference, statusScript)   = true
+currentRealizationGate(adversarial, statusScript) = true
+
+lower(reference, statusScript) ≠
+lower(adversarial, statusScript)
+```
+
+This keeps ordinary CI green while proving a negative fact about the current
+design.
+
+RED here means **the desired research property is false of the current
+architecture**, not that the repository intentionally fails to build.
+
+## Claim boundary
+
+This experiment deliberately does **not** prove that physical address
+`0x20` is correct and `0x21` is wrong.
+
+That distinction cannot yet be represented.
+
+Calling `0x21` adversarial is relative to the repository's existing
+reference binding. GREEN-1 must introduce enough target semantics to make
+correctness a formal statement rather than a convention.
+
+## Why this matters
+
+A boolean declaration such as:
+
+```text
+supports(write) = true
+```
+
+can establish only that an operation class is declared available.
+
+It cannot establish:
+
+```text
+semantic identity
+      ↓
+correct target resource
+      ↓
+correct target behavior
+```
+
+Therefore:
+
+> **Capability declaration is not realization correctness.**
+
+That statement is now backed by a checked counterexample in the repository.
+
+## GREEN-1 obligation
+
+GREEN-1 should introduce the **minimum** theory needed to make the reference
+and adversarial cases distinguishable.
+
+Candidate objects are:
+
+```text
+DeviceModel
+Realization
+RealizationEvidence
+RealizationChecker
+Observation
+```
+
+But GREEN-1 should not add all of them merely because they appear in the
+research charter. We should add only what the proof requires.
+
+The acceptance target is:
+
+```text
+reference realization   -> ACCEPT
+adversarial realization -> REJECT
+```
+
+without:
+
+- placing target address `0x20` inside the target-neutral semantic contract;
+- trusting the realization generator;
+- modifying the historical PVM32 semantics to make the test pass;
+- introducing QEMU/Renode yet;
+- making a claim about physical hardware.
+
+## Kill condition
+
+If rejecting the adversarial binding requires hard-coding the expected
+physical address into the semantic contract, then the proposed continuity
+boundary has failed its first abstraction test.

lean/Audit.lean

@@ -1,9 +1,13 @@
 import PSL.Semantics
 import PSL.PVM32Driver
+import PSL.SemanticContinuityRed1
 
 #print axioms validateIRClosed_sound
 #print axioms validateWords_execution
 #print axioms validated_ir_executes
 #print axioms valid_program_executes
 #print axioms certified_ir_executes
 #print axioms PSL.status_script_realizes_on_pvm32
+
+#print axioms PSL.red1_bindings_are_distinct
+#print axioms PSL.red1_capability_gate_is_binding_blind

lean/PSL/SemanticContinuityRed1.lean

@@ -0,0 +1,79 @@
+import PSL.PVM32Driver
+
+namespace PSL
+
+/-
+  Semantic Continuity RED-1
+  -------------------------
+
+  Purpose:
+  exhibit a machine-checked counterexample to the idea that the current
+  capability gate establishes realization correctness.
+
+  The existing model can check whether a script requires WRITE and whether the
+  PVM32 driver declares WRITE support. It can also lower any supplied
+  SemanticId -> target-byte binding.
+
+  What it cannot express is why one supplied binding is semantically faithful
+  and another is not.
+
+  This file deliberately does NOT introduce the missing device model or
+  realization-proof machinery. It records the gap we want GREEN-1 to close.
+-/
+
+/-- An adversarial alternative to the existing reference binding.
+
+Both bindings are total enough for statusScript to lower. The current core has
+no semantic relation capable of preferring 0x20 over 0x21.
+-/
+def adversarialPVM32Bindings : PVM32Bindings :=
+  { targetOf := fun id =>
+      if id == statusIdentity then some (fin256 0x21) else none }
+
+/--
+Characterize the acceptance boundary that exists today:
+  1. the driver declares the script's required capabilities, and
+  2. lowering succeeds for the supplied target binding.
+
+This is an observation of the current architecture, not the desired future
+definition of realization correctness.
+-/
+def currentRealizationGate
+    (bindings : PVM32Bindings) (script : SemanticScript) : Bool :=
+  pvm32Driver.acceptsScript script &&
+    (pvm32LowerScript? bindings script).isSome
+
+theorem red1_bindings_are_distinct :
+    referencePVM32Bindings.targetOf statusIdentity ≠
+      adversarialPVM32Bindings.targetOf statusIdentity := by
+  native_decide
+
+theorem red1_reference_binding_lowers :
+    pvm32Words? referencePVM32Bindings statusScript =
+      some [0x200520F0] := by
+  native_decide
+
+theorem red1_adversarial_binding_also_lowers :
+    pvm32Words? adversarialPVM32Bindings statusScript =
+      some [0x200521F0] := by
+  native_decide
+
+/--
+RED-1 result.
+
+Two distinct target bindings for the same semantic script both pass the entire
+acceptance boundary available today, even though they produce different target
+programs.
+
+The theorem does NOT assert which target byte is physically correct. That fact
+cannot be stated in the current model. The inability to state and check that
+relationship is exactly the research gap.
+-/
+theorem red1_capability_gate_is_binding_blind :
+    currentRealizationGate referencePVM32Bindings statusScript = true ∧
+    currentRealizationGate adversarialPVM32Bindings statusScript = true ∧
+    pvm32Words? referencePVM32Bindings statusScript ≠
+      pvm32Words? adversarialPVM32Bindings statusScript := 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]
+  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1]