Discounted Prime-Time Ultrametric

Abstract

The discounted finite-family prime-time distance obeys the strong triangle law.

Definition 1.1 (Discounted prime-time distance).

$$\begin{gathered} \forall x,y\in X, \\ {d}_{J,gamma}^F(x,y)={\sup }_{i\in J,n\in \mathbb{N}}w\left(i\right)gamm{a}^n\mathrm{discreteOutputDistance}\left(q\left(i,\mathrm{iterate}\left(F,n,x\right)\right),q\left(i,\mathrm{iterate}\left(F,n,y\right)\right)\right). \end{gathered}$$

Formalization. D5/S3/Observer/PrimeTimeGeometry/DiscountedPrimeTimeUltrametric.discountedPrimeTimeDistance (✓ std3).

Source. Repository-derived.

Commentary.

For a finite observer budget J, take the real supremum over each selected index i and each nonnegative time n. The summand is the coordinate weight times gamma to the nth power times the zero-or-one discrepancy between the two readouts after n updates.

Source-boundary open: the source does not define a real supremum for the empty coordinate family J = emptyset. The Lean iSup expression has a totalized empty-budget behavior supplied by its ambient order structure; that behavior is formalization-specific, not a source convention, and remains open pending an authoritative source clause.

Theorem 1.2 (Prime-time prediction distance obeys the strong triangle inequality).

$$\begin{gathered} \forall I\in \mathrm{Type},X\in \mathrm{Type},O\in I\to \mathrm{Type},J\in \mathrm{Finset}\left(I\right),w\in I\to \mathbb{R},q\in \forall i:I,X\to O\left(i\right),F\in X\to X,gamma\in \mathbb{R},\forall i:I,0<w\left(i\right)\Rightarrow \\ gamma\in (0,1]\Rightarrow \\ \forall x,y,z\in X, \\ {d}_{J,gamma}^F(x,z)\le \max (d_{J,gamma}^F(x,y),d_{J,gamma}^F(y,z)) \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/PrimeTimeGeometry/DiscountedPrimeTimeUltrametric.discounted_prime_time_distance_strong_triangle (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source standing carrier clause requires strictly positive weight on every coordinate i in I, while gamma belongs to (0,1]. Both are clauses of the source volume, cited here so the claim can be checked against the source rather than taken on this document’s word. The opening setup of Section 32, at source line 2016, assigns a positive weight to every coordinate, and Definition 33.1 reuses that same weight family; Theorems 32.1 and 32.2 sit in between, so that setup is inherited rather than immediately adjacent. The opening clause of Section 33 sets 0 < gamma <= 1 and is the only place the upper bound appears. The preamble to Theorem 33.2 at line 2083 separately reiterates positive weights and the lower bound gamma > 0 only. The source states these in LaTeX; they are transcribed to plain text here because Scribe text runs carry no raw LaTeX delimiters, and the verbatim quotations are kept in the Lean docstring instead. They are therefore not premises introduced here; the atom for Theorem 33.1 is a slice that does not carry them. The proof only invokes that positivity on the selected finite budget J, but the public theorem preserves the source’s global premise.

The source is silent on the empty-budget supremum (J = emptyset), so that case is an open source boundary rather than an added premise or an assigned source value.

The finite budget, the bounded discount powers, and the zero-or-one coordinate discrepancy bound every supremum by the sum of the selected weights. The existing weighted joint strong triangle theorem supplies the pointwise law, and ciSup_sup_eq moves the maximum through the prime-time supremum.

References

• Truth anchor: D5/S3/Observer/PrimeTimeGeometry/DiscountedPrimeTimeUltrametric.discountedPrimeTimeDistance
• Truth anchor: D5/S3/Observer/PrimeTimeGeometry/DiscountedPrimeTimeUltrametric.discounted_prime_time_distance_strong_triangle
• Dependency: D5/S3/Observer/MetricGeometryLaws/WeightedJointUltrapseudometric