Establish RED-2: representation-blind binding correctness

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-1
+## Active formal milestone — RED-2
 
 RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate.
 
@@ -65,7 +65,13 @@ See \`docs/research/RED1_DISHONEST_BINDING.md\` and \`docs/research/GREEN1_DEVIC
 
 This closes only binding correctness relative to a stated device model. Representation, units, protocol state, persistence, failure handling, and physical-device conformance remain open.
 
-The next falsification target is the same physical resource with a wrong representation:
+RED-2 now freezes the GREEN-1-correct resource binding and mutates only the target payload. A machine-checked witness shows that both raw values pass the GREEN-1 binding checker because representation is outside its model.
+
+See \`docs/research/RED2_REPRESENTATION_BLINDNESS.md\`.
+
+This establishes the next narrow gap: **binding correctness is not representation correctness**.
+
+The motivating case is:
 
 Example:
 
@@ -79,10 +85,9 @@ correct:
   ACK observed
 
 incorrect:
-  write 25
-  wrong resource
-  wrong unit
-  missing state transition
+  encode 25.0 as 25
+  correct resource
+  representation mismatch
 ```
 
 The new theory should reject incorrect realizations because of behavior, not

docs/research/RED2_REPRESENTATION_BLINDNESS.md

@@ -0,0 +1,149 @@
+# RED-2 — Representation-Blind Binding Check
+
+**Branch:** `research/semantic-continuity-red2`  
+**Baseline:** `ebb21af2489e3a05a2fb17f6bb67657f7bba813e`
+
+## Research question
+
+After GREEN-1, can PSL distinguish two realizations that use the **same correct
+resource binding** but carry **different raw representations**?
+
+At this baseline, the answer is **no**.
+
+## Why RED-2 is different from RED-1
+
+RED-1 changed the physical resource:
+
+```text
+reference:   SemanticId(1001) -> 0x20
+adversarial: SemanticId(1001) -> 0x21
+```
+
+GREEN-1 fixed that gap by independently modeling what each target resource
+denotes.
+
+RED-2 holds the resource fixed:
+
+```text
+resource: 0x20
+```
+
+and mutates only the target payload:
+
+```text
+reference raw value: 250
+mutated raw value:    25
+```
+
+The intended motivating interpretation is a 25.0 °C setpoint on a legacy
+fixed-point target, but RED-2 does not yet formalize that interpretation.
+
+## Machine-checked negative result
+
+`lean/PSL/SemanticContinuityRed2.lean` introduces a minimal:
+
+```text
+CandidateWrite(Resource)
+  resource
+  rawValue
+```
+
+and proves:
+
+```text
+reference.resource = mutated.resource
+reference.rawValue != mutated.rawValue
+
+GREEN1(reference) = true
+GREEN1(mutated)   = true
+```
+
+This is enough to establish the next gap:
+
+> **Binding correctness is not representation correctness.**
+
+## Important claim boundary
+
+RED-2 does **not** prove that raw value `250` is semantically correct or that
+`25` is semantically wrong.
+
+The current theory cannot express that relationship.
+
+The words "reference" and "wrong-scale" describe the experiment setup relative
+to the planned 25.0 °C witness. GREEN-2 must introduce enough representation
+semantics to turn that convention into a formal statement.
+
+## What GREEN-1 can see
+
+GREEN-1 checks:
+
+```text
+semantic identity
+      |
+      v
+target resource
+      |
+      v
+device-model denotation
+```
+
+For both RED-2 candidates:
+
+```text
+SemanticId(1001)
+      |
+      v
+0x20
+      |
+      v
+SemanticId(1001)
+```
+
+So both correctly pass.
+
+## What GREEN-1 cannot see
+
+It has no relation for:
+
+```text
+semantic value
+      |
+      v
+target representation
+      |
+      v
+raw payload
+```
+
+Therefore changing only the payload is invisible to the checker.
+
+## GREEN-2 obligation
+
+GREEN-2 should add the **minimum** semantics required to state and check a
+representation relation.
+
+The acceptance target is:
+
+```text
+same resource 0x20
+
+reference representation -> ACCEPT
+mutated representation   -> REJECT
+```
+
+without:
+
+- hard-coding raw value `250` into a supposedly target-neutral contract;
+- trusting the realization generator;
+- conflating resource binding with representation;
+- adding protocol-state machinery before it is required;
+- introducing QEMU/Renode yet.
+
+A likely next object is a target-specific representation model or encoder
+relation, but RED-2 intentionally does not prescribe its final shape.
+
+## Kill condition
+
+If representation correctness can only be obtained by embedding the target's
+raw encoding directly in the semantic contract, then the abstraction boundary
+has failed and should be redesigned.

lean/Audit.lean

@@ -2,6 +2,7 @@ import PSL.Semantics
 import PSL.PVM32Driver
 import PSL.SemanticContinuityRed1
 import PSL.SemanticContinuityGreen1
+import PSL.SemanticContinuityRed2
 
 #print axioms validateIRClosed_sound
 #print axioms validateWords_execution
@@ -16,3 +17,6 @@ import PSL.SemanticContinuityGreen1
 #print axioms PSL.checkBinding_true_iff
 #print axioms PSL.green1_separates_red1_witness
 #print axioms PSL.green1_checked_binding_is_model_faithful
+
+#print axioms PSL.red2_same_resource
+#print axioms PSL.red2_green1_is_representation_blind

lean/PSL/SemanticContinuityRed2.lean

@@ -0,0 +1,128 @@
+import PSL.SemanticContinuityGreen1
+
+namespace PSL
+
+/-
+  Semantic Continuity RED-2
+  -------------------------
+
+  GREEN-1 established binding correctness relative to an independently stated
+  DeviceModel.
+
+  RED-2 asks whether that boundary also establishes representation correctness.
+
+  It does not.
+
+  Two candidate writes may select the same semantically correct resource while
+  carrying different raw payloads. The GREEN-1 checker inspects only the
+  resource binding, so both candidates pass.
+
+  This file deliberately does NOT introduce representation semantics. It
+  records the next missing relation.
+-/
+
+/--
+A minimal target-side write candidate used only for RED-2.
+
+The resource and raw payload are separated explicitly so the theorem can show
+which field GREEN-1 observes and which field it ignores.
+-/
+structure CandidateWrite (Resource : Type) where
+  resource : Resource
+  rawValue : Nat
+  deriving Repr, BEq, DecidableEq
+
+/--
+Turn one concrete candidate into the single semantic binding needed by the
+GREEN-1 checker.
+
+The raw payload is intentionally absent because GREEN-1 has no representation
+semantics.
+-/
+def CandidateWrite.resourceOf
+    {Resource : Type}
+    (semanticId : SemanticId)
+    (candidate : CandidateWrite Resource) :
+    SemanticId → Option Resource :=
+  fun id => if id == semanticId then some candidate.resource else none
+
+/--
+The strongest GREEN-1 gate available for one explicit write candidate:
+binding agreement with the independently stated device model.
+-/
+def green1CandidateGate
+    {Resource : Type}
+    (device : DeviceModel Resource)
+    (semanticId : SemanticId)
+    (candidate : CandidateWrite Resource) : Bool :=
+  checkBinding
+    device
+    (candidate.resourceOf semanticId)
+    semanticId
+
+/--
+Reference encoding for the next falsification experiment.
+
+At RED-2 this is only an experimental reference payload. The current theory
+does not yet state why 250 represents the desired semantic value.
+-/
+def referenceSetpointWrite : CandidateWrite (Fin 256) :=
+  { resource := fin256 0x20
+  , rawValue := 250 }
+
+/--
+Wrong-scale mutation of the same target resource.
+
+Again, RED-2 does not yet prove that 25 is semantically wrong. It proves that
+GREEN-1 cannot distinguish it from the reference payload.
+-/
+def wrongScaleSetpointWrite : CandidateWrite (Fin 256) :=
+  { resource := fin256 0x20
+  , rawValue := 25 }
+
+theorem red2_same_resource :
+    referenceSetpointWrite.resource =
+      wrongScaleSetpointWrite.resource := by
+  native_decide
+
+theorem red2_payloads_are_distinct :
+    referenceSetpointWrite.rawValue ≠
+      wrongScaleSetpointWrite.rawValue := by
+  native_decide
+
+theorem red2_reference_passes_green1 :
+    green1CandidateGate
+      pvm32Green1DeviceModel
+      statusIdentity
+      referenceSetpointWrite = true := by
+  native_decide
+
+theorem red2_wrong_scale_also_passes_green1 :
+    green1CandidateGate
+      pvm32Green1DeviceModel
+      statusIdentity
+      wrongScaleSetpointWrite = true := by
+  native_decide
+
+/--
+RED-2 result.
+
+The two candidates select the same resource and therefore both satisfy the
+GREEN-1 binding relation, even though their raw payloads differ.
+
+The theorem deliberately does not claim which payload realizes the intended
+semantic value. That relation is exactly what is missing.
+-/
+theorem red2_green1_is_representation_blind :
+    referenceSetpointWrite.rawValue ≠ wrongScaleSetpointWrite.rawValue ∧
+    green1CandidateGate
+      pvm32Green1DeviceModel
+      statusIdentity
+      referenceSetpointWrite = true ∧
+    green1CandidateGate
+      pvm32Green1DeviceModel
+      statusIdentity
+      wrongScaleSetpointWrite = 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]
+  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2]