From 63334508f7ba5a8b54121845712b9861cd8eba84 Mon Sep 17 00:00:00 2001
From: pravkr <121178833+splashevolution@users.noreply.github.com>
Date: Wed, 7 Oct 2026 20:21:56 +0530
Subject: [PATCH 1/2] Close GREEN-2 with target-specific representation
 checking

---
 STATUS.md                                    |  17 +-
 docs/research/GREEN2_REPRESENTATION_CHECK.md | 189 +++++++++++++++++++
 lean/Audit.lean                              |   5 +
 lean/PSL/SemanticContinuityGreen2.lean       | 184 ++++++++++++++++++
 lean/lakefile.lean                           |   2 +-
 5 files changed, 391 insertions(+), 6 deletions(-)
 create mode 100644 docs/research/GREEN2_REPRESENTATION_CHECK.md
 create mode 100644 lean/PSL/SemanticContinuityGreen2.lean

diff --git a/STATUS.md b/STATUS.md
index 5ce5421..d14f231 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -55,7 +55,7 @@ They should not be copied into new semantic-continuity modules.
 
 See `docs/TERMINOLOGY_AUDIT.md`.
 
-## Active formal milestone — RED-2
+## Active formal milestone — GREEN-2
 
 RED-1 established that two distinct target bindings for the same semantic script both pass the capability-plus-lowering gate.
 
@@ -69,7 +69,15 @@ RED-2 now freezes the GREEN-1-correct resource binding and mutates only the targ
 
 See \`docs/research/RED2_REPRESENTATION_BLINDNESS.md\`.
 
-This establishes the next narrow gap: **binding correctness is not representation correctness**.
+This established the next narrow gap: **binding correctness is not representation correctness**.
+
+GREEN-2 adds a generic target-specific \`RepresentationModel(SemanticValue, Raw)\` plus an executable representation checker. The target-neutral witness states 25 °C; the PVM32 model independently defines Celsius as fixed-point ×10, so raw 250 is derived at the target boundary rather than embedded in the semantic value.
+
+The composed GREEN-2 gate accepts the reference candidate and rejects the RED-2 wrong-scale candidate while preserving the GREEN-1 resource check.
+
+See \`docs/research/GREEN2_REPRESENTATION_CHECK.md\`.
+
+Protocol state, ordering, acknowledgements, persistence, and physical-device conformance remain open.
 
 The motivating case is:
 
@@ -85,9 +93,8 @@ correct:
   ACK observed
 
 incorrect:
-  encode 25.0 as 25
-  correct resource
-  representation mismatch
+  write 250 to the correct resource
+  but omit required configuration/state transitions
 ```
 
 The new theory should reject incorrect realizations because of behavior, not
diff --git a/docs/research/GREEN2_REPRESENTATION_CHECK.md b/docs/research/GREEN2_REPRESENTATION_CHECK.md
new file mode 100644
index 0000000..125ecc1
--- /dev/null
+++ b/docs/research/GREEN2_REPRESENTATION_CHECK.md
@@ -0,0 +1,189 @@
+# GREEN-2 — Target-Specific Representation Check
+
+**Branch:** `research/semantic-continuity-green2`  
+**Baseline:** `39dced4cb4a10fc7730eef06afeae474049a94b7`
+
+## Result
+
+GREEN-2 closes the exact representation gap demonstrated by RED-2.
+
+RED-2 established:
+
+```text
+binding correctness
+        !=
+representation correctness
+```
+
+because two candidates used the same GREEN-1-correct resource while carrying
+different raw values:
+
+```text
+resource = 0x20
+
+reference raw = 250
+mutated raw   = 25
+```
+
+GREEN-1 accepted both because it checked only resource denotation.
+
+GREEN-2 adds one missing formal object:
+
+```text
+RepresentationModel(SemanticValue, Raw)
+    encode : SemanticValue -> Option Raw
+```
+
+and one executable relation:
+
+```text
+checkRepresentation(model, semanticValue, raw)
+```
+
+## Target-neutral value
+
+The witness now states the intended value independently of the target:
+
+```text
+setpoint25C:
+    magnitude = 25
+    unit      = Celsius
+```
+
+There is no PVM32 address, fixed-point scale, or raw value in this semantic
+quantity.
+
+## Target-specific representation
+
+The PVM32 representation model states:
+
+```text
+Celsius magnitude n -> raw n * 10
+Fahrenheit           -> unsupported
+```
+
+Therefore:
+
+```text
+25 °C -> 250
+```
+
+is derived from target-specific representation semantics rather than copied
+into the target-neutral value.
+
+## Machine-checked result
+
+`lean/PSL/SemanticContinuityGreen2.lean` proves:
+
+```text
+GREEN1(reference) = true
+GREEN1(mutated)   = true
+
+Representation(reference raw 250) = true
+Representation(mutated raw 25)    = false
+
+GREEN2(reference) = true
+GREEN2(mutated)   = false
+```
+
+It also proves generically:
+
+```text
+checkRepresentation(model, value, raw) = true
+    <->
+representationMatches(model, value, raw)
+```
+
+So the executable checker is sound and complete for the representation
+relation GREEN-2 actually states.
+
+## Separation of concerns
+
+GREEN-2 keeps two target obligations distinct:
+
+```text
+semantic identity
+      |
+      v
+DeviceModel
+      |
+      v
+target resource
+
+semantic value
+      |
+      v
+RepresentationModel
+      |
+      v
+raw payload
+```
+
+A candidate must satisfy both.
+
+This matters because a correct address with an incorrect payload is still an
+incorrect realization.
+
+## What GREEN-2 does not prove
+
+GREEN-2 is still **not** full realization soundness.
+
+It does not yet model:
+
+- required configuration/privilege state;
+- command ordering;
+- ACK/NACK semantics;
+- persistence;
+- atomicity;
+- timing;
+- simulator conformance;
+- physical-device conformance.
+
+The `DeviceModel` and `RepresentationModel` are stated model assumptions.
+Future evidence must justify their relationship to executable and physical
+targets.
+
+## Why this remains minimal
+
+GREEN-2 does not introduce traces, protocol automata, realization certificates,
+or virtual hardware.
+
+RED-2 required only one missing distinction: semantic value versus raw target
+representation.
+
+Adding protocol theory now would solve a problem that has not yet been
+machine-demonstrated.
+
+## Next falsification target
+
+The natural RED-3 is:
+
+> use the correct resource **and** the correct raw representation, but violate
+> a required target state transition or command sequence.
+
+For example:
+
+```text
+semantic intent: SetSetpoint(25 °C)
+
+correct:
+    enter-config
+    write 250 -> 0x20
+    observe ACK
+    exit-config
+
+mutated:
+    write 250 -> 0x20
+```
+
+GREEN-2 should accept both if it has no protocol-state semantics.
+
+That would justify the next layer rather than assuming it in advance.
+
+## Kill condition retained
+
+If representation correctness requires raw target values to appear in the
+target-neutral semantic value itself, the abstraction boundary has failed.
+
+GREEN-2 avoids that: raw `250` is derived by the target-specific
+representation model.
diff --git a/lean/Audit.lean b/lean/Audit.lean
index e7011b6..0404000 100644
--- a/lean/Audit.lean
+++ b/lean/Audit.lean
@@ -3,6 +3,7 @@ import PSL.PVM32Driver
 import PSL.SemanticContinuityRed1
 import PSL.SemanticContinuityGreen1
 import PSL.SemanticContinuityRed2
+import PSL.SemanticContinuityGreen2
 
 #print axioms validateIRClosed_sound
 #print axioms validateWords_execution
@@ -20,3 +21,7 @@ import PSL.SemanticContinuityRed2
 
 #print axioms PSL.red2_same_resource
 #print axioms PSL.red2_green1_is_representation_blind
+
+#print axioms PSL.checkRepresentation_true_iff
+#print axioms PSL.green2_separates_red2_witness
+#print axioms PSL.green2_checked_representation_is_model_faithful
diff --git a/lean/PSL/SemanticContinuityGreen2.lean b/lean/PSL/SemanticContinuityGreen2.lean
new file mode 100644
index 0000000..af77bf5
--- /dev/null
+++ b/lean/PSL/SemanticContinuityGreen2.lean
@@ -0,0 +1,184 @@
+import PSL.SemanticContinuityRed2
+
+namespace PSL
+
+/-
+  Semantic Continuity GREEN-2
+  ---------------------------
+
+  RED-2 showed that GREEN-1 binding correctness is blind to raw
+  representation. Two candidates can select the same semantically correct
+  resource while carrying different payloads.
+
+  GREEN-2 adds the minimum missing relation: a target-specific representation
+  model that independently maps a target-neutral semantic value to a raw
+  target representation.
+
+  This closes only the RED-2 representation gap. It does NOT yet model
+  protocol state, ordering, acknowledgements, persistence, atomicity, timing,
+  or physical-device conformance.
+-/
+
+/-- Target-neutral units needed by the current witness. -/
+inductive SemanticUnit where
+  | celsius
+  | fahrenheit
+  deriving Repr, BEq, DecidableEq
+
+/--
+A minimal target-neutral semantic quantity.
+
+Magnitude is expressed in whole semantic units for the current witness. The
+target representation may choose any scaling or encoding.
+-/
+structure SemanticQuantity where
+  magnitude : Nat
+  unit      : SemanticUnit
+  deriving Repr, BEq, DecidableEq
+
+/--
+Target-specific representation semantics.
+
+The semantic value type and raw target type are parameters so future hardware
+generations may choose different target encodings without changing the
+target-neutral value.
+-/
+structure RepresentationModel (SemanticValue Raw : Type) where
+  encode : SemanticValue → Option Raw
+
+/--
+A raw payload matches the target representation model when the independent
+model encodes the semantic value to exactly that payload.
+-/
+def representationMatches
+    {SemanticValue Raw : Type}
+    (model : RepresentationModel SemanticValue Raw)
+    (value : SemanticValue)
+    (raw : Raw) : Prop :=
+  model.encode value = some raw
+
+/-- Executable representation checker. -/
+def checkRepresentation
+    {SemanticValue Raw : Type}
+    [DecidableEq Raw]
+    (model : RepresentationModel SemanticValue Raw)
+    (value : SemanticValue)
+    (raw : Raw) : Bool :=
+  decide (model.encode value = some raw)
+
+/--
+The executable checker is sound and complete for the representation relation
+that GREEN-2 actually claims.
+-/
+theorem checkRepresentation_true_iff
+    {SemanticValue Raw : Type}
+    [DecidableEq Raw]
+    (model : RepresentationModel SemanticValue Raw)
+    (value : SemanticValue)
+    (raw : Raw) :
+    checkRepresentation model value raw = true ↔
+      representationMatches model value raw := by
+  simp [checkRepresentation, representationMatches]
+
+/--
+The target-neutral value used by the RED-2 / GREEN-2 witness.
+
+No PVM32 address, scaling factor, or raw payload appears here.
+-/
+def setpoint25C : SemanticQuantity :=
+  { magnitude := 25
+  , unit := .celsius }
+
+/--
+PVM32 target-specific representation model for the witness.
+
+This target represents supported Celsius values as fixed-point ×10. Fahrenheit
+is intentionally unsupported in this minimal model.
+
+The scaling factor belongs here, at the target representation boundary.
+-/
+def pvm32SetpointRepresentation :
+    RepresentationModel SemanticQuantity Nat :=
+  { encode := fun value =>
+      match value.unit with
+      | .celsius    => some (value.magnitude * 10)
+      | .fahrenheit => none }
+
+/--
+Compose GREEN-1 resource correctness with GREEN-2 representation correctness.
+
+The resource and representation checks remain separate: binding correctness
+does not imply representation correctness, and vice versa.
+-/
+def green2CandidateGate
+    {Resource SemanticValue : Type}
+    (device : DeviceModel Resource)
+    (representation : RepresentationModel SemanticValue Nat)
+    (semanticId : SemanticId)
+    (semanticValue : SemanticValue)
+    (candidate : CandidateWrite Resource) : Bool :=
+  green1CandidateGate device semanticId candidate &&
+    checkRepresentation representation semanticValue candidate.rawValue
+
+theorem green2_reference_representation_accepts :
+    checkRepresentation
+      pvm32SetpointRepresentation
+      setpoint25C
+      referenceSetpointWrite.rawValue = true := by
+  native_decide
+
+theorem green2_wrong_scale_representation_rejects :
+    checkRepresentation
+      pvm32SetpointRepresentation
+      setpoint25C
+      wrongScaleSetpointWrite.rawValue = false := by
+  native_decide
+
+/--
+GREEN-2 closes exactly the RED-2 witness:
+
+* both candidates still use the same GREEN-1-correct resource;
+* the target representation model maps semantic 25 °C to raw 250;
+* the composed checker accepts the reference candidate;
+* the same checker rejects the wrong-scale candidate.
+-/
+theorem green2_separates_red2_witness :
+    red2_same_resource ∧
+    green1CandidateGate
+      pvm32Green1DeviceModel
+      statusIdentity
+      referenceSetpointWrite = true ∧
+    green1CandidateGate
+      pvm32Green1DeviceModel
+      statusIdentity
+      wrongScaleSetpointWrite = true ∧
+    green2CandidateGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      statusIdentity
+      setpoint25C
+      referenceSetpointWrite = true ∧
+    green2CandidateGate
+      pvm32Green1DeviceModel
+      pvm32SetpointRepresentation
+      statusIdentity
+      setpoint25C
+      wrongScaleSetpointWrite = false := by
+  native_decide
+
+/--
+Any payload accepted by checkRepresentation satisfies the stated target
+representation relation. The realization generator itself is not trusted for
+that claim.
+-/
+theorem green2_checked_representation_is_model_faithful
+    {SemanticValue Raw : Type}
+    [DecidableEq Raw]
+    (model : RepresentationModel SemanticValue Raw)
+    (value : SemanticValue)
+    (raw : Raw)
+    (hcheck : checkRepresentation model value raw = true) :
+    representationMatches model value raw :=
+  (checkRepresentation_true_iff model value raw).mp hcheck
+
+end PSL
diff --git a/lean/lakefile.lean b/lean/lakefile.lean
index 7566b91..d07ceec 100644
--- a/lean/lakefile.lean
+++ b/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]
+  roots := #[`PSL.SemanticKernel, `PSL.Semantics, `PSL.PVM32Driver, `PSL.SemanticContinuityRed1, `PSL.SemanticContinuityGreen1, `PSL.SemanticContinuityRed2, `PSL.SemanticContinuityGreen2]

From 539ef1439ab33e0670f937442b8de875e2f7e156 Mon Sep 17 00:00:00 2001
From: pravkr <121178833+splashevolution@users.noreply.github.com>
Date: Wed, 7 Oct 2026 20:25:04 +0530
Subject: [PATCH 2/2] Fix GREEN-2 conjunction proposition

---
 lean/PSL/SemanticContinuityGreen2.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lean/PSL/SemanticContinuityGreen2.lean b/lean/PSL/SemanticContinuityGreen2.lean
index af77bf5..be5d810 100644
--- a/lean/PSL/SemanticContinuityGreen2.lean
+++ b/lean/PSL/SemanticContinuityGreen2.lean
@@ -143,7 +143,8 @@ GREEN-2 closes exactly the RED-2 witness:
 * the same checker rejects the wrong-scale candidate.
 -/
 theorem green2_separates_red2_witness :
-    red2_same_resource ∧
+    referenceSetpointWrite.resource =
+      wrongScaleSetpointWrite.resource ∧
     green1CandidateGate
       pvm32Green1DeviceModel
       statusIdentity