Diagonal Escape Needs Type Extension

Abstract

Six countermodels separate four closure notions, including degenerate carriers.

Theorem 1.1 (Faithfulness does not equal representation surjectivity).

$$\mathrm{StateFaithfulness}\left(idBool\right)\wedge \neg \mathrm{RepresentationSurjectivity}\left(constFalse\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.state_faithfulness_not_representation_surjectivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Use identity as the Boolean readout and the constant-false map as the representation. Identity distinguishes states, while true has no representing coordinate under the constant map.

Theorem 1.2 (Effective descent does not equal state faithfulness).

$$\mathrm{EffectiveDescent}\left(constFalse,idBool\right)\wedge \neg \mathrm{StateFaithfulness}\left(constFalse\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.effective_descent_not_state_faithfulness (✓ std3). ∎

Source. Repository-derived.

Commentary.

A constant Boolean readout identifies false and true, so it is not faithful. Identity dynamics preserve its sole realized fiber and therefore descend effectively to the realized image.

Theorem 1.3 (State faithfulness does not equal self-description closure).

$$\mathrm{StateFaithfulness}\left(idBool\right)\wedge \neg \mathrm{SelfDescriptionClosure}\left(Bool\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.state_faithfulness_not_self_description_closure (✓ std3). ∎

Source. Repository-derived.

Commentary.

Boolean identity is injective. A surjective Boolean evaluator would, by Lawvere diagonalization, give Boolean negation a fixed point; case analysis refutes that fixed point.

Theorem 1.4 (Effective descent does not equal representation surjectivity).

$$\mathrm{EffectiveDescent}\left(idBool,idBool\right)\wedge \neg \mathrm{RepresentationSurjectivity}\left(constFalse\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.effective_descent_not_representation_surjectivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Identity Boolean dynamics descend along identity readout. The separate constant-false representation still omits the true state, showing that dynamic closure does not supply representation coverage.

Theorem 1.5 (Representation surjectivity does not equal self-description closure).

$$\mathrm{RepresentationSurjectivity}\left(idBool\right)\wedge \neg \mathrm{SelfDescriptionClosure}\left(Bool\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.representation_surjectivity_not_self_description_closure (✓ std3). ∎

Source. Repository-derived.

Commentary.

Boolean identity represents both states, but the carrier cannot encode all four Boolean endomaps. The formal contradiction again uses the fixed-point consequence of a surjective evaluator.

Theorem 1.6 (Effective descent does not equal self-description closure).

$$\mathrm{EffectiveDescent}\left(idBool,notBool\right)\wedge \neg \mathrm{SelfDescriptionClosure}\left(Bool\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.effective_descent_not_self_description_closure (✓ std3). ∎

Source. Repository-derived.

Commentary.

Boolean negation descends along identity readout because every identity fiber is preserved. This does not create an internal enumeration of all Boolean endomaps.

Theorem 1.7 (The empty carrier separates typed maps from self-description).

$$\mathrm{StateFaithfulness}\left(idEmpty\right)\wedge \mathrm{RepresentationSurjectivity}\left(idEmpty\right)\wedge \mathrm{EffectiveDescent}\left(idEmpty,idEmpty\right)\wedge \neg \mathrm{SelfDescriptionClosure}\left(Empty\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.empty_degenerate_audit (✓ std3). ∎

Source. Repository-derived.

Commentary.

On Empty, identity injectivity and surjectivity are vacuous and identity dynamics descend. Self-description fails because the unique empty endomap has no code in an empty code type.

Theorem 1.8 (The singleton carrier satisfies all four notions).

$$\mathrm{StateFaithfulness}\left(idUnit\right)\wedge \mathrm{RepresentationSurjectivity}\left(idUnit\right)\wedge \mathrm{EffectiveDescent}\left(idUnit,idUnit\right)\wedge \mathrm{SelfDescriptionClosure}\left(Unit\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.unit_degenerate_audit (✓ std3). ∎

Source. Repository-derived.

Commentary.

On Unit, identity readout and representation satisfy their map laws, identity dynamics descend, and the constant evaluator represents the unique Unit endomap. No nonemptiness premise is assumed.

References

• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.effective_descent_not_representation_surjectivity
• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.effective_descent_not_self_description_closure
• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.effective_descent_not_state_faithfulness
• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.empty_degenerate_audit
• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.representation_surjectivity_not_self_description_closure
• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.state_faithfulness_not_representation_surjectivity
• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.state_faithfulness_not_self_description_closure
• Truth anchor: D5/S3/ConceptDynamics/Representation/DiagonalEscapeNeedsTypeExtension.unit_degenerate_audit
• Dependency: D5/S3/ConceptDynamics/Dialectics/DeterministicInterfaceEquivalence