Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A tied jump produces a nonzero cross bracket

Example

Let W∼Exp⁡(λ), λ>0, and put Nt1=Nt2=1{W≤t} with common natural filtration. For each component use Y0i:=1 and Yti:=1{t≤W}=1−(Ni)t− for 0<t≤T, Ati=λ(t∧W), and Mi=Ni−Ai. Both component contracts hold, but the components jump together. For every t>0, [M1,M2]t=Nt,⟨M1,M2⟩t=At, which are nonzero with positive probability. This is why the no-simultaneous-jump condition is required for zero cross brackets.

Facts & Assumptions

Given: λ>0, a waiting time W with density fW(w)=λe−λw on [0,∞) and tail P(W>w)=e−λw, and the common filtration generated by the two identical one-event processes.

[F1]

A unit-jump process with At=∫0tYsλds is in the model class when N−A is a square-integrable martingale and EAT<∞. (Simple counting-process intensity and compensator contract)

[F2]

For that contract, [M]t=Nt and ⟨M⟩t=At. (Brackets of a compensated simple counting process)

[F3]

Optional cross brackets are jump-product sums; predictable cross brackets are their continuous predictable martingale compensators. (Optional and predictable brackets for counting-process martingales)

[F4]

Predictability is generated by time-zero sets and rectangles (s,t]×B with B∈Fs; it is preserved under pointwise limits, products, and deterministic Borel time functions. (Progressively measurable and predictable processes)

[A1]

AC is inherited through conditional expectation in the model contract. (The Axiom of Choice)

Verification

1.1A1F1F4givenconstruct

Each Ni has one unit jump and Y0i=1. For t>0, Yti=1−(Ni)t− is predictable by dyadic left-step approximation using [F4]; its time-zero value is predictable on the time-zero generator. Direct integration gives Ati=λ(t∧W); left Riemann sums make it adapted, and continuous left-step approximations make it predictable by [F4]. The exponential density gives EATi=λ(∫0Tuλe−λudu+Te−λT)=1−e−λT<∞. If W≤s, the martingale increment is zero; if W>s, the residual waiting time R=W−s is exponential and, for h=t−s, E[Nt−Ns∣Fs]=1−e−λh=E[At−As∣Fs] on that event, since λ(∫0huλe−λudu+he−λh)=1−e−λh. Hence each Mi is an all-pairs martingale; ∣Mti∣≤1+λT makes it square-integrable and verifies [F1].

2.1A1F2F3givenstep 1.1∎

The two component martingales are identical, so [F3] gives [M1,M2]=[M,M]. By [F2], [M,M]=N and ⟨M,M⟩=A, hence the pair has the same cross-bracket values. For every t>0, P(Nt=1)=1−e−λt>0 and At=λ(t∧W)>0 almost surely because W>0 almost surely; neither cross-bracket process is identically zero when simultaneous jumps are allowed.

Source notes

Tian states zero cross brackets under a no-simultaneous-jump hypothesis; Andersen–Borgan–Gill–Keiding impose the same condition for multivariate counting processes. This tied-process construction shows the boundary case directly.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources