Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

MapInjectiveRegistrationTemplates

Abstract

Exact injectivity registration programs over finite object states.

Definition 1.1 (mapInjectiveSignature).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveSignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveSignature (✓ std3).

Source. Repository-derived.

Commentary.

One typed CUT slot retains the complete map as its readout.

Definition 1.2 (mapInjectiveRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveRealization (✓ std3).

Source. Repository-derived.

Commentary.

The supplied map remains unchanged; its values are not replaced by truth labels.

Definition 1.3 (mapInjectiveArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveArena (✓ std3).

Source. Repository-derived.

Commentary.

The law is injectivity of the readout on the supplied finite arena, with no arbitrary law parameter.

Theorem 1.4 (mapInjectiveLegacy).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveLegacy

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveLegacy (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete Function.Injective statement is definitionally the generated law.

Theorem 1.5 (mapInjective_sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjective_sensitivity

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjective_sensitivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

An injective readout and two distinct states witness sensitivity of the only CUT slot: replacing the map by a constant falsifies the law.

References

  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjectiveSignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MapInjectiveRegistrationTemplates.mapInjective_sensitivity
  • Dependency: D5/S0/History/HistoryCarrier
  • Dependency: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates
  • Dependency: D5/S3/ConceptDynamics/RegistrationWitnesses