Multiscale Fingerprint Append

Abstract

A finite damping-defect history is stable under scale append, while an unequal new defect separates extended fingerprints.

Definition 1.1 (Finite damping-defect history).

$$\forall Zero\in \mathrm{Type}\left(\right),n\in \mathrm{Nat}\left(\right),realPart\in \mathrm{Function}\left(Zero,\mathrm{Real}\left(\right)\right),scale\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),\mathrm{Real}\left(\right)\right),k\in \mathrm{Fin}\left(n\right),\mathrm{Fintype}\left(Zero\right)\Rightarrow \mathrm{multiscaleDampingFingerprint}\left(realPart,scale\right)\left(k\right)=\mathrm{criticalDampingDefect}\left(realPart,scale\left(k\right)\right)$$

Formalization. D5/S3/Zeros/Symmetry/MultiscaleFingerprintAppend.multiscaleDampingFingerprint (✓ std3).

Source. Repository-derived.

Commentary.

Each coordinate applies the frozen critical damping defect to the same finite carrier at one prescribed scale.

Theorem 1.2 (Appending one scale preserves and separates).

$$\forall Zero\in \mathrm{Type}\left(\right),ZeroPrime\in \mathrm{Type}\left(\right),n\in \mathrm{Nat}\left(\right),realPart\in \mathrm{Function}\left(Zero,\mathrm{Real}\left(\right)\right),realPartPrime\in \mathrm{Function}\left(ZeroPrime,\mathrm{Real}\left(\right)\right),scale\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),\mathrm{Real}\left(\right)\right),tauNew\in \mathrm{Real}\left(\right),\left(\mathrm{Fintype}\left(Zero\right)\wedge \mathrm{Fintype}\left(ZeroPrime\right)\right)\Rightarrow \left(\left(\forall k\in \mathrm{Fin}\left(n\right),\mathrm{multiscaleDampingFingerprint}\left(realPart,\mathrm{snoc}\left(scale,tauNew\right)\right)\left(\mathrm{castSucc}\left(k\right)\right)=\mathrm{multiscaleDampingFingerprint}\left(realPart,scale\right)\left(k\right)\right)\wedge \left(\mathrm{criticalDampingDefect}\left(realPart,tauNew\right)\ne \mathrm{criticalDampingDefect}\left(realPartPrime,tauNew\right)\Rightarrow \mathrm{multiscaleDampingFingerprint}\left(realPart,\mathrm{snoc}\left(scale,tauNew\right)\right)\ne \mathrm{multiscaleDampingFingerprint}\left(realPartPrime,\mathrm{snoc}\left(scale,tauNew\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/Symmetry/MultiscaleFingerprintAppend.multiscale_fingerprint_append (✓ std3). ∎

Source. Repository-derived.

Commentary.

The snoc-castSucc law identifies every old coordinate with its extended counterpart. Equality of extended functions would also identify the last coordinates, contradicting unequal defects at the appended scale.

Theorem 1.3 (The preregistered collision separates at scale two).

$$\mathrm{let}b:=\mathrm{arcosh}\left(\frac{\cosh \left(1\right)+1}{2}\right)\mathrm{let}X:=\mathrm{Vector}\left(\frac{3}{2},-\frac{1}{2}\right)\mathrm{let}Y:=\mathrm{Vector}\left(\frac{1}{2}+b,\frac{1}{2}+b,\frac{1}{2}-b,\frac{1}{2}-b\right)\mathrm{criticalDampingDefect}\left(X,1\right)=\mathrm{criticalDampingDefect}\left(Y,1\right)\wedge \left(\mathrm{criticalDampingDefect}\left(X,1\right)=2\cdot \left(\cosh \left(1\right)-1\right)\wedge \left(\mathrm{criticalDampingDefect}\left(Y,1\right)=2\cdot \left(\cosh \left(1\right)-1\right)\wedge \left(\mathrm{criticalDampingDefect}\left(X,2\right)-\mathrm{criticalDampingDefect}\left(Y,2\right)=2\cdot (\cosh \left(1\right)-1{)}^2\wedge \left(0<2\cdot (\cosh \left(1\right)-1{)}^2\wedge \mathrm{criticalDampingDefect}\left(X,2\right)\ne \mathrm{criticalDampingDefect}\left(Y,2\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/Symmetry/MultiscaleFingerprintAppend.two_scale_collision_separation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two-point centered offsets plus and minus one collide at scale one with the four-point offsets plus and minus b. The double-angle identity makes their scale-two difference the displayed strictly positive square.

References

• Truth anchor: D5/S3/Zeros/Symmetry/MultiscaleFingerprintAppend.multiscaleDampingFingerprint
• Truth anchor: D5/S3/Zeros/Symmetry/MultiscaleFingerprintAppend.multiscale_fingerprint_append
• Truth anchor: D5/S3/Zeros/Symmetry/MultiscaleFingerprintAppend.two_scale_collision_separation
• Dependency: D5/S3/Zeros/Symmetry/CriticalDampingFlatness