Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Visible Adaptive Physical Record Law

Abstract

Finite visible adaptive instruments have hidden-state independent physical records and sharp absolute minimax risk.

Definition 1.1 (Legal dependent instrument events).

Formalization. D5/S3/Quantum/Measurement/VisibleAdaptiveRecordLaw.ActualEventStage (✓ std3).

Source. Repository-derived.

Commentary.

A preceding history has its own outcome carrier and measurable structure. Every measurable event in the declared next-history space pulls back to a legal instrument event. The measurable preceding projection recovers the previous history on each fibre embedding. Completely positive event operations vanish on the empty event, are countably additive in their matrix coordinates, and have measurable coordinates for every fixed retained event. Neither outcome cardinality nor a StandardBorel structure is imposed.

Definition 1.2 (Finite adaptive waiting and stopping).

Formalization. D5/S3/Quantum/Measurement/VisibleAdaptiveRecordLaw.FiniteStoppedPolicy (✓ std3).

Source. Repository-derived.

Commentary.

The finite family contains exactly the history spaces from depth zero through N. Before N, the visible policy supplies a legal instrument, a measurable real waiting-time control, a measurable stop set, and a measurable cemetery continuation compatible with the preceding projection. Stopping persists where a subsequent stop set exists. The measurable returned record includes a natural-number length: an active outcome increments it and a stopped continuation preserves the entire record.

Definition 1.3 (Actual local tensor wait and instrument amplification).

Formalization. D5/S3/Quantum/Measurement/VisibleAdaptiveRecordLaw.actualFiniteStep (✓ std3).

Source. Repository-derived.

Commentary.

An active transition first conjugates the joint state by the actual matrix exponential of minus i times the controlled waiting time times H_A tensor I_B. It then applies the actual tensor amplification of the visible CP event operation with the identity map on B. The visible map is transported through the CStarMatrix linear equivalence and tensored by the matrix-map Kronecker operation. For each supplied finite Kraus representation of the visible map, this amplification agrees on every joint matrix with the sum of conjugations by its Kraus operators tensored with I_B. This identity does not restrict the measurable classical outcome carrier or require a measurable choice of Kraus operators. A stopped transition is the identity quantum action on its deterministic cemetery event, with no added wait.

Theorem 1.4 (Physical law independence and sharp randomized absolute risk).

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/VisibleAdaptiveRecordLaw.visible_adaptive_record_law_and_absolute_minimax (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a finite-dimensional visible state rho_A, a Hermitian local Hamiltonian H_A, a hidden dimension e at least two, and a positive inverse temperature beta. The same finite measurable visible policy is used for every hidden density sigma_B. Its independently specified physical histories have measurable integrable positive trace-one densities, initial Dirac history law and product preparation rho_A tensor sigma_B. Their next quantum event integrals satisfy the actual finite-step transition equations. Total trace preservation is required almost everywhere on executed active histories, separately for each hidden state.

The conclusion constructs a common probability measure equal to every terminal physical history law. Pushing it through the same returned record map gives the same record law for every hidden density. For every retained measurable record event, the next mass whose preceding history was stopped equals its previous stopped-record mass. No stopping or failure mass is discarded or renormalized.

For the hidden target (log(e) minus von Neumann entropy of sigma_B) divided by beta, the infimum over all real-valued Markov estimator kernels of the supremum over all hidden density states of expected absolute error is exactly log(e) divided by twice beta. Expectation is an extended nonnegative integral, so infinite risks and arbitrary real outputs remain in scope. Pure and maximally mixed hidden states provide the indistinguishable endpoints, and a constant midpoint estimator attains the bound. The logarithm is natural.

The proof constructs the visible history from the actual instruments. Its finite induction identifies joint quantum event integrals with visible event integrals tensored with the fixed hidden density. Taking eventwise traces identifies the independently specified physical classical measure before common-density uniqueness gives the tensor posterior almost everywhere. Measurable cemetery completion outside the normalization domain changes no physical event integral. Record independence is a conclusion, not an interface field.

This is a per-protocol theorem with explicit operational history hypotheses. It does not posit a hidden-state oracle, measurable Kraus selection, full-rank hidden states, a common null set for all hidden states, or a finite classical outcome space. The zero-Hamiltonian Gibbs identity identifies the hidden reference with I/e. Optimizing also over a nonempty legal experiment class is an application of the universal per-protocol value; it is not a separate declaration in this module. The result makes no algorithmic runtime or hidden partition-function counting claim.

References