Concrete RawHistory on the actual diagram
Abstract
SignedOrdinalRawHistory
Definition 1.1 (Concrete RawHistory on the actual diagram).
Lean statement: D5/S3/Topology/InverseLimit/SignedOrdinalRawHistory.rawHistory
Formalization. D5/S3/Topology/InverseLimit/SignedOrdinalRawHistory.rawHistory (✓ std3).
Source. Repository-derived.
Commentary.
The concrete RawHistory on finalPrefix.diagram is populated with the actual U and its surjectivity, original V, whole nu and its surjectivity, actual cofinal launches, permanent disjoint reservoirs, original eligible J, infinite intersections and directed finite differences. Its proper F directly applies the canonical history proper_f through equality of the literal carrier and the original whole measure readback. The actual incoming regular bounded evidence is preserved. The full canonical run remains available with its selected ordinary or delayed Result and quantitative G; RawHistory alone does not encode G.
No final endpoint is asserted.