Documentation

CsdLean4.SigmaLayer.UnifiedFlowedRecords

SigmaLayer/UnifiedFlowedRecords: time-indexed records ON the unified model (#5) #

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

unified_projectiveSector_capstone (UnifiedMeasurement.lean) bundles the dynamics + measurement core of the ONE ontic model productDynamics H hH p₀ on Σ = ℂℙ^M × T², but its record layer vnRecordSemanticsProd uses a STATIC event (it ignores the recorded time). This module puts the GENUINELY TIME-INDEXED record semantics flowedSemantics onto that same model, with the ISOLATED Hamiltonian flow Φ = exp(-itH) as the evolution — so the model's records become time-physical, with the persistence (probability conserved + flow-covariant) of flowedSemantics_persistence instantiated on it.

The construction is pure assembly: flowedSemantics needs a base outcome-region family, its measurability, and outcome-exclusivity — all three are exactly the fields already proved in vnRecordSemanticsProd. The static vnRecordSemanticsProd is recovered as the t = 0 slice (unifiedFlowedSemantics_zero), so nothing about the working capstone changes; this ADDS the time-indexed layer.

What this establishes (all on the unified model productDynamics H hH p₀) #

So the "records are time-physical on the unified model" claim, previously supported only by the generic flowedSemantics, is now instantiated on the actual model — the piece L9 needs to list records in the "proved on the unified model" tier.

References: SigmaLayer/UnifiedMeasurement.lean (vnRecordSemanticsProd, unifiedDeisolationModel), SigmaLayer/TimeIndexedRecord.lean (flowedSemantics, flowedSemantics_persistence).

source
noncomputable def CSD.SigmaLayer.unifiedFlowedSemantics {N M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) :
RecordSemantics (LF4.KSigma (M + 1)) (vnRecordSignature N)

Time-indexed records on the unified model. flowedSemantics over the isolated flow productDynamics H hH p₀, with base region = the pointer fibre (the same region vnRecordSemanticsProd uses), its measurability and exclusivity reused verbatim. event ⟨c,i,t⟩ = Φ_t⁻¹'(pointer fibre i).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CSD.SigmaLayer.unified_records_persistence {N M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (c : (vnRecordSignature N).Context) (i : (vnRecordSignature N).Outcome c) :
    (∀ (t : OnticTime), ↑(productDynamics H hH p₀).muL ((unifiedFlowedSemantics H hH p₀ e ψ' hψ'0).event { context := c, outcome := i, time := t }) = ↑(productDynamics H hH p₀).muL ((fun (x : LF4.KSigma (M + 1)) => LF5.vnPointerOutcome ψ' hψ'0 e x.1) ⁻¹' {some i})) ∧ ∀ (s t : OnticTime), (unifiedFlowedSemantics H hH p₀ e ψ' hψ'0).event { context := c, outcome := i, time := t + s } = (productDynamics H hH p₀).flow s ⁻¹' (unifiedFlowedSemantics H hH p₀ e ψ' hψ'0).event { context := c, outcome := i, time := t }

    Records are time-physical on the unified model. For every context/outcome, the time-indexed record probability is conserved by the isolated Hamiltonian evolution AND the record transforms covariantly with the flow — flowedSemantics_persistence instantiated on productDynamics H hH p₀. So the unified model's records are genuine time-physical evidence carried consistently by its own isolated dynamics.

    source
    theorem CSD.SigmaLayer.unifiedFlowedSemantics_zero {N M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (c : (vnRecordSignature N).Context) (i : (vnRecordSignature N).Outcome c) :
    (unifiedFlowedSemantics H hH p₀ e ψ' hψ'0).event { context := c, outcome := i, time := 0 } = (vnRecordSemanticsProd e ψ' hψ'0).event { context := c, outcome := i, time := 0 }

    Consistency: the static capstone semantics is the t = 0 slice. At t = 0 the time-indexed record event coincides with vnRecordSemanticsProd's (since Φ₀ = id), so adding the flowed layer does not disturb unified_projectiveSector_capstone.

    #2: Born-frequency ON the unified model #

    manyToOneSetup_born_frequency (the independent-trial LLN Born frequency) transfers directly to the unified model, because (productDynamics H hH p₀).muL = (manyToOneSetup (schrodingerUnitary hH) p₀) .liouvilleMeasure (by productDynamics_muL_eq, itself rfl) and (productSector H hH p₀).pi is that setup's π. So the Born frequencies are stated on the SAME model that carries the dynamics, measurement, and records — no separate base object.

    source
    theorem CSD.SigmaLayer.unified_born_frequency {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (X : ℕ → Ω → LF4.KSigma (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = ↑(productDynamics H hH p₀).muL) (hindep : ∀ (i : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' (productSector H hH p₀).pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator fun (x : Ω) => 1)) :
    ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' (productSector H hH p₀).pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

    Born frequency on the unified model. For i.i.d. trials X whose law is the unified model's own Liouville measure (productDynamics H hH p₀).muL, the frequency of trials landing in the i-th outcome region π⁻¹(bornRegion i) converges a.s. to the Born weight ‖⟨eᵢ,ψ⟩‖². A direct transfer of manyToOneSetup_born_frequency through the definitional identity productDynamics.muL = liouvilleMeasure — so Born frequencies are now stated on the unified model itself.