OP-from-preparation construction (pre-LF4 Phase 3)

Category: 3-Local (pre-LF4 plan Phase 3 sub-component 3a — MeasureBridgeData bundle).

This module defines:

• MeasureBridgeData D μFS — a structure bundling the projective reference measure μFS, its G-invariance, the bridge constant c : ENNReal, and the bridge equality Measure.map D.π D.μL = c • μFS. Passive data: callers supply the bridge equality directly, and the concrete instances supply it axiom-free (CSD.LF4.cp_measure_bridge, k_measure_bridge).
• OperationalPackage.fromPreparation — the projective Born wrapper (representation layer), which takes a MeasureBridgeData D μFS argument but does not extensionally invoke its bridge_eq content in the operational-axiom field proofs, so #print axioms on it reads only the foundational triple.
• MeasureBridgeData.integral_comp_pi + OperationalPackage.fromPreparation_liouville_apply — the theorems in which bridge_eq is extensionally consumed (F-01 discharge, 2026-08-06): the bridge equality transports the ontic volume integral over Σ into the projective reference integral, and for the Liouville preparation of a c = 1 bridge the operational probability IS the μFS-integral of the effect function. This is the load-bearing form of the symmetry datum; in fromPreparation itself the bridge stays type-level (see below).

History note (2026-06-04)

Earlier revisions carried an axiom-citing constructor MeasureBridgeData.ofSectorData, which derived the bridge fields from the abstract measure_bridge lemma and so cited the invariant_measure_uniqueness axiom; the option-(b) discipline of specs/pre-LF4-plan.md was to route the chain through it to keep the citation in the audit. Both the constructor and the abstract measure_bridge/axiom were removed once it was clear nothing downstream used them (the concrete instances build the bridge directly and axiom-free), leaving busch_effect_gleason as the corpus's only imported axiom — itself discharged 2026-07-21 (proved as effect_gleason_representation); the corpus has imported zero axioms since.

structure CSD.LF2.MeasureBridgeData {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) : Type

Measure-bridge data. Bundles the projective reference measure μFS, its G-invariance, the bridge constant c : ENNReal, and the bridge equality Measure.map D.π D.μL = c • μFS. The structure is passive data: its fields are not extensionally consumed by OperationalPackage.fromPreparation's operational-axiom proofs, and callers supply the bridge equality directly. The concrete instances supply it axiom-free (CSD.LF4.cp_measure_bridge, k_measure_bridge — c = 1, trivial / product-marginal fibres).

(The earlier axiom-citing constructor ofSectorData, which derived the fields from the abstract measure_bridge / invariant_measure_uniqueness, was removed 2026-06-04 — see LF2/MeasureBridge.lean. Nothing used it.)

μFS is taken as an explicit (Type-level) field rather than carried in the structure because callers may want to instantiate the same SectorData with different reference measures; the MeasureBridgeData ties a specific μFS to its bridge facts.

• is_inv (g : G) : MeasureTheory.MeasurePreserving (fun (x : P) => g • x) μFS μFS

  Each epistemic action map g • · preserves μFS.

• c : ENNReal

  The bridge constant: π_*μL = c • μFS.

• bridge_eq : MeasureTheory.Measure.map D.π D.μL = self.c • μFS

  The bridge equality.

theorem CSD.LF2.MeasureBridgeData.integral_comp_pi {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {D : SectorData SigmaSpace P G} {μFS : MeasureTheory.Measure P} (bridge : MeasureBridgeData D μFS) {f : P → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μFS) : ∫ (σ : SigmaSpace), f (D.π σ) ∂D.μL = bridge.c.toReal • ∫ (p : P), f p ∂μFS

The bridge transports ontic integrals to projective integrals (F-01 discharge, 2026-08-06). For any μFS-a.e.-strongly-measurable f : P → ℝ, the ontic integral of f ∘ π against the Liouville measure equals c.toReal times the projective integral of f against the reference measure:

∫ σ, f (D.π σ) ∂D.μL = c.toReal • ∫ p, f p ∂μFS.

This is the theorem in which bridge_eq is extensionally consumed — the symmetry datum doing real work: an ontic volume computation over Σ is carried into the projective probability integrand. The 2026-08-06 external review (F-01) observed that no theorem consumed bridge_eq; this and fromPreparation_liouville_apply are the response. #print axioms reads only the foundational triple (the concrete bridge instances are axiom-free).

Operational package from a preparation

OperationalPackage.fromPreparation constructs the operational probability assignment by integrating the projective effect function effectProjFn rep E against the pushforward Measure.map D.π μprep. The four operational-axiom fields (nonneg, le_one, total_one, additivity) follow from the pointwise content of effectProjFn plus standard Bochner integration facts.

The MeasureBridgeData argument is type-level only: the fromPreparation proof body does not extensionally invoke bridge.bridge_eq or any other field for the operational-axiom checks. Hence #print axioms OperationalPackage.fromPreparation itself reports only the foundational triple.

MeasureBridgeData is supplied directly by the concrete instances, whose bridge proofs are axiom-free; nothing here forces the (now-removed) abstract bridge or its axiom. See the module docstring history note.

noncomputable def CSD.LF2.OperationalPackage.fromPreparation {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : OperationalPackage N

OperationalPackage.fromPreparation (the projective Born wrapper, structural form). Given a SectorData, the bridge data bridge : MeasureBridgeData D μFS, a probability preparation measure μprep, and a unit-norm measurable representative rep : P → EuclideanSpace ℂ (Fin N), the operational probability assignment is integration of effectProjFn rep E against the pushforward π_*μprep.

Equations

• One or more equations did not get rendered due to their size.

Pure preparation and the Born rank-1 theorem

A PurePreparation packages a Hilbert-space unit vector ψ, the caller-supplied projective representative map rep, a projective point ray_point : P whose rep-image is ψ, and the Dirac-concentration hypothesis Measure.map D.π μprep = Measure.dirac ray_point expressing that the preparation concentrates on the projective ray through ψ.

Two Born theorems are proved:

• PurePreparation.born_rank_one (chain critical path) — derives OP.p (rankOneEffect φ hφ) = ‖⟨ψ, φ⟩‖² by composing the volume-content step (OP_certain_at_ψ) with the Busch packaging step (pure_state_born_weights_of_certainty). Matches spec §5.4 four- ingredient combinatorial framing.
• PurePreparation.born_rank_one_direct (direct auxiliary, representation layer) — derives the same conclusion by direct Dirac integration of effectProjFn rep (rankOneEffect φ hφ) against Measure.dirac ray_point, without invoking busch_effect_gleason. Tagged as the eventual migration target for the chain capstones once downstream consumers accommodate the leaner cite set; v1.00 chain stays Busch-mediated per spec §5.4.

structure CSD.LF2.PurePreparation {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) (μprep : MeasureTheory.Measure SigmaSpace) (N : ℕ) : Type u_2

Pure preparation. A bundle expressing that the projective pushforward of an ontic preparation measure is the Dirac on the ray through a specified Hilbert-space unit vector ψ. Carries the caller-supplied representative map rep and the equality rep ray_point = ψ linking abstract projective points to Hilbert vectors.

• ψ : EuclideanSpace ℂ (Fin N)

  The Hilbert-space unit vector representing the pure preparation.

• unit_ψ : ‖self.ψ‖ = 1

  ψ is a unit vector.

• rep : P → EuclideanSpace ℂ (Fin N)

  The caller-supplied projective-to-Hilbert representative map.

• hrep_unit (p : P) : ‖self.rep p‖ = 1

  rep lands on unit vectors.

• hrep_meas : Measurable self.rep

  rep is measurable.

• ray_point : P

  The abstract projective point of the preparation.

• rep_at_ray : self.rep self.ray_point = self.ψ

  rep evaluates to ψ at the preparation's projective point.

• push_dirac : MeasureTheory.Measure.map D.π μprep = MeasureTheory.Measure.dirac self.ray_point

  The Dirac-concentration hypothesis: the projective pushforward of μprep is the Dirac on ray_point.

theorem CSD.LF2.PurePreparation.OP_certain_at_ψ {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (PP : PurePreparation D μprep N) : (OperationalPackage.fromPreparation D μFS bridge μprep PP.rep ⋯ ⋯).p (rankOneEffect PP.ψ ⋯) = 1

OP is certain at ψ (volume content). For a pure preparation, the operational package built by OperationalPackage.fromPreparation assigns probability 1 to the rank-1 effect through ψ. Proof is direct Dirac evaluation on the volume integral: effectProjFn at the rank-1 effect reduces to ‖⟨rep p, ψ⟩‖², which at p = ray_point becomes ‖⟨ψ, ψ⟩‖² = 1 by rep_at_ray and unit_ψ. This is the "preparation-dependent density ρ_ep" content of spec §5.4 (third bullet).

theorem CSD.LF2.PurePreparation.born_rank_one {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (PP : PurePreparation D μprep N) (hN : 2 ≤ N) (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : (OperationalPackage.fromPreparation D μFS bridge μprep PP.rep ⋯ ⋯).p (rankOneEffect φ hφ) = ‖inner ℂ PP.ψ φ‖ ^ 2

Born quadratic form for pure preparations (Busch-mediated form, chain critical path). For a pure preparation and a rank-1 effect through φ, the operational package assigns ‖⟨ψ, φ⟩‖². Proof composes the volume-content step (OP_certain_at_ψ) with the Busch packaging step (pure_state_born_weights_of_certainty, which uses the proved effect_gleason_representation — formerly the busch_effect_gleason axiom, discharged 2026-07-21 — plus rankOneDensity_unique_of_certainty + born_quadratic).

Busch is a spec-faithfulness choice, not a mathematical necessity

The Born quadratic form on fromPreparation is also derivable without busch_effect_gleason: the Busch-free route is born_rank_one_direct below (direct Dirac integration of the projective effect function). So in the LF2-only Hilbert-space view, the chain capstone is not mathematically dependent on the Busch axiom.

The Busch route is retained as the chain's headline form for two spec-faithfulness reasons:

1. Spec §5.4 four-ingredient framing. The paper presents the Born derivation as the combinatorial composition: measure bridge + ρ_ep + operational consistency + Busch effect-Gleason. The Lean chain's headline cites those four ingredients literally. Removing Busch (and switching the chain capstones to the direct form) would deviate from this presentation.

2. Trace-form characterisation. Busch effect-Gleason is the canonical operational-to-trace-form bridge. Citing it makes explicit that the LF2 wrapper agrees with the standard quantum-mechanical density-operator interpretation, beyond the weaker statement that the projective integral equals ‖⟨ψ, φ⟩‖² for rank-1 effects. The direct form proves the same equation but does not export the trace-form view.

The four-ingredient framing of spec §5.4: measure bridge (via the bridge argument's type), preparation-dependent density ρ_ep (via the volume content of OP_certain_at_ψ), operational consistency package (via the OperationalPackage.fromPreparation construction), Busch effect-Gleason (via pure_state_born_weights_of_certainty).

#print axioms PurePreparation.born_rank_one reads only the foundational triple (AxiomAudit-pinned) — the Busch step is the proved effect_gleason_representation since 2026-07-21. The bridge argument carries no axiom — the concrete instances supply it axiom-free.

theorem CSD.LF2.PurePreparation.born_rank_one_direct {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (PP : PurePreparation D μprep N) (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : (OperationalPackage.fromPreparation D μFS bridge μprep PP.rep ⋯ ⋯).p (rankOneEffect φ hφ) = ‖inner ℂ PP.ψ φ‖ ^ 2

Born quadratic form for pure preparations (direct auxiliary, the representation layer). Same conclusion as born_rank_one, but proved by direct Dirac integration of effectProjFn rep (rankOneEffect φ hφ) against Measure.dirac ray_point, without invoking busch_effect_gleason.

Honest scope (F-02, external review 2026-08-06)

effectProjFn is the Born quadratic form by definition (Re(v†Ev)), so this theorem is a representation/consistency statement: it exhibits the operational probability as the Dirac evaluation of an already-quadratic integrand. What it avoids relative to born_rank_one is the trace-form characterisation step (Busch's effect-Gleason theorem) — not the quadratic form itself. The genuine Born-FROM-VOLUME content (the measure of a separately specified region computed to be the Born weight) lives in the LF4 engine (MomentBornN, BornRegionUncond); cite that, not this, for "Born from volume".

Where the structural inputs actually live (corrected 2026-08-06 — the earlier text claimed symmetry "enters via the bridge argument", overstating a type-level binder):

• Symmetry / the bridge: in THIS theorem the bridge argument is carried type-level only (spec §5.4 four-ingredient framing). Its load-bearing form is MeasureBridgeData.integral_comp_pi and OperationalPackage.fromPreparation_liouville_apply, where bridge_eq is extensionally consumed. The concrete instances supply the bridge axiom-free (CSD.LF4.cp_measure_bridge, k_measure_bridge).
• Operations enter via the OperationalPackage.fromPreparation construction, whose nonneg/le_one/total_one/additivity fields formalise the operational consistency package of spec Definition 5.1 (the four-axiom characterisation of probability assignments on effects).

This is the route the LF3 chain capstones now take (re-routed off Busch 2026-06-02), giving the explicit quadratic-form Born statement (representation layer; see the F-02 scope note above).

#print axioms PurePreparation.born_rank_one_direct cites only the foundational triple [propext, Classical.choice, Quot.sound].

The bridge is load-bearing: the Liouville-preparation transport form

theorem CSD.LF2.OperationalPackage.fromPreparation_liouville_apply {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) [MeasureTheory.IsProbabilityMeasure D.μL] (hc : bridge.c = 1) (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (E : Effect N) : (fromPreparation D μFS bridge D.μL rep hrep_unit hrep_meas).p E = ∫ (p : P), effectProjFn rep E p ∂μFS

The operational probability from the ontic (Liouville) preparation IS the projective reference integral (F-01 discharge, 2026-08-06). For a normalized Liouville measure and a c = 1 bridge (the shape every concrete instance supplies — cp_measure_bridge, k_measure_bridge), the operational package built from the ontic preparation D.μL assigns to every effect exactly the μFS-integral of the effect function:

(fromPreparation D μFS bridge D.μL rep …).p E
  = ∫ p, effectProjFn rep E p ∂μFS.

The proof is bridge_eq doing the work — the pushforward π_*μL is rewritten to μFS inside the volume integral. Together with MeasureBridgeData.integral_comp_pi this is the extensional consumption of the bridge the 2026-08-06 review (F-01) asked for; fromPreparation itself still carries the bridge type-level only, so its own #print axioms hygiene note is unchanged.