LF2 ↔ LF1 interface #
Category: 3-Local (LF1 ↔ LF2 weight identity plus combined LF1_main_theorem_projective headline theorem).
Spec §6. The measure-theoretic identity linking the LF1 ontic weight
μprep(π⁻¹(O)) to the LF2 projective weight (π*μprep)(O).
This is the cleanest theorem in the LF2 stack: a single application of
Measure.map_apply. Its role is structural — it is the formal connection
point for LF1_main_theorem_ae to speak about projective outcome weights,
and the hinge by which LF2's measure bridge feeds back into the LF1 frequency
theorem.
Spec §6.2 — the LF1 ↔ LF2 weight identity. The ontic mass of the pulled-back outcome region under a preparation measure equals the projective weight of that region under the pushforward preparation.
Specialisation of lf1_weight_eq_projective_weight to the LF1 conditional
preparation measure S.prepMeasure. This is the exact form consumed by a
caller who has invoked LF1_main_theorem_ae for some
T : S.TrialModel Ω and wants to reinterpret the limiting ontic weight
as a projective weight.
Projective-first outcome constructor #
SectorData.outcomeOfProjective builds an LF1 ontic OutcomeRegion
from a measurable projective region Oep ⊆ P by taking the π-preimage:
Ω := D.π ⁻¹' Oep. The constructor itself requires only measurability
of Oep.
The flow-projection compatibility hypothesis
∀ x, D.π (D.toOntic.Φ x) = D.π x (CSD's constraint-surface
preservation reading — the ontic flow preserves projective rays) is
not consumed by the constructor itself. It is consumed by the
companion lemma outcomeOfProjective_preEvent to identify
preEvent = Ω (i.e. to fold the LF1 one-step-ahead pullback into the
plain preimage), which is what LF1_main_theorem_projective and the
LF3 chain capstones need.
Architectural rationale: the Φ-π compatibility hypothesis is supplied
as a lemma argument rather than as a field on SectorData —
adding a field would commit all SectorData instances to the
constraint-surface reading, which is LF4 instantiation work. Keeping
it on the per-lemma side lets the projective-first outcome family be
built at the LF3 chain capstone with a single CSD-foundational
hypothesis.
Projective-first outcome constructor. Given a measurable
projective region Oep ⊆ P, returns the ontic OutcomeRegion
with Ω := D.π ⁻¹' Oep. The constructor requires only hOep;
flow-projection compatibility is consumed by the companion lemma
outcomeOfProjective_preEvent, which identifies preEvent = Ω.
The companion lemma outcomeOfProjective_weight_eq_projectiveWeight
gives the projective-side reformulation of the LF1 outcome weight.
Instances For
Unfolding lemma: the ontic outcome region's underlying set is the projection preimage.
Pre-event of outcomeOfProjective equals π⁻¹(Oep) under the
flow-projection compatibility hypothesis. This is the lemma that
discharges the hCorresp argument of LF1_main_theorem_projective
for the constructor-built outcome region.
Weight of outcomeOfProjective equals the projective weight of
Oep under the flow-projection compatibility hypothesis. Direct
consequence of outcomeOfProjective_preEvent and
lf1_weight_eq_projective_weight.
Combined LF1 + LF2 main theorem. Under the LF1 repeated-trial model
and an LF2 sector structure with projection π, if an LF1 outcome
region's pre-event coincides with the π-preimage of a projective
outcome region Oep, then the empirical frequency converges almost
surely to the (real-valued) projective weight of Oep under the
pushforward of the preparation measure.
This is the theorem-level consumption of LF1 by LF2: it shows that the LF1 limit is not merely an ontic volume fraction but can be reinterpreted natively in the projective measurable space that LF2 introduces. No new mathematical content beyond LF1 + the LF2 interface identity — the point is the combined statement.
A full Born-form conclusion (‖⟨ψ, φ⟩‖²) would require an additional
spec-layer correspondence between measure-theoretic projective
preparations and Hilbert-space unit vectors, which LF2 does not
formalise. See spec §6.4 and §8.5.