Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

SomerUniformSubsequenceCertificateRegistration

Abstract

The complete finite counterexample is retained by six independently sensitive CUT readouts.

Definition 1.1 (certificateArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.certificateArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.certificateArena (✓ std3).

Source. Repository-derived.

Commentary.

The certificate law requires equality with the actual six-code word and every field of its CounterexampleCertificate.

Definition 1.2 (certificateRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.certificateRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.certificateRealization (✓ std3).

Source. Repository-derived.

Commentary.

Each CUT slot returns the actual certificate word’s code at that position.

Definition 1.3 (bumpCode).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.bumpCode

Formalization. D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.bumpCode (✓ std3).

Source. Repository-derived.

Commentary.

Cyclic increment modulo five supplies a different code at any chosen position.

Definition 1.4 (alteredRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.alteredRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/SomerUniformSubsequenceCertificateRegistration.alteredRealization (✓ std3).

Source. Repository-derived.

Commentary.

The selected slot uses bumpCode while the other five slots preserve the actual word, witnessing independent sensitivity.

References