Documentation

CsdLean4.SigmaLayer.LiftedMeasurement

SigmaLayer/LiftedMeasurement: the concrete de-isolation model from the LF5 pointer machinery #

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

The concrete DeisolationModel for Tranche 2b, on the dilated projective sector CP^{M} (M + 1 = N * N). The physical interaction is the LF5 von Neumann de-isolation flow measurementFlow (a genuine measure-preserving unitary map), and the contextual readout is the LF5 per-microstate pointer outcome vnPointerOutcome. The outcome regions are the pointer fibres, so the readout is a genuine function (hence the outcome is unique), the fibres are pairwise disjoint, and the readout equals some i exactly on the i-th region. Almost-everywhere totality (the outcome is defined off an FS-null set, transferred through the measure-preserving interaction) is vnDeisolationModel_ae_total.

Crucially, the model reproduces the Born STATISTICS, not merely a defined outcome: for the dilated system state ψ' and i.i.d. FS-typical trials, the frequency of trials whose de-isolation readout is pointer i converges almost surely to ‖⟨eᵢ, ψ⟩‖² (vnDeisolationModel_born_frequency). This is the LF5 outcome-frequency capstone measurement_flow_outcome_frequency transferred through the measure-preserving interaction, so the frequency is about the model's OWN outcome (readout after the interaction), not the raw microstate. lifted_projectiveSector_measurement_born_capstone bundles the full measurement: measure preservation, unique outcome a.e., record establishment, and Born frequencies.

This is a theorem-backed construction, not an assumed instance: every field is discharged by an LF5 lemma. The isolated dynamics is trivial here (trivialDynamics); the physical content is the de-isolation interaction.

The record signature of the von Neumann pointer measurement: a single fixed context, outcome type Fin N (the pointer index).

Equations
Instances For
    noncomputable def CSD.SigmaLayer.vnRecordSemantics {N M : } (e : Fin N × Fin N Fin (M + 1)) (ψ' : EuclideanSpace (Fin (M + 1))) (hψ'0 : ψ' 0) :

    The record semantics: the event of pointer outcome i is the pointer fibre vnPointerOutcome ⁻¹' {some i} on CP^{M}.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def CSD.SigmaLayer.vnDeisolationModel {N M : } [NeZero N] (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N Fin (M + 1)) (ψ' : EuclideanSpace (Fin (M + 1))) (hψ'0 : ψ' 0) :

      The concrete de-isolation model. Interaction = the LF5 measurement flow (measure-preserving unitary); readout = the LF5 pointer outcome; outcome regions = the pointer fibres. Every field is discharged by an LF5 lemma. Preparation type is Unit (the reference state ψ' is fixed).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem CSD.SigmaLayer.vnDeisolationModel_records {N M : } [NeZero N] (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N Fin (M + 1)) (ψ' : EuclideanSpace (Fin (M + 1))) (hψ'0 : ψ' 0) :

        The readout records the established outcome (B5 proved for the model). If the pointer readout after the interaction is some i, the post-interaction state lies in the record event for i.

        theorem CSD.SigmaLayer.vnDeisolationModel_ae_total {N M : } [NeZero N] (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N Fin (M + 1)) (ψ' : EuclideanSpace (Fin (M + 1))) (hψ'0 : ψ' 0) (hψ' : ψ' = 1) :

        Almost-everywhere unique outcome (T6 for the model). For almost every initial ontic state (Fubini-Study measure), the pointer readout after the de-isolation interaction is defined: the outcome is established a.e. Uniqueness is automatic (the readout is a function; its fibres are pairwise disjoint). Transfers bornOutcome_ae_isSome through the measure-preserving interaction.

        The lifted projective sector measurement capstone. For the concrete de-isolation model on CP^{M} (M + 1 = N * N), with the LF5 measurement flow as the physical interaction and the LF5 pointer outcome as the contextual readout, the following hold with no open hypotheses beyond a unit reference state:

        • the interaction is measure-preserving (DeisolationModel.interaction_preserves);
        • the outcome regions (pointer fibres) are pairwise disjoint, so the recorded outcome is unique;
        • the readout records the established outcome (bridge B5);
        • the outcome is established for almost every initial ontic state (target T6).

        This is the contextual pointer readout and almost-everywhere unique outcome that the product forward capstone product_projectiveSector_forward_capstone explicitly did not claim: the measurement content, delivered from a genuine de-isolation interaction rather than an assumed instance.

        theorem CSD.SigmaLayer.vnDeisolationModel_born_frequency {N M : } [NeZero N] (hN : 1 < N) (e : Fin N × Fin N Fin (M + 1)) (ψ : EuclideanSpace (Fin N)) ( : ψ = 1) (ψ' : EuclideanSpace (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 e) ((Matrix.toEuclideanLin (LF5.vnDilationV N)) ψ)) (hψ'0 : ψ' 0) (p₀ : LF4.CPN (M + 1)) :
        ∀ᵐ (ω : LF4.fsTrialSpace (M + 1)) LF4.fsTrialMeasure p₀, ∀ (i : Fin N), Filter.Tendsto (fun (m : ) => (∑ kFinset.range m, (LF5.measurementFlow N e LF4.fsTrial (M + 1) k ⁻¹' LF5.vnPointerOutcome ψ' hψ'0 e ⁻¹' {some i}).indicator (fun (x : LF4.fsTrialSpace (M + 1)) => 1) ω) / m) Filter.atTop (nhds (inner (EuclideanSpace.single i 1) ψ ^ 2))

        The model reproduces the Born statistics (the measurement content). For the dilated system state ψ' (the von Neumann dilation of a unit system state ψ) and i.i.d. FS-typical trials, the frequency of trials whose de-isolation readout is pointer i converges almost surely to the Born weight ‖⟨eᵢ, ψ⟩‖². The event (interaction ∘ trial)⁻¹' (readout⁻¹' {some i}) is exactly "the model reads pointer i on this trial", the readout applied AFTER the model's interaction.

        This is the LF5 outcome-frequency capstone measurement_flow_outcome_frequency transferred through the measure-preserving interaction: the composed trial process measurementFlow ∘ fsTrial still samples the Fubini-Study law (measure preservation), and its per-trial indicators are still independent (a fixed deterministic map of independent trials), so the Born weights are unchanged. Hence the frequency is a genuine statistic of the model's own outcome, not of the raw microstate.

        The full lifted projective sector measurement capstone (with Born statistics). For the concrete de-isolation model on the dilated sector, with the system state ψ' the von Neumann dilation of a unit state ψ, the following hold with no open hypotheses beyond the dilation data:

        • the interaction is measure-preserving;
        • the outcome regions (pointer fibres) are pairwise disjoint, so the recorded outcome is unique;
        • the readout records the established outcome (bridge B5);
        • the outcome is established for almost every initial ontic state (target T6);
        • the frequency of pointer-i readouts converges almost surely to the Born weight ‖⟨eᵢ, ψ⟩‖².

        This is the genuine measurement: a defined, unique outcome a.e. AND the Born statistics, delivered from a de-isolation interaction rather than an assumed instance.