Manuscript En08-A@1 · En08-A.tex · section · c688d76d
Audit of the lemma ladder
An audited reconstruction sequence › Audit of the lemma ladder · lines 2176–2236
The following checklist records the proof obligations underlying the conditional results summarized in Figure fig:ladder.
| Step | Required statement |
|---|---|
| Step | Required statement |
| L1 | Retain occurrence identity. Equal support and residual state do not identify distinct events. |
| L2 | Use dependency reachability as an order candidate. Prove sensitivity–reachability equivalence separately. |
| L3 | Acyclicity yields an order. Strongly connected quotienting also does so, but neither proves that cycles are exactly inconsistent records. |
| L4 | Derive ownership disjointness from channel discipline and simultaneous enabledness, not from no-signaling alone. |
| L5 | Use (eq:recurrence). Minkowski addition needs a fixed increment representation. |
| L6 | The ball and orthant constructions refute selection from the operational assumptions alone. |
| L7 | Prove a relay for actual event pairs. Closure of a displacement set does not supply protocols. |
| L8 | A causal order does not uniquely determine chronology. Proper cones give a conditional construction. |
| L9 | Interpolation alone gives neither an interval basis nor a manifold. |
| L10 | Quadratic signature selection requires a full negative component with pointed closure and a nonempty positive region. |
| L10a | Uniform local shapes are not . Apply Theorem thm:representation, or the precisely cited weaker Theorem thm:weaker. |
| L10b | Separate cone automorphisms from their possible lifts to records, and generated-cone boundaries from attained displacements. |
| L11 | Use explicit causal-origin rules. The criterion concerns free uses, not unused context entries. |
| L12 | Apply conformal reconstruction only after Lorentzian realizability. |