Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Registration Template and Helpers

Abstract

Typed constructors generate primitive inventories and laws over explicit canonical arenas.

The separation family serves two gold registrations. Bijection, admitted surjection, anchored separation, context selection, exact design, completion exchange, scope tables, and two-step binary protocols each serve one gold registration and are helpers under the reuse criterion.

Definition 1.1 (Single CUT realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.cutRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.cutRealization (✓ std3).

Source. Repository-derived.

Commentary.

One typed function supplies the single CUT readout, with no point anchors.

Definition 1.2 (Bijection helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.bijectiveArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.bijectiveArena (✓ std3).

Source. Repository-derived.

Commentary.

The generated law requires bijectivity of the realization’s readout.

Definition 1.3 (Separation realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.separationRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.separationRealization (✓ std3).

Source. Repository-derived.

Commentary.

Two typed functions supply coarse and fine CUT readouts.

Definition 1.4 (Separation template).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.separationArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.separationArena (✓ std3).

Source. Repository-derived.

Commentary.

The generated law requires two states with equal coarse readouts and different fine readouts.

Definition 1.5 (Admitted-surjection realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.admittedSurjectionRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.admittedSurjectionRealization (✓ std3).

Source. Repository-derived.

Commentary.

A function supplies a CUT readout and a decidable predicate supplies a Boolean ADMIT readout.

Definition 1.6 (Admitted-surjection helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.admittedSurjectionArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.admittedSurjectionArena (✓ std3).

Source. Repository-derived.

Commentary.

Every output has an admitted preimage, and two admitted states have distinct outputs.

Definition 1.7 (Anchored-separation realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.anchoredSeparationRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.anchoredSeparationRealization (✓ std3).

Source. Repository-derived.

Commentary.

Two CUT readouts, two ADMIT predicates, and two point anchors supply the primitive inventory.

Definition 1.8 (Anchored-separation helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.anchoredSeparationArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.anchoredSeparationArena (✓ std3).

Source. Repository-derived.

Commentary.

The anchors satisfy their admission predicates, agree in one readout, differ in the other, and preclude a recovery map.

Definition 1.9 (Context-selection realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.contextSelectionRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.contextSelectionRealization (✓ std3).

Source. Repository-derived.

Commentary.

Two shared readouts, three Boolean parameters, two ADMIT predicates, and two anchors supply the context inventory.

Definition 1.10 (Context-selection helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.contextSelectionArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.contextSelectionArena (✓ std3).

Source. Repository-derived.

Commentary.

The law records agreement of the shared readouts, variation of all three parameters, and admission at the two anchors.

Definition 1.11 (Exact-design realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.exactDesignRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.exactDesignRealization (✓ std3).

Source. Repository-derived.

Commentary.

Two Boolean functions supply the experimental CUT readouts.

Definition 1.12 (Exact-design helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.exactDesignArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.exactDesignArena (✓ std3).

Source. Repository-derived.

Commentary.

Each readout alone is noninjective; the joint readout is injective and requires both experiments.

Definition 1.13 (Completion-exchange realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.completionExchangeRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.completionExchangeRealization (✓ std3).

Source. Repository-derived.

Commentary.

Two state transitions supply FLOW readouts and one observation supplies a CUT readout.

Definition 1.14 (Completion-exchange helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.completionExchangeArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.completionExchangeArena (✓ std3).

Source. Repository-derived.

Commentary.

The law requires noncommuting transitions and different kernels for the two completion orders, using the existing unbounded predictiveProjection.

Definition 1.15 (Scope-table realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.scopeTableRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.scopeTableRealization (✓ std3).

Source. Repository-derived.

Commentary.

Three decidable predicates supply Boolean ADMIT readouts.

Definition 1.16 (Scope-table helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.scopeTableArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.scopeTableArena (✓ std3).

Source. Repository-derived.

Commentary.

Explicit coordinate functions compare the three local marginals; no state satisfies all three admission predicates.

Definition 1.17 (Binary sensor inventory).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.binaryFamilySignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.binaryFamilySignature (✓ std3).

Source. Repository-derived.

Commentary.

An arbitrary finite sensor type indexes Boolean CUT readouts over the supplied carrier.

Definition 1.18 (Binary sensor realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.binaryFamilyRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.binaryFamilyRealization (✓ std3).

Source. Repository-derived.

Commentary.

The supplied sensor family defines the readouts, with no point anchors.

Definition 1.19 (First successful natural index).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.firstSuccess

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.firstSuccess (✓ std3).

Source. Repository-derived.

Commentary.

A natural-number predicate has its least successful index when a witness exists, and zero otherwise.

Theorem 1.20 (Witnessed minimum transport).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.firstSuccess_eq_find

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

Source. Repository-derived.

Commentary.

An existence witness identifies firstSuccess with Nat.find for the same predicate.

Definition 1.21 (Two-step binary protocol statement).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepStatement

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepStatement (✓ std3).

Source. Repository-derived.

Commentary.

The first sensor divides four named states into pairs. A history-dependent second question identifies the state; individual sensors and smaller depths fail, while adaptive and static costs are two and three.

Definition 1.22 (Two-step protocol helper).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepArena (✓ std3).

Source. Repository-derived.

Commentary.

The supplied finite arena and sensors generate the protocol law with realization-dependent adaptive and static minima.

Theorem 1.23 (Two-step registration bridge).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepLegacy

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

Source. Repository-derived.

Commentary.

Existence witnesses transport the two source Nat.find costs to the generated law using firstSuccess_eq_find.

References

  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.admittedSurjectionArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.admittedSurjectionRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.anchoredSeparationArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.anchoredSeparationRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.bijectiveArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.binaryFamilyRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.binaryFamilySignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.completionExchangeArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.completionExchangeRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.contextSelectionArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.contextSelectionRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.cutRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.exactDesignArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.exactDesignRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.firstSuccess
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.firstSuccess_eq_find
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.scopeTableArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.scopeTableRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.separationArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.separationRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates.twoStepStatement
  • Dependency: D5/S3/ConceptDynamics/Coding/AdaptiveResidueIdentification
  • Dependency: D5/S3/ConceptDynamics/Completion/CommutingCompletionExchange
  • Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
  • Dependency: D5/S3/ConceptDynamics/InformationEscape/TheoremUnit