[splashevolution]

Purpose

Establish the first machine-checked negative result for the new semantic-continuity research line.

The question is:

Can the current PSL realization boundary distinguish a usable target binding from a semantically justified target binding?

At the current baseline, the answer is no.

What this PR adds

• lean/PSL/SemanticContinuityRed1.lean
  • defines an adversarial alternative to the existing reference PVM32 binding;
  • proves the two bindings are distinct;
  • proves both bindings pass the current capability-plus-lowering gate;
  • proves they produce different PVM32 word streams.
• docs/research/RED1_DISHONEST_BINDING.md
  • defines the research question, evidence boundary, GREEN-1 obligation, and kill condition.
• adds RED-1 to the Lean default build and axiom audit;
• updates STATUS.md to mark RED-1 as the active formal milestone.

Important claim boundary

This PR does not claim that 0x20 is physically correct and 0x21 is physically wrong.

The current model cannot state that relationship. That inability is precisely the RED result.

The theorem shows that:

capability declaration + successful lowering
                 ≠
realization correctness

while keeping ordinary CI green.

GREEN-1 constraint

The next step must distinguish reference from adversarial realization without:

• putting the physical address into the target-neutral semantic contract;
• trusting the realization generator;
• modifying the legacy PVM32 semantics just to satisfy the test;
• introducing QEMU/Renode yet.

This is a research falsification checkpoint, not a feature expansion.