Prove max-zero through branch-dependent propagators

[kim-em]

Summary

• add a conformance-local max-zero/ReLU operation with independent nonnegative-side and negative-side propagators
• require each propagator theorem to consume its own exact split assumption
• run both sealed prepared child sessions, pin and replay exactly one rule event per child, and join them with the generic split proof
• produce the ordinary kernel-checked theorem 0 ≤ max x 0 with a guarded dependency report
• reject unsplit top facts and swapped sibling assumptions
• state honestly that conditionality is package-test design for an unconditional theorem, while mathematical necessity remains a future acceptance test
• leave package promotion as an open experimental choice

Validation

• lake build HexIntervalMathlib.ExpSignConformance HexIntervalMathlib.PntLogTableConformance HexInterval.SinTenIntervalConformance HexIntervalMathlib.SinTenConformance HexIntervalMathlib.SinTenIntervalConformance (2244 jobs)
• PNT inventory validation
• copyright, line-count, DAG, released trust-surface, Phase 4, factor-sweep freshness, diff, and banned-proof checks

Reconciled onto exact current main 4cbf00eac03c1e47b053218bad7c123623b5511b, preserving merged #9222/#9256 and the PNT-log, Machin, and endpoint-sine additions.

No native_decide, axiom, or sorry is introduced.