Five Mode Predictive Law Geometry Core

Abstract

Finite-horizon mixture geometry and exact startup cutoffs of the actual five-mode source.

The literal five-state source has visible symbols Fin 4, with B as code 2. Admissibility is p>0, q>0, r>0 and p+q+r<1. Write a=1-p-q, b=1-r and c=1-p-q-r. Pure and empty laws are the actual future and initial word laws of FiniteStartFiveModeSource. LawProfile contains every finite horizon. ProbabilityProfile requires nonnegative weights of total mass one; CoherentProfile also requires consistency under deleting the final read.

Finite total variation is half the sum of absolute mass differences; profileDistance is its supremum over finite horizons. mixtureLaw x combines pure laws 2 and 4 with weights x and 1-x. Finite TV holds for real signed coordinates; probability and supremum statements restrict coordinates to [0,1].

For unequal a and b, theta=min(a,b)/max(a,b), minority theta k=theta^k/(1+theta^k), and orientedMixture z puts weight z on the minority branch. The acquired startup word is B^(k+1). cutoff t e is the natural ceiling of log((1-e)/e)/abs(log t), and N2=cutoff theta (2 epsilon). The first accepted index uses a non-strict inequality, including exact ties.

Theorem 1.1 (Literal all-B holding masses).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\forall H:\mathbb{N},(\mathrm{word}\left(\mathrm{pureLaw}\left(p,q,r,2\right),H,\mathrm{constant}\left(B\right)\right)=(a\left(p,q\right){)}^H\wedge \mathrm{word}\left(\mathrm{pureLaw}\left(p,q,r,4\right),H,\mathrm{constant}\left(B\right)\right)=(b\left(r\right){)}^H)))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.branch_all_B (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both masses are powers at every finite horizon, including H=0.

Theorem 1.2 (Exact common branch support).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (\forall H:\mathbb{N},(\forall w:\mathrm{Fin}\left(H\right)\to Visible,((0<\mathrm{word}\left(\mathrm{pureLaw}\left(p,q,r,2\right),H,w\right)\wedge 0<\mathrm{word}\left(\mathrm{pureLaw}\left(p,q,r,4\right),H,w\right))⟺w=\mathrm{constant}\left(B\right))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.branch_word_overlap (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first exit categories are disjoint, so the common positive support is exactly the all-B word.

Theorem 1.3 (Finite branch total variation).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (\forall H:\mathbb{N},\mathrm{TV}\left(\mathrm{at}\left(\mathrm{pureLaw}\left(p,q,r,2\right),H\right),\mathrm{at}\left(\mathrm{pureLaw}\left(p,q,r,4\right),H\right)\right)=(1-(\min \left(a\left(p,q\right),b\left(r\right)\right){)}^H))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.branch_finite_tv (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite value is 1-min(a,b)^H. Its horizon dependence is retained.

Theorem 1.4 (Finite mixture total variation).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (\forall x:\mathbb{R},(\forall z:\mathbb{R},(\forall H:\mathbb{N},\mathrm{TV}\left(\mathrm{at}\left(\mathrm{mixtureLaw}\left(p,q,r,x\right),H\right),\mathrm{at}\left(\mathrm{mixtureLaw}\left(p,q,r,z\right),H\right)\right)=(\mathrm{abs}\left((x-z)\right)\ast (1-(\min \left(a\left(p,q\right),b\left(r\right)\right){)}^H)))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.mixture_finite_tv (✓ std3). ∎

Source. Repository-derived.

Commentary.

Homogeneity of the signed difference combines with the actual branch overlap.

Theorem 1.5 (The all-horizon mixture metric).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (\forall x:\mathbb{R},(\forall z:\mathbb{R},((x\in \mathrm{Icc}\left(0,1\right)\wedge z\in \mathrm{Icc}\left(0,1\right))\Rightarrow \mathrm{profileDistance}\left(\mathrm{mixtureLaw}\left(p,q,r,x\right),\mathrm{mixtureLaw}\left(p,q,r,z\right)\right)=\mathrm{abs}\left((x-z)\right))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.mixture_profile_distance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite holding powers tend to zero, so the supremum equals the coordinate distance.

Theorem 1.6 (Positive uniform separation constant).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow 0<\mathrm{kappa}\left(p,q,r\right)))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.kappa_positive (✓ std3). ∎

Source. Repository-derived.

Commentary.

kappa is min(c,p,q,a,cs/(s+r),ap/s,a*q/s,1/25), with every term strictly positive.

Theorem 1.7 (Singleton versus any mixture).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (\forall x:\mathbb{R},(x\in \mathrm{Icc}\left(0,1\right)\Rightarrow (\forall j:State,((j=0\vee (j=1\vee j=3))\Rightarrow \mathrm{kappa}\left(p,q,r\right)\le \mathrm{profileDistance}\left(\mathrm{pureLaw}\left(p,q,r,j\right),\mathrm{mixtureLaw}\left(p,q,r,x\right)\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.singleton_mixture_separation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The coordinate and finite-event estimates apply without generic-parameter exclusions.

Theorem 1.8 (Empty versus any mixture).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (\forall x:\mathbb{R},(x\in \mathrm{Icc}\left(0,1\right)\Rightarrow \frac{1}{25}\le \mathrm{profileDistance}\left(\mathrm{emptyLaw}\left(p,q,r\right),\mathrm{mixtureLaw}\left(p,q,r,x\right)\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.empty_mixture_separation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two one-step event gaps give the universal lower bound one twenty-fifth.

Theorem 1.9 (Strict geometric monotonicity).

$$(\forall t:\mathbb{R},((0<t\wedge t<1)\Rightarrow \mathrm{StrictAnti}\left(\mathrm{minority}\left(t\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.minority_strictAnti (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite startup minority coordinate decreases at every step when 0<t<1.

Theorem 1.10 (Geometric decay).

$$(\forall t:\mathbb{R},((0<t\wedge t<1)\Rightarrow \mathrm{Tendsto}\left(\mathrm{minority}\left(t\right),atTop,\mathrm{nhds}\left(0\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.minority_tendsto_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The limit concerns finite startup coordinates, not an observed infinite history.

Theorem 1.11 (Exact first non-strict cutoff and ties).

$$(\forall t:\mathbb{R},(\forall e:\mathbb{R},(((0<t\wedge t<1)\wedge (0<e\wedge e<\frac{1}{2}))\Rightarrow (0<\mathrm{cutoff}\left(t,e\right)\wedge (\mathrm{minority}\left(t,\mathrm{cutoff}\left(t,e\right)\right)\le e\wedge ((\forall i:\mathbb{N},(i<\mathrm{cutoff}\left(t,e\right)\Rightarrow e<\mathrm{minority}\left(t,i\right)))\wedge ((\forall k:\mathbb{N},(\mathrm{minority}\left(t,k\right)\le e⟺\mathrm{cutoff}\left(t,e\right)\le k))\wedge (\mathrm{minority}\left(t,\mathrm{cutoff}\left(t,e\right)\right)=e⟺\frac{\log \left(\frac{(1-e)}{e}\right)}{\mathrm{abs}\left(\log \left(t\right)\right)}=\mathrm{castReal}\left(\mathrm{cutoff}\left(t,e\right)\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.cutoff_first_nonstrict (✓ std3). ∎

Source. Repository-derived.

Commentary.

The literal natural ceiling is positive, accepts equality at the threshold, and excludes all earlier indices.

Theorem 1.12 (The actual acquired startup law).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (a\left(p,q\right)\ne b\left(r\right)\Rightarrow (\forall k:\mathbb{N},(\forall H:\mathbb{N},(\forall w:\mathrm{Fin}\left(H\right)\to Visible,\mathrm{word}\left(\mathrm{actualFutureWordWeight}\left(p,q,r,\mathrm{replicate}\left((k+1),B\right)\right),H,w\right)=\mathrm{word}\left(\mathrm{orientedMixture}\left(p,q,r,\mathrm{minority}\left(\mathrm{theta}\left(p,q,r\right),k\right)\right),H,w\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.actual_oriented_startup (✓ std3). ∎

Source. Repository-derived.

Commentary.

The acquired all-B posterior from the literal source gives G_delta at every future word.

Theorem 1.13 (The source-specific minority cutoff).

$$(\forall p:\mathbb{R},(\forall q:\mathbb{R},(\forall r:\mathbb{R},(\mathrm{admissible}\left(p,q,r\right)\Rightarrow (a\left(p,q\right)\ne b\left(r\right)\Rightarrow (\forall epsilon:\mathbb{R},((0<(2\ast epsilon)\wedge (2\ast epsilon)<\mathrm{kappa}\left(p,q,r\right))\Rightarrow (0<N2\left(p,q,r,epsilon\right)\wedge (\mathrm{minority}\left(\mathrm{theta}\left(p,q,r\right),N2\left(p,q,r,epsilon\right)\right)\le (2\ast epsilon)\wedge ((\forall i:\mathbb{N},(i<N2\left(p,q,r,epsilon\right)\Rightarrow (2\ast epsilon)<\mathrm{minority}\left(\mathrm{theta}\left(p,q,r\right),i\right)))\wedge ((\forall k:\mathbb{N},(\mathrm{minority}\left(\mathrm{theta}\left(p,q,r\right),k\right)\le (2\ast epsilon)⟺N2\left(p,q,r,epsilon\right)\le k))\wedge (\mathrm{minority}\left(\mathrm{theta}\left(p,q,r\right),N2\left(p,q,r,epsilon\right)\right)=(2\ast epsilon)⟺\frac{\log \left(\frac{(1-(2\ast epsilon))}{(2\ast epsilon)}\right)}{\mathrm{abs}\left(\log \left(\mathrm{theta}\left(p,q,r\right)\right)\right)}=\mathrm{castReal}\left(N2\left(p,q,r,epsilon\right)\right)))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.actual_startup_cutoff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both unequal orientations have the same exact minority threshold index N2.

References

• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.actual_oriented_startup
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.actual_startup_cutoff
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.branch_all_B
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.branch_finite_tv
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.branch_word_overlap
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.cutoff_first_nonstrict
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.empty_mixture_separation
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.kappa_positive
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.minority_strictAnti
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.minority_tendsto_zero
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.mixture_finite_tv
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.mixture_profile_distance
• Truth anchor: D5/S3/ObserverMemory/Prediction/FiveModePredictiveLawGeometry/Core.singleton_mixture_separation
• Dependency: D5/S3/ObserverMemory/Prediction/FiniteStartFiveModeSource
• Dependency: D5/S3/TotalVariation/Metric