[splashevolution]

Purpose

Close RED-2 with the smallest formal addition that distinguishes semantic value from raw target representation.

RED-2 showed that two candidates using the same GREEN-1-correct resource can still carry different raw payloads while both pass the binding checker.

GREEN-2 introduces:

• a target-neutral SemanticQuantity;
• a generic target-specific RepresentationModel(SemanticValue, Raw);
• an executable checkRepresentation relation;
• a composed GREEN-2 gate that requires both resource correctness and representation correctness.

Witness

Target-neutral intent:

25 °C

PVM32 target representation:

Celsius n -> raw n * 10

Therefore:

25 °C -> 250

is derived from target-specific representation semantics rather than embedded in the semantic value.

Machine-checked result

GREEN1(reference raw 250) = true
GREEN1(mutated raw 25)    = true

GREEN2(reference raw 250) = true
GREEN2(mutated raw 25)    = false

The PR also proves generically:

checkRepresentation(model, value, raw) = true
    <->
representationMatches(model, value, raw)

Deliberate limitation

GREEN-2 still does not model protocol state, ordering, ACK/NACK behavior, persistence, atomicity, timing, simulator conformance, or physical-device conformance.

Those remain separate obligations.

Next falsification target

RED-3 should use:

• the correct resource;
• the correct raw payload;
• but an invalid target-state/command sequence.

That will tell us whether protocol/state semantics are actually required next.