Signed defect, harmonic limit and sixth-power gain

Abstract

Superharmonic completion on the acquired chain

F is an arbitrary original boxed CommonFlow. The acquired return chain is C=BA with its original stationary unweighted p marginal, and L has the original (1-u)*v weights. T is normalizedAction, with endpointRate=6/25. The ENNReal threeStepAverage is (g+Tg+T squared g)/3; h is its real value, excess=g.toReal-9/25, and delta=h-(Th).toReal uses signed real subtraction. AE(mu,Q,P) means P holds for mu-almost every Q. qIterateAt(F,Q) denotes the sequence n mapped to qIterate(F,n,Q). CRow and LRow denote the actual acquired rows.

Theorem 1.1 (h finite).

$$\forall F:CommonFlow,\forall Q:PDescriptor,\mathrm{threeStepAverage}\left(F,Q\right)\ne top$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.h_finite (✓ std3). ∎

Source. Repository-derived.

Commentary.

All original normalized g iterates are finite, using L <= C and finite endpointRate inverse. Their finite three-step sum is finite. This bound is consumed by Holder, real conversion and stationary cancellation.

Theorem 1.2 (h global bound).

$$\forall F:CommonFlow,\forall Q:PDescriptor,\mathrm{threeStepAverage}\left(F,Q\right)\le 10$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.h_global_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The global g bound one and normalized iterate bounds (25/6) to the powers one and two bound the finite three-step average by ten. This global bound is consumed by row integrability and stationary localization.

Theorem 1.3 (sixth le h).

$$\forall F:CommonFlow,\forall Q:PDescriptor,\mathrm{sixthFunctional}\left(F,Q\right)\le \mathrm{threeStepAverage}\left(F,Q\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.sixth_le_h (✓ std3). ∎

Source. Repository-derived.

Commentary.

q is bounded above by the first term of its infimum, namely threeStepAverage. If h is zero, q is zero. Otherwise cancellation gives q to the sixth power divided by h to the fifth power <= h. This bound supplies finite sixth-functional integrals.

Theorem 1.4 (sixth measurable).

$$\forall F:CommonFlow,\mathrm{Measurable}\left(\mathrm{sixthFunctional}\left(F\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.sixth_measurable (✓ std3). ∎

Source. Repository-derived.

Commentary.

Countable-infimum measurability and measurable finite powers and division give measurability of the actual sixth functional. This is consumed by Holder and the stationary integral identity.

Theorem 1.5 (common flow signed h).

$$\forall F:CommonFlow,(\mathrm{Measurable}\left(\mathrm{descriptorTVBorel}\left(p\right),BorelR,h\left(F\right)\right)\wedge \mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,(\frac{3}{25}\le h\left(F,Q\right)\wedge h\left(F,Q\right)\le \frac{1}{2}\wedge 0\le \mathrm{excess}\left(Q\right)\wedge \mathrm{delta}\left(F,Q\right)=\frac{(\mathrm{toReal}\left(g\left(Q\right)\right)-\mathrm{toReal}\left(\mathrm{normalizedIterate}\left(F,g,3,Q\right)\right))}{3}\wedge \frac{\mathrm{excess}\left(Q\right)}{3}\le \mathrm{delta}\left(F,Q\right)\wedge \mathrm{normalizedAction}\left(F,\mathrm{threeStepAverage}\left(F\right),Q\right)\le \mathrm{threeStepAverage}\left(F,Q\right))\right))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_signed_h (✓ std3). ∎

Source. Repository-derived.

Commentary.

h is measurable for the actual TV-Borel sigma algebra on the exact p descriptor. The original three-step upper endpoint box supplies the signed defect. Finite row domination makes every normalized g iterate finite, so conversion to real values preserves the signed identity. The bound h <= 1/2 follows from g <= 4/9 and T <= (10/9) C for the first two iterates. A global bound ten ensures finite row integrals.

Theorem 1.6 (common flow q limit).

$$\forall F:CommonFlow,(\mathrm{Measurable}\left(q\left(F\right)\right)\wedge \mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,(\mathrm{Antitone}\left(\mathrm{qIterateAt}\left(F,Q\right)\right)\wedge \mathrm{Tendsto}\left(\mathrm{qIterateAt}\left(F,Q\right),atTop,\mathrm{Nhds}\left(q\left(F,Q\right)\right)\right)\wedge q\left(F,Q\right)\le \mathrm{threeStepAverage}\left(F,Q\right)\wedge \mathrm{normalizedAction}\left(F,q\left(F\right),Q\right)=q\left(F,Q\right))\right))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_q_limit (✓ std3). ∎

Source. Repository-derived.

Commentary.

qIterate(F,n) is T to the power n applied to the same threeStepAverage, and q is its infimum over all natural n. The initial decrease follows from the signed defect. Stationarity of C transports subsequent conull inequalities to acquired rows, and L <= C transfers them to weighted rows. Decreasing monotone convergence applies because the first row integral is finite. Dropping the first term leaves the infimum unchanged.

Theorem 1.7 (common flow sixth power gain).

$$\forall F:CommonFlow,\mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,\mathrm{sixthFunctional}\left(F,Q\right)\cdot \mathrm{ofReal}\left((1+\frac{10\cdot \mathrm{excess}\left(Q\right)}{3})\right)\le \mathrm{normalizedAction}\left(F,\mathrm{sixthFunctional}\left(F\right),Q\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_sixth_power_gain (✓ std3). ∎

Source. Repository-derived.

Commentary.

sixthFunctional is q to the sixth power divided by threeStepAverage to the fifth power, on the same actual flow. Weighted Holder with exponents 1/6 and 5/6, followed by Tq=q, gives q to the sixth power <= TF times (Th) to the fifth power. The signed defect and h <= 1/2 yield the displayed multiplicative gain. Positive h and finite row bounds justify division and conversion to reals.

Theorem 1.8 (common flow unweighted gain).

$$\forall F:CommonFlow,\mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,(\mathrm{smul}\left(\mathrm{inv}\left(endpointRate\right),\mathrm{LRow}\left(F,Q\right)\right)\le \mathrm{smul}\left(\mathrm{ofReal}\left((1+\frac{25\cdot \mathrm{excess}\left(Q\right)}{9})\right),\mathrm{CRow}\left(F,Q\right)\right)\wedge (\mathrm{sixthFunctional}\left(F,Q\right)+\frac{9}{20}\cdot \mathrm{ofReal}\left(\mathrm{excess}\left(Q\right)\right)\cdot \mathrm{sixthFunctional}\left(F,Q\right))\le \mathrm{lintegral}\left(\mathrm{CRow}\left(F,Q\right),R,\mathrm{sixthFunctional}\left(F,R\right)\right))\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_unweighted_gain (✓ std3). ∎

Source. Repository-derived.

Commentary.

The full B completion equation gives g >= (1-u)(3/5), while v <= 2/5 bounds the actual weighted row. Thus T <= (1+25excess/9) C on the original marginal. Together with the sixth-power gain and 0 <= excess <= 19/225, this gives CF >= F+(9/20)excessF. The two inequalities use the same acquired B and A, and the margin remains unweighted.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_q_limit
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_signed_h
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_sixth_power_gain
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.common_flow_unweighted_gain
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.h_finite
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.h_global_bound
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.sixth_le_h
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelSuperharmonic.sixth_measurable
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelTVTopology