============================================================================== MVPS MARITIME & TACTICAL-EDGE PROFILE -- MATHEMATICAL PROOF (Coherence monitoring across a fleet of vantages in a Disconnected, Intermittent, Limited (DIL) environment under GNSS-denied clock holdover. Companion to draft-melegassi-ippm-mvps-maritime-edge-00.) "The hard part at sea is not the detector; it is keeping the clocks close enough while the sky is jammed and the link comes and goes." ============================================================================== DEFENSIVE SCOPE. This profile is about DETECTING anomalies in the network / coherence telemetry of a critical maritime or tactical-edge deployment (cyber intrusion, comms tampering, PNT/GNSS spoofing). It contains NO targeting, navigation, fire-control, or kinetic function, produces no such output, and MUST NOT be represented as doing so. Mathematical assembly: Leonardo Melegassi (Catellix) Produced: 2026-05-28 Companion: docs/draft-melegassi-ippm-mvps-maritime-edge-00.txt Inherits: docs/MVPS_ARCH_PROOF.txt (D-8 Architecture-Invariance Theorem) Core: docs/MVPS_MATHEMATICAL_EXISTENCE_PROOF_V4.txt (T1, T2, T9, T3') Method: docs/MVPS_METHODOLOGY_PROOF.txt (claim discipline M-1..M-9) Numerical receipt: scripts/validate_maritime_edge.py (exit 0, 7/7) evidence/maritime_edge_receipt.json ============================================================================== 0. THE ONLY THING THAT CHANGES ============================================================================== MVPS coherence detection rests on five axioms (A1..A5) and promotes its theorems verbatim to any surface that satisfies them (the D-8 Architecture-Invariance Theorem; the same mechanism used by the BBF mesh profile). Four of the five axioms are unaffected at sea: A2 (bundle), A3 (coherence axes), A5 (Byzantine-tolerant aggregator) are structural and carry over; A4 is handled exactly as in the core. Only A1 is at risk. A1 requires the JOINT CLOCK SKEW across vantages to be smaller than the coherence tick: 2 * eps + tau_RTT_max < T_tick. At sea, two things break the terrestrial argument for A1: (i) GNSS time may be DENIED (jammed/spoofed), so a vantage must run on a holdover oscillator that drifts; (ii) the link is INTERMITTENT, so an observation is stored at the source and forwarded later (store-and-forward / DTN). This document proves A1 still holds, on an enlarged tick T_tick_eff, under explicit DIL budgets -- and is honest about when it does not. ============================================================================== 0.1 IMPORTS ============================================================================== Core v4.0 basis I1..I12 (statistics), in particular I12 (Minsker/Cohen, geometric-median max-bias) for A5. Standard sampled-data / holdover-clock model: P1. A free-running oscillator under GNSS denial accumulates time offset bounded by rho * Delta_d over a denial interval Delta_d, where rho is the fractional-frequency holdover drift rate (datasheet OCXO ~ 1e-8 s/s; TCXO ~ 1e-6 s/s). P2. Store-and-forward delivers a source-timestamped observation within bounded latency tau_store; ordering is recovered from the source timestamp, not arrival time. ============================================================================== 1. DEFINITIONS ============================================================================== F-M1. eps_sync : residual sync error at the last GNSS/PTP contact (s). F-M2. rho : holdover fractional-frequency drift rate (s/s). F-M3. Delta_d : maximum GNSS-denied (disconnect) interval a vantage must tolerate before re-sync (s). F-M4. tau_store: maximum store-and-forward delivery latency for a source-timestamped bundle over the intermittent link (s). F-M5. EFFECTIVE JOINT SKEW under DIL: skew_eff = 2 * ( eps_sync + rho * Delta_d ) + tau_store . F-M6. T_tick_eff : the enlarged coherence tick chosen by the operator. ============================================================================== 2. LEMMAS AND THEOREMS ============================================================================== ------------------------------------------------------------------------------ L-MAR-1 [T]. (A1 under DIL.) If skew_eff = 2*(eps_sync + rho*Delta_d) + tau_store < T_tick_eff, then axiom A1 holds for the maritime deployment on tick T_tick_eff. ------------------------------------------------------------------------------ Proof. At worst case two vantages are each off true time by their holdover bound eps_sync + rho*Delta_d (P1), in opposite directions, contributing 2*(eps_sync + rho*Delta_d) to pairwise skew. A source-timestamped bundle is placed in its tick window using its source timestamp; the only added uncertainty is that the bundle is observed up to tau_store later, which the window assignment absorbs as long as tau_store < T_tick_eff (P2, and L-MAR-4). Summing gives skew_eff; the hypothesis is exactly the A1 inequality on T_tick_eff. [] Validator: L-MAR-1 (OCXO 5.0037 s, TCXO 5.0092 s, stress 51.748 s, all < 60 s). ------------------------------------------------------------------------------ L-MAR-2 [T]. (Maximum tolerable denial.) For fixed eps_sync, rho, tau_store, T_tick_eff, the largest disconnect interval preserving A1 is Delta_d_max = ( T_tick_eff - tau_store - 2*eps_sync ) / ( 2*rho ). ------------------------------------------------------------------------------ Proof. Set skew_eff = T_tick_eff and solve for Delta_d. Monotonicity (L-MAR-3) makes the threshold one-sided. [] Validator: L-MAR-2 (TCXO: Delta_d_max ~ 318 days; round-trips to exactly 60.000000 s). OBSERVE: with a decent oscillator the BINDING constraint is tau_store, not drift -- the sea problem is the link, not the clock. ------------------------------------------------------------------------------ L-MAR-3 [T]. (Monotonicity.) skew_eff is strictly increasing in each of rho, Delta_d, tau_store. ------------------------------------------------------------------------------ Proof. Partial derivatives 2*Delta_d, 2*rho, 1 are all positive. [] Validator: L-MAR-3. ------------------------------------------------------------------------------ L-MAR-4 [T] + [D]. (Store-and-forward tick assignment.) A source-timestamped bundle delivered after tau_store is assigned to its correct tick window iff tau_store < T_tick_eff. If tau_store >= T_tick_eff the operator MUST enlarge T_tick_eff (a Design choice), else A1 fails. ------------------------------------------------------------------------------ Proof. The window index is floor(source_ts / T_tick_eff); a delivery delay strictly below one tick cannot move a sample across a window boundary relative to its source-stamped index. At tau_store >= T_tick_eff the delayed sample can land two windows away, breaking the joint observation. [] Validator: L-MAR-4 (feasible accepted; infeasible config skew 70.009 s >= 60 s correctly rejected). ------------------------------------------------------------------------------ T-MAR-INHERIT [T]. (Inheritance.) If A1 holds on T_tick_eff (L-MAR-1) and the compromised-vantage fraction f < 1/2, then the core theorems T1 (D^2 dominance), T2 (Phi_D concentration), T3' (empirical FAR), and T9 (Byzantine robustness) hold on the maritime surface VERBATIM, by the D-8 Architecture-Invariance Theorem. ------------------------------------------------------------------------------ Proof. D-8 promotes any core theorem to a surface satisfying A1..A5. A2, A3, A4, A5 are inherited unchanged; A1 is re-established by L-MAR-1. The premise set of D-8 is met; promotion is immediate. [] Validator: A-MAR-INHERIT (promotes T1, T2, T9, T3' at f = 0.2). ------------------------------------------------------------------------------ B-MAR-1 [T]. (Byzantine ships.) With f < 1/2 of vantages compromised, lying, or destroyed, the geometric-median aggregator has finite max-bias b(f) = C * f/(1-2f) (I12, Minsker/Cohen), diverging only as f -> 1/2. ------------------------------------------------------------------------------ Proof. Direct from I12 applied to the vantage observation set; the maritime surface changes neither the aggregator nor the bound. [] Validator: B-MAR-1 (b(0.2)=0.333, b(0.4)=2.000, b(0.5)=inf). ============================================================================== 3. CONJECTURE (with falsification protocol -- methodology M-6) ============================================================================== C-MAR-1. CONJECTURE: coordinated PNT/GNSS spoofing across a fleet injects a rank-low, correlated clock-offset signature that the multi-vantage D^2 detector flags BEFORE any single vantage crosses its per-node threshold. (a) observable: cross-vantage correlated clock-offset jump versus per-vantage max-z, on the coherence tick; (b) data source: fleet PTP/GNSS offset telemetry plus a controlled GNSS-spoofing testbed (record-and-replay); (c) test: one-sided detection-time advantage, Wilson 95% lower bound > 0; falsified if the lower bound <= 0; (d) current blocker: access to a controlled GNSS-spoofing range; held as [C] until that receipt exists. This conjecture is NOT promoted to a theorem. The PROFILE's guarantees (L-MAR-1..B-MAR-1) do not depend on it. ============================================================================== 4. WHAT THIS PROVES / DOES NOT PROVE ============================================================================== Proves: (i) A1 holds at sea under explicit, datasheet-grounded DIL budgets (L-MAR-1), with a closed-form denial tolerance (L-MAR-2); (ii) the binding constraint is store-and-forward latency, not clock drift, for any reasonable oscillator (L-MAR-2 remark, L-MAR-4); (iii) the core detection and Byzantine theorems inherit verbatim (T-MAR-INHERIT, B-MAR-1). Does NOT prove / explicitly disclaims: (a) any PNT-spoofing detection guarantee (that is conjecture C-MAR-1); (b) operation when tau_store >= T_tick_eff without enlarging the tick; (c) anything outside DEFENSIVE coherence monitoring -- no kinetic, targeting, or navigation claim exists or is implied. ============================================================================== 5. REFERENCES ============================================================================== [I-D.melegassi-ippm-mvps-maritime-edge] this document's companion draft. [ARCH] draft-melegassi-iab-mvps-architecture-00 (D-8 invariance). [MVPS-V4] MVPS Mathematical Existence Proof v4.0 (T1, T2, T9, T3'). [I12] Minsker, S.; Cohen, M., geometric-median max-bias. [BBF-MESH] draft-melegassi-ganascim-mvps-bbf-mesh-00 (same inheritance pattern over a different surface). ============================================================================== END OF MVPS MARITIME & TACTICAL-EDGE PROFILE MATHEMATICAL PROOF ==============================================================================