Carrier-Relative First Contact: A Mechanized Toy Theorem on Inscription, Carrier, Transport, and Replay

This release contains a short research note and Lean 4 formalization kernel on carrier-relative interpretation in first-contact protocols. The motivating example is the Short-Time Fourier Transform (STFT). The central claim is not that the STFT equation is wrong, nor that mathematics is not universal. The claim is narrower: a raw mathematical inscription is not self-grounding. It becomes meaningful only relative to a carrier: symbols, syntax, operations, units, gauge conventions, semantics, and verification procedures. The note proves a toy-model theorem in Lean 4 showing that no carrier-independent interpretation function can agree with all admissible carrier interpretations. It also mechanizes an acceptance-obstruction result: two carriers with incompatible acceptance conditions admit no lawful transport when transport must preserve acceptance. The paper applies these formal results to first-contact protocol design. It argues that formula transmission should be downstream of carrier discovery, gauge alignment, lawful transport, finite replay, and terminalization. The STFT equation is therefore treated as a late-stage compression of a shared carrier, not as a first-contact primitive. This release includes:- the research note,- the Lean 4 proof kernel,- a public-facing summary,- proof ledger and scope notes,- explicit non-claims and future formalization targets.