Promote the E2 finite joint instances to an actual locally covariant net. Define the admissible event-region and causal-embedding category, construct the functor into finite/limit observable algebras, prove naturality of the public-record subfunctor, and establish isotony, locality, refinement independence, and the time-slice property for the declared Cauchy embeddings. Supply at least one inhabited nontrivial example. E2 remains a finite common-refinement package and does not itself discharge this limit.
Boundary: E2 must already carry source-produced channel/instrument and refinement-natural scheduler receipts. E3 promotes those data through the continuum/causal-embedding construction and owns the time-slice theorem; it does not retroactively infer CP/CPTP or adaptive physical locality from B2's Kraus normalization/trace identities or E1's finite interface.
Deliverables: QFT/LocallyCovariantLimit.lean, QFT/PublicRecordSubfunctor.lean, QFT/TimeSlice.lean, typed assumption/countermodel matrix.
Depends on: E2 (#693) and A4 (#699, closed bounded).
Wave: V2-W3 Covariant net and gravity.
Promote the E2 finite joint instances to an actual locally covariant net. Define the admissible event-region and causal-embedding category, construct the functor into finite/limit observable algebras, prove naturality of the public-record subfunctor, and establish isotony, locality, refinement independence, and the time-slice property for the declared Cauchy embeddings. Supply at least one inhabited nontrivial example. E2 remains a finite common-refinement package and does not itself discharge this limit.
Boundary: E2 must already carry source-produced channel/instrument and refinement-natural scheduler receipts. E3 promotes those data through the continuum/causal-embedding construction and owns the time-slice theorem; it does not retroactively infer CP/CPTP or adaptive physical locality from B2's Kraus normalization/trace identities or E1's finite interface.
Deliverables:
QFT/LocallyCovariantLimit.lean,QFT/PublicRecordSubfunctor.lean,QFT/TimeSlice.lean, typed assumption/countermodel matrix.Depends on: E2 (#693) and A4 (#699, closed bounded).
Wave: V2-W3 Covariant net and gravity.