IterationDepthNoGapRegistration

Abstract

A finite two-origin arena records the no-gap theorem and a falsifying shifted readout.

Definition 1.1 (depthOriginRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/IterationDepthNoGapRegistration.depthOriginRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/IterationDepthNoGapRegistration.depthOriginRealization (✓ std3).

Source. Repository-derived.

Commentary.

The identity readout preserves the published zero-based depth origin.

Definition 1.2 (depthNoGapArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/IterationDepthNoGapRegistration.depthNoGapArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/IterationDepthNoGapRegistration.depthNoGapArena (✓ std3).

Source. Repository-derived.

Commentary.

The arena law requires downward closure of the arbitrary-language iteration-depth spectrum at the read origin.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/IterationDepthNoGapRegistration.depthNoGapArena
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/IterationDepthNoGapRegistration.depthOriginRealization
• Dependency: D5/S1/Words/IterationDepthNoGap
• Dependency: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates
• Dependency: D5/S3/ConceptDynamics/RegistrationWitnesses