Adjudication-Signature Sufficiency and Its Target-Laundering Failure

Abstract

The four-coordinate adjudication signature preserves non-anticipation, admissible judging, and scientific gain, but not target laundering’s whole-commitment report identity.

Theorem 1.1 (OP1-NA: equal signatures preserve non-anticipation).

$$\left(\mathrm{adjudicationSignature}\left(Z,L,K,v\right)=\mathrm{adjudicationSignature}\left(Z,R,J,w\right)\wedge \mathrm{SameOutNA}\left(Z,z\right)\right)\Rightarrow \left(\mathrm{NonAnticipating}\left(K,z\right)\iff \mathrm{NonAnticipating}\left(J,z\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.non_anticipating_signature_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a common record in the finite history, equality of the decision-visible, freeze-visible, and directly contaminated coordinates transports each conjunct of NonAnticipating in both directions.

Theorem 1.2 (OP1-AJ: equal signatures preserve admissible judging).

$$\left(\mathrm{adjudicationSignature}\left(Z,L,K,v\right)=\mathrm{adjudicationSignature}\left(Z,R,J,w\right)\wedge \mathrm{SameOutAJ}\left(Z,r\right)\right)\Rightarrow \left(\mathrm{AdmissibleJudge}\left(L,K,v,r\right)\iff \mathrm{AdmissibleJudge}\left(R,J,w,r\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.admissible_judge_signature_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

The fourth coordinate records existence of adjudicate events and of each generate, tune, or select event together with its dependency-closure touch bit. It therefore transports both the positive role requirement and the negated adaptive-contamination requirement.

Theorem 1.3 (OP1-SG: equal signatures preserve scientific gain).

$$\left(\mathrm{adjudicationSignature}\left(Z,L,\mathrm{adjudication}\left(K\right),v\right)=\mathrm{adjudicationSignature}\left(Z,R,\mathrm{adjudication}\left(J\right),w\right)\wedge \mathrm{SameOutSG}\left(Z,z,K,J\right)\right)\Rightarrow \left(\mathrm{ScientificGain}\left(E,K,z,a,b\right)\iff \mathrm{ScientificGain}\left(E,J,z,a,b\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.scientific_gain_signature_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

SameOutSG fixes the committed and baseline action sets and the comparator. The only remaining history-dependent conjunct is NonAnticipating, which is supplied by OP1-NA.

Theorem 1.4 (OP1-TL: equal signatures do not preserve target laundering).

$$\exists Z\in \mathrm{Finset}\left(\mathrm{Bool}\left(\right)\right),K\in \mathrm{Commitment}\left(\right),N\in \mathrm{Commitment}\left(\right),J\in \mathrm{Commitment}\left(\right),M\in \mathrm{Commitment}\left(\right),L\in \mathrm{Ledger}\left(\right),R\in \mathrm{Ledger}\left(\right),P\in \mathrm{Ledger}\left(\right),Q\in \mathrm{Ledger}\left(\right),v\in \mathrm{ValidTrace}\left(L,\mathrm{adjudication}\left(K\right)\right),w\in \mathrm{ValidTrace}\left(R,\mathrm{adjudication}\left(N\right)\right),x\in \mathrm{ValidTrace}\left(P,\mathrm{adjudication}\left(J\right)\right),y\in \mathrm{ValidTrace}\left(Q,\mathrm{adjudication}\left(M\right)\right),E\in \mathrm{Commitment}\left(\right)\to \left(\mathrm{Bool}\left(\right)\to \mathrm{Unit}\left(\right)\right),T\in \mathrm{RegradeReport}\left(\mathrm{Commitment}\left(\right),\mathrm{Bool}\left(\right),\mathrm{Unit}\left(\right),\mathrm{Bool}\left(\right),E\right),\mathrm{adjudicationSignature}\left(Z,L,\mathrm{adjudication}\left(K\right),v\right)=\mathrm{adjudicationSignature}\left(Z,P,\mathrm{adjudication}\left(J\right),x\right)\wedge \left(\mathrm{adjudicationSignature}\left(Z,R,\mathrm{adjudication}\left(N\right),w\right)=\mathrm{adjudicationSignature}\left(Z,Q,\mathrm{adjudication}\left(M\right),y\right)\wedge \left(\mathrm{SameOutTL}\left(Z,true,K,N,J,M\right)\wedge \left(\mathrm{SketchTargetLaundering}\left(E,K,N,true,T\right)\wedge \left(\neg \mathrm{SketchTargetLaundering}\left(E,J,M,true,T\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.target_laundering_signature_counterexample (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite witness uses Boolean event, evidence, artifact, and time types with empty valid role ledgers. The two new commitments differ only in adjudication.frozenAt; all four signature coordinates and all commitment fields outside adjudication are equal.

The common report names the first new commitment as its revised object. SketchTargetLaundering is true on that side, but the same report cannot also name the second, unequal commitment. The omitted frozenAt field separately changes the timestamp identity as well.

SketchTargetLaundering is the frozen Lean name for the no-arrival target-laundering interface used by Part 55; the distinct prose-level TargetLaundering declaration has an additional arrival argument.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.admissible_judge_signature_sufficiency
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.non_anticipating_signature_sufficiency
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.scientific_gain_signature_sufficiency
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeSignatures/AdjudicationSignatureSufficiency.target_laundering_signature_counterexample
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/RoleLedgerPrefixStability
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeLaws/ScientificGainGeneralizationReversal