Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

MechanicalRealReadoutRegistration

Abstract

Real mechanical readouts retain their full parameter dependence in a finite observation slot.

Definition 1.1 (PrefixOutput).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.PrefixOutput

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.PrefixOutput (✓ std3).

Source. Repository-derived.

Commentary.

A readout of weights, slope, phase, and finite horizon is a real number.

Definition 1.2 (CompletionOutput).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.CompletionOutput

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.CompletionOutput (✓ std3).

Source. Repository-derived.

Commentary.

A completed real readout is paired with all its geometric finite prefixes.

Definition 1.3 (actualPrefix).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.actualPrefix

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.actualPrefix (✓ std3).

Source. Repository-derived.

Commentary.

The finite component sums weighted mechanical letters at the given slope and phase.

Definition 1.4 (actualCompletion).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.actualCompletion

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.actualCompletion (✓ std3).

Source. Repository-derived.

Commentary.

The paired components are the geometric series and its finite weighted prefix.

Definition 1.5 (localOrderClaim).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderClaim

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderClaim (✓ std3).

Source. Repository-derived.

Commentary.

Local order preservation at every phase is equivalent to decreasing weights with a nonnegative terminal weight.

Definition 1.6 (isometricClaim).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.isometricClaim

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.isometricClaim (✓ std3).

Source. Repository-derived.

Commentary.

The completed readout has uniform tails, integrability, exact finite and infinite L1 distances, and a mixed-error formula.

Definition 1.7 (uniformBoundClaim).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.uniformBoundClaim

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.uniformBoundClaim (✓ std3).

Source. Repository-derived.

Commentary.

Geometric readouts lie within one minus the ratio of the slope, with phase-sensitive one-sided bounds.

Definition 1.8 (regularityClaim).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.regularityClaim

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.regularityClaim (✓ std3).

Source. Repository-derived.

Commentary.

Integer hits classify fixed-phase continuity and give a quantitative lower jump at each hit.

Definition 1.9 (localOrderArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderArena (✓ std3).

Source. Repository-derived.

Commentary.

One CUT slot retains the entire weighted-prefix function for the order law.

Definition 1.10 (isometricArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.isometricArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.isometricArena (✓ std3).

Source. Repository-derived.

Commentary.

One CUT slot retains both real functions needed for the L1 completion law.

Definition 1.11 (uniformBoundArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.uniformBoundArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.uniformBoundArena (✓ std3).

Source. Repository-derived.

Commentary.

The same paired observation supports the uniform slope bound.

Definition 1.12 (regularityArena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.regularityArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.regularityArena (✓ std3).

Source. Repository-derived.

Commentary.

The completed-value component supports the continuity and jump law.

Definition 1.13 (localOrderRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderRealization (✓ std3).

Source. Repository-derived.

Commentary.

The slot is filled with actual finite mechanical-letter sums.

Definition 1.14 (completionRealization).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.completionRealization

Formalization. D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.completionRealization (✓ std3).

Source. Repository-derived.

Commentary.

The slot is filled with the actual geometric readout and its finite prefixes.

References

  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.CompletionOutput
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.PrefixOutput
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.actualCompletion
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.actualPrefix
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.completionRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.isometricArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.isometricClaim
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderClaim
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.localOrderRealization
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.regularityArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.regularityClaim
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.uniformBoundArena
  • Truth anchor: D5/S3/ConceptDynamics/InformationEscape/MechanicalRealReadoutRegistration.uniformBoundClaim
  • Dependency: D5/S1/Words/Mechanical/MechanicalReadoutRegularity
  • Dependency: D5/S1/Words/Mechanical/MechanicalReadoutUniformLimit
  • Dependency: D5/S3/ConceptDynamics/InformationEscape/MechanicalDyadicRegistration
  • Dependency: D5/S3/ConceptDynamics/InformationEscape/MechanicalReadoutSources