Cross-Strait Safeguards

Abstract

Conditional cross-strait judgments distinguish unification goals, means, consent, and rights.

Theorem 1.1 (A unification aim does not supply a necessary consent premise).

Lean statement: D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.unification_aim_does_not_replace_consent

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.unification_aim_does_not_replace_consent (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume endorsement requires the freely expressed consent of Taiwan residents. If a proposal serves a unification aim but lacks that consent, it is not endorsed under this standard, and the aim is not a sufficient criterion. The theorem supplies no polling data, historical entitlement, sovereignty ruling, or premise that a particular real proposal lacks consent.

Theorem 1.2 (A failed safeguard excludes endorsement under the stated standard).

Lean statement: D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.failed_cross_strait_safeguard_excludes_endorsement

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.failed_cross_strait_safeguard_excludes_endorsement (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under the explicit premise that endorsement requires peaceful implementation, residents’ consent, and protection of basic rights, failure of any one excludes endorsement. This is a chosen evaluative standard, not a complete definition of international legality or a uniquely proved moral theory. No voting population, threshold, or measurement method is silently fixed.

Theorem 1.3 (The final arrangement alone need not determine endorsement).

Lean statement: D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.unification_outcome_does_not_determine_endorsement

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.unification_outcome_does_not_determine_endorsement (✓ std3). ∎

Source. Repository-derived.

Commentary.

If two proposals lead to one arrangement, one is endorsed, and the other violates a necessary safeguard, endorsement cannot be a function of the arrangement alone. Both the equal-arrangement comparison and the endorsement premise remain explicit. The argument applies the reusable safeguard theorem without independently reproving its factorization step.

References

• Truth anchor: D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.failed_cross_strait_safeguard_excludes_endorsement
• Truth anchor: D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.unification_aim_does_not_replace_consent
• Truth anchor: D5/S3/ConceptDynamics/NormativeRequirements/CrossStraitSafeguards.unification_outcome_does_not_determine_endorsement
• Dependency: D5/S3/ConceptDynamics/NormativeRequirements/NecessarySafeguardObstruction