Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Loss is the decrease of the surviving mode weight

Abstract

Native mode balance and complete arbitrary-reference operational outputs.

Theorem 1.1 (Every original control and every subinterval).

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalReferenceRepeatedMass.native_mode_balance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix c<1/2, 0<a<c and an original height k on [0,T] with constant phase zero. For each original mode i, let p_i(k) be its positive double-wall probability, S(t)=exp(-integral_0^t hazard(c,k)) its native survival, and f_i(t) the squared literal jump amplitude. For every 0<=s<=t<=T, f_i is integrable on (s,t] and its integral equals [S(s)p_i(k(s))-S(t)p_i(k(t))]/p_i(a). No initial-height equality is needed for this general balance law.

The original regularity alternatives imply absolute continuity of k. OriginalRepeatedMarkedLaw.native_bounds gives 0<k(t)<c on [0,T]; the unordered interval used by almost-everywhere differentiation equals [0,T] because the original control includes T>=0. FiniteRectangleTransport.probability_derivative, at base (c,c,1-2c) and velocity k prime(t), gives p_i prime(t)=direction_i k prime(t), with direction=(1,-1,0,-1,1). The integrable native hazard has an absolutely continuous primitive. Exponentiation preserves absolute continuity on its compact range, and multiplication by each affine probability coordinate preserves it. Almost everywhere, logarithmic differentiation gives g_i=hazard-p_i’/p_i. The explicit five coordinates show g_i>=0. Consequently the literal squared square-root amplitude is g_i S p_i/p_i(a), which is minus the derivative of S p_i divided by p_i(a). The fundamental theorem for absolutely continuous functions gives the balance identity. Exceptional derivative values at corners have zero Lebesgue mass.

Theorem 1.2 (The same arbitrary joint input across prefix and suffix).

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalReferenceRepeatedMass.repeated_reference_completeness (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let B be any band 0<a<b<c<1/2, n>=1 and e either literal early or late history k. Put q=(a/b)(c-b)/(c-a). H is any complete complex Hilbert space, including nonseparable spaces. rho is any positive trace-class operator on Blocks(Fin5,H), with no normalization, finite-rank, separability or product-state assumption. A_i is the positive trace-class compression of that same rho to reference block i. The actual reference-output density is F_i(t)=f_i(t) A_i, as identified with tensor-amplified Kraus conjugation by OriginalReferenceOutputMeasure.repeated_failure_event.

For every mode i and every 1<t<=2, F_i(t)=q^n F_i^suffix(t-1), where the suffix uses the same rho and the original earlySuffix or lateSuffix control. This is exact prefix scaling of each reference operator, using the already established chronological Kraus action. The coefficient integrals on (0,1], (1,2] and (0,2] are respectively 1-q^n, q^n(1-q) and 1-q^(n+1). In particular the suffix Bochner integral is q^n(1-q) A_i. The endpoint heights and native survival values are supplied by OriginalRepeatedPrefix; they are applied to the general mode balance identity.

Summing the norms of the five suffix event outputs gives q^n(1-q) norm(rho). Summing the norms of the five full failure event outputs and adding norm(q^(n+1) rho) gives norm(rho). Positivity turns each scalar multiple into its nonnegative coefficient times norm(A_i), and the same-input block trace partition gives sum_i norm(A_i)=norm(rho). Thus all modes and their unchanged reference correlations contribute to exact mass completeness. The terminal scalar is identified with the genuine tensor Kraus conjugation by repeated_live_operational. The six-coordinate extension and the supremum are supplied by repeated_stopped_operational and repeated_operational_supremum.

These identities retain their unnormalized form; normalized live inputs have norm(rho)=1. The operational companion statements below consume this balance and the corresponding reference-distance theorem.

Theorem 1.3 (Common prefix cancellation and disjoint suffix windows).

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalReferenceRepeatedMass.repeated_reference_distance (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every band B, n>=1, arbitrary complete complex Hilbert reference H and positive joint trace-class rho, every mode’s prefix Bochner outputs agree on (0,1] intersect every Borel event E. Moreover sum_i integral_(0,2] norm(F_i^early(t)-F_i^late(t)) equals 2 q^n(1-q) norm(rho). Both densities use the same rho, including all entanglement with its unchanged reference.

Before time one, the literal heights, native survival and jump rates coincide almost everywhere. The seam has zero Lebesgue mass, giving equality on every restricted event. The late suffix is constant before its excursion and the early suffix is constant after its excursion. Local constancy makes both the height derivative and logarithmic probability derivative vanish, so the actual jump coefficient vanishes on the corresponding waiting window. Exact prefix scaling carries these zero densities to the original clock. Except at the middle seam, one of the two suffix densities is zero. Thus the norm of their difference equals the sum of their norms, without comparing independent inputs or replacing joint operators by marginal probabilities.

Split the full interval into prefix and suffix. The prefix difference integrates to zero, and the suffix norm integral is the sum of the two positive suffix masses. The preceding completeness theorem supplies each mass q^n(1-q) norm(rho). The complete operational companion statements below retain the fixed absorbing successor isometrically, identify the common successful Kraus action, extend to initially stopped six-coordinate states and take the genuine all-input supremum.

Theorem 1.4 (Complete five-mode classical-quantum output).

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalReferenceRepeatedMass.repeated_live_operational (✓ std3). ∎

Source. Repository-derived.

Commentary.

H is any complete complex Hilbert space in any universe, including nonseparable spaces, and rho is any positive trace-class joint input on Blocks(Fin5,H). No normalization, finite rank or product-state assumption is imposed. referenceSuccess is the diagonal original successfulKraus amplified by the unchanged identity reference. The theorem proves both the literal matrix action on the scalar system and its intertwining with TensorProduct.map under the onto Hilbert isometry tensorCoordinates, on every joint tensor vector. successOutput is its actual Kraus conjugation of the same rho. liveFailure embeds the reference compression in the fixed absorbing coordinate f=5, with the squared literal jump amplitude, and is proved equal to absorbingJump rho absorbingJump-adjoint at every time and mode.

At the terminal time two, both actual successful operators equal sqrt(q^(n+1)) times the identity. Hence their successful outputs agree for the same arbitrary rho. liveDistance is exactly the IS.7 half-sum: the trace norm of the successful-output difference plus the sum over all five modes of the Lebesgue integral on (0,2] of the trace norm of the full absorbing-output-density difference. The fixed f embedding preserves the norm of each signed scalar multiple of its positive reference block. Applying repeated_reference_distance therefore gives liveDistance=q^n(1-q) norm(rho). Neither the mode/time record nor any reference correlation is discarded.

Theorem 1.5 (The original six-dimensional absorbing extension).

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalReferenceRepeatedMass.repeated_stopped_operational (✓ std3). ∎

Source. Repository-derived.

Commentary.

The input is an arbitrary positive trace-class rho on Blocks(Fin6,H), with any complete complex Hilbert reference H. stoppedSuccess is exactly K direct-sum the stopped identity: its first five coordinates use the original diagonal K, and coordinate five is unchanged. The theorem gives its tensor intertwining and explicit coordinate action. stoppedJump is the rank-one literal jump extended by zero on stopped input. Its tensor intertwining is proved on every joint tensor vector; every jump annihilates insertion into f. stoppedFailure is proved equal to that actual tensor-amplified Kraus conjugation of rho, at every time and original mode. For either repeated history, these full output densities are Bochner integrable on (0,2] intersect every Borel event E.

The successful six-coordinate outputs are identical for the same original rho. In particular, arbitrary initial live-stopped coherences are retained in A rho A-adjoint, and cancel only because the two terminal A operators are equal. liveWeight is the sum of the norms of the five positive diagonal reference compressions. Positivity identifies these with their real traces, and the existing finite-block trace partition proves liveWeight plus the stopped block trace equals norm(rho). To reuse the five-mode distance result, diagonalLive embeds these same five blocks into a positive five-mode auxiliary operator. Its compression in mode i is exactly the original six-coordinate compression in i.castSucc, and its norm is liveWeight. Only the failure calculation uses this auxiliary operator; the successful output continues to act on the original rho. Thus stoppedDistance=q^n(1-q) liveWeight. For every normalized six-coordinate input, liveWeight is at most one, so stoppedDistance is at most q^n(1-q).

Theorem 1.6 (All references, attainment and the original marked law).

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalReferenceRepeatedMass.repeated_operational_supremum (✓ std3). ∎

Source. Repository-derived.

Commentary.

JointState(m) packages a reference H in an arbitrary fixed universe, its complete complex Hilbert instances, and a positive joint trace-class input of norm one on Blocks(Fin m,H). operationalDistance is the real supremum of the actual stoppedDistance values of all JointState(6) inputs in that universe. Its definition contains no proposed scalar. The previous theorem bounds every such input, including infinite-dimensional and nonseparable references. A one-dimensional lifted reference and an input supported in live coordinate zero provide a positive normalized fully live witness, with liveWeight one and distance q^n(1-q). The identity on this one-dimensional reference has trace and trace norm one by the existing finite-multiplicity trace theorem. Thus the independently defined supremum equals q^n(1-q) in every universe. The theorem also gives this value for every normalized five-live-mode input, and links the supremum to OriginalRepeatedMarkedLaw.native_marked_tv for every common unknown beta, integer parity m and initial phase vector theta.

The inverse application uses that exact operational/marked equality at every n in OriginalRepeatedMarkedLaw.marked_inverse_nonuniformity. The actual height gap remains b-a while q^n(1-q) tends to zero, defeating every modulus tending to zero at the origin on the fixed-duration, common-band class. OriginalRepeatedResources supplies the same literal controls with their finite-piecewise-C1 regularity and exact aggregate resources: duration two, height variation and arc length 2(n+1)(b-a), zero phase variation, squared-speed integral (4n^2+8)(b-a)^2, height essential speed max(2n,4)(b-a), and zero phase speed. These values agree within each compared pair and grow with n. The obstruction applies to the class without a common speed or height-variation cap. No law acquisition, waveform sensor, reset, unexecuted-tail read or additional programme register is supplied.

References