Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

PointwiseRegistrationTemplates

Abstract

Exact pointwise registration programs over finite object states.

Definition 1.1 (pointwiseEqSignature).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqSignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqSignature (✓ std3).

Source. Repository-derived.

Commentary.

Two typed CUT readouts retain the two terms of a pointwise equation.

Definition 1.2 (pointwiseEqRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqRealization (✓ std3).

Source. Repository-derived.

Commentary.

The two supplied functions remain the readouts, with no theorem-based reduction.

Definition 1.3 (pointwiseEqArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqArena (✓ std3).

Source. Repository-derived.

Commentary.

The law equates the two readouts at every state of the supplied finite arena.

Theorem 1.4 (pointwiseEqLegacy).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqLegacy

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

Source. Repository-derived.

Commentary.

The complete universally quantified equation is definitionally the generated law.

Theorem 1.5 (pointwiseEq_sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEq_sensitivity

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

Source. Repository-derived.

Commentary.

Two distinct output values and an inhabited arena witness sensitivity of each individual CUT slot.

Definition 1.6 (pointwiseNeSignature).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeSignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeSignature (✓ std3).

Source. Repository-derived.

Commentary.

Two typed CUT readouts retain the two terms of a pointwise disequality.

Definition 1.7 (pointwiseNeRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeRealization (✓ std3).

Source. Repository-derived.

Commentary.

Both supplied functions remain unchanged in the realization.

Definition 1.8 (pointwiseNeArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeArena (✓ std3).

Source. Repository-derived.

Commentary.

The law requires different readout values at every state.

Theorem 1.9 (pointwiseNeLegacy).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeLegacy

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

Source. Repository-derived.

Commentary.

The complete universally quantified disequality is definitionally the generated law.

Theorem 1.10 (pointwiseNe_sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNe_sensitivity

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

Source. Repository-derived.

Commentary.

An inhabited state and distinct output values witness both readout slots independently.

Definition 1.11 (pointwiseOrderSignature).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderSignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderSignature (✓ std3).

Source. Repository-derived.

Commentary.

Two typed CUT readouts carry values in a linear order.

Definition 1.12 (pointwiseOrderRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderRealization (✓ std3).

Source. Repository-derived.

Commentary.

The supplied left and right functions are retained verbatim.

Definition 1.13 (pointwiseOrderArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderArena (✓ std3).

Source. Repository-derived.

Commentary.

An explicit strictness selector chooses pointwise less-than or less-than-or-equal, with no arbitrary law parameter.

Theorem 1.14 (pointwiseOrderLegacy).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderLegacy

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

Source. Repository-derived.

Commentary.

The full universal comparison is definitionally the law selected by strictness.

Theorem 1.15 (pointwiseOrder_sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrder_sensitivity

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

Source. Repository-derived.

Commentary.

Strictly ordered values witness independent sensitivity of each slot for both strict and weak laws.

Definition 1.16 (homogeneousPointwiseEqSignature).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqSignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqSignature (✓ std3).

Source. Repository-derived.

Commentary.

Two Boolean-indexed CUT slots share one output type and its explicit equality dictionary; there are no anchors.

Definition 1.17 (homogeneousPointwiseEqRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqRealization (✓ std3).

Source. Repository-derived.

Commentary.

Boolean elimination selects the supplied left or right readout in the shared output type.

Definition 1.18 (homogeneousPointwiseEqArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqArena (✓ std3).

Source. Repository-derived.

Commentary.

The law equates the homogeneous readouts at every state of the supplied finite arena.

Theorem 1.19 (homogeneousPointwiseEqLegacy).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqLegacy

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

Source. Repository-derived.

Commentary.

The full pointwise equation is definitionally equivalent to the homogeneous arena law.

Theorem 1.20 (homogeneousPointwiseEq_sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEq_sensitivity

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

Source. Repository-derived.

Commentary.

Distinct output values and an inhabited state witness a law change from changing either CUT slot alone.

Definition 1.21 (homogeneousPointwiseNeSignature).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeSignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeSignature (✓ std3).

Source. Repository-derived.

Commentary.

Two Boolean-indexed CUT slots share an output type with decidable equality and no anchors.

Definition 1.22 (homogeneousPointwiseNeRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeRealization (✓ std3).

Source. Repository-derived.

Commentary.

Boolean elimination retains the two supplied homogeneous readouts for disequality.

Definition 1.23 (homogeneousPointwiseNeArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeArena (✓ std3).

Source. Repository-derived.

Commentary.

The law requires the homogeneous readouts to differ at every state.

Theorem 1.24 (homogeneousPointwiseNeLegacy).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeLegacy

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

Source. Repository-derived.

Commentary.

The full pointwise disequality is definitionally equivalent to the homogeneous arena law.

Theorem 1.25 (homogeneousPointwiseNe_sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNe_sensitivity

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

Source. Repository-derived.

Commentary.

Distinct output values make disequality true; changing either slot alone to match the other falsifies it.

Definition 1.26 (homogeneousPointwiseOrderSignature).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderSignature

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderSignature (✓ std3).

Source. Repository-derived.

Commentary.

Two Boolean-indexed CUT slots share an output type and equality dictionary; order is supplied separately by the arena law.

Definition 1.27 (homogeneousPointwiseOrderRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderRealization (✓ std3).

Source. Repository-derived.

Commentary.

Boolean elimination selects the left or right output without an order parameter in the realization.

Definition 1.28 (homogeneousPointwiseOrderArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderArena (✓ std3).

Source. Repository-derived.

Commentary.

The arena supplies the linear order and selects strict or weak pointwise comparison of the shared output type.

Theorem 1.29 (homogeneousPointwiseOrderLegacy).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderLegacy

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

Source. Repository-derived.

Commentary.

The complete universal strict or weak comparison is definitionally equivalent to the selected arena law.

Theorem 1.30 (homogeneousPointwiseOrder_sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrder_sensitivity

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

Source. Repository-derived.

Commentary.

Two strictly ordered values witness independent changes to each CUT slot for both comparison laws.

References

  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEqSignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseEq_sensitivity
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNeSignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseNe_sensitivity
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrderSignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.homogeneousPointwiseOrder_sensitivity
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEqSignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseEq_sensitivity
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNeSignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseNe_sensitivity
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderLegacy
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrderSignature
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/PointwiseRegistrationTemplates.pointwiseOrder_sensitivity
  • Dependency: D5/S3/ConceptDynamics/InformationEscape/RegistrationTemplates
  • Dependency: D5/S3/ConceptDynamics/RegistrationWitnesses