[davidwilliam]

Integration test: change only the protected specification, leaving candidate files untouched.

Expected result: the workflow runs and the tree check rejects the changed protected-file hash. The edit is a comment, deliberately demonstrating byte-level lock enforcement without introducing a new behavioral policy. This test PR is not intended to merge.

[github-actions]

ProofForge: payout-flagship REFUTED

REQ-VALID-SUCCEEDS  UNRESOLVED  
REQ-INVALID-NOOP    UNRESOLVED  
REQ-AUTHORIZATION   UNRESOLVED  
REQ-EFFECTS         UNRESOLVED  
REQ-IDEMPOTENCY     UNRESOLVED  
REQ-NONNEGATIVE     UNRESOLVED  
REQ-FAIR-SHARES     REFUTED     witness: account 2: expected 34, got 33
REQ-CONSERVATION    REFUTED     witness: total changed by -1
Executable payout-sidecar: sha256:0fa923b7a14e7ed7  REFUTED (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:1c4e8ca758849079  Passport sha256:4f8cf22e2cf0d240

Reproduce: proofforge verify passport.json --candidate pr/formal

Proof check rejected:

• protected file modified: spec/Payout/Spec.lean

[github-actions]

ProofForge: payout-flagship REFUTED

REQ-VALID-SUCCEEDS  UNRESOLVED  
REQ-INVALID-NOOP    UNRESOLVED  
REQ-AUTHORIZATION   UNRESOLVED  
REQ-EFFECTS         UNRESOLVED  
REQ-IDEMPOTENCY     UNRESOLVED  
REQ-NONNEGATIVE     UNRESOLVED  
REQ-FAIR-SHARES     REFUTED     witness: account 2: expected 34, got 33
REQ-CONSERVATION    REFUTED     witness: total changed by -1
Executable payout-sidecar: sha256:0fa923b7a14e7ed7  REFUTED (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:1c4e8ca758849079  Passport sha256:338fc34d92651817

Reproduce: proofforge verify passport.json --candidate pr/formal

Proof check rejected:

• protected file modified: spec/Payout/Spec.lean

[github-actions]

ProofForge: payout-flagship REFUTED

REQ-VALID-SUCCEEDS  UNRESOLVED  
REQ-INVALID-NOOP    UNRESOLVED  
REQ-AUTHORIZATION   UNRESOLVED  
REQ-EFFECTS         UNRESOLVED  
REQ-IDEMPOTENCY     UNRESOLVED  
REQ-NONNEGATIVE     UNRESOLVED  
REQ-FAIR-SHARES     REFUTED     witness: account 2: expected 34, got 33
REQ-CONSERVATION    REFUTED     witness: total changed by -1
Executable payout-sidecar: sha256:0fa923b7a14e7ed7  REFUTED (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:1c4e8ca758849079  Passport sha256:334cfcf093f13c16

Reproduce: proofforge verify passport.json --candidate pr/formal

Proof check rejected:

• protected file modified: spec/Payout/Spec.lean

[davidwilliam]

Demonstration of the ProofForge pull request check, kept as evidence and closed without merging. The failing check is the intended outcome: the change edits only the protected specification, and the check rejects it. Recorded outcomes: reports/pr-integration/summary.json.

[github-actions]

ProofForge: payout-flagship REFUTED

REQ-VALID-SUCCEEDS  UNRESOLVED  
REQ-INVALID-NOOP    UNRESOLVED  
REQ-AUTHORIZATION   UNRESOLVED  
REQ-EFFECTS         UNRESOLVED  
REQ-IDEMPOTENCY     UNRESOLVED  
REQ-NONNEGATIVE     UNRESOLVED  
REQ-FAIR-SHARES     REFUTED     witness: account 2: expected 34, got 33
REQ-CONSERVATION    REFUTED     witness: total changed by -1
Executable payout-sidecar (linux/amd64): sha256:0fa923b7a14e7ed7  REFUTED (2001 cases + 696 follow-ups); wrapper TESTED_ONLY
Locked manifest sha256:53e32ebeda25c170  Lean v4.35.0  kernels: none
Solution tree sha256:1c4e8ca758849079  Passport sha256:6817fe01633afe91

Counterexamples checked by the kernel:

REQ-FAIR-SHARES     Payout.cex_req_fair_shares : ¬ (FairShares step)  kernels: 6  axioms: Quot.sound, propext  source sha256:a5373f17a01c
REQ-CONSERVATION    Payout.cex_req_conservation : ¬ (Conserves step)  kernels: 6  axioms: Quot.sound, propext  source sha256:ed53148d7dd0

Reproduce: bin/proofforge verify passport.json --candidate pr/formal

Proof check rejected:

• protected file modified: spec/Payout/Spec.lean