Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
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.

The logrank ordering gives a valid Fisher randomization p-value

Statement

Fix a finite randomized treatment-assignment model with allowed assignments Z and known law p, with unit set I as in Finite randomized treatment-assignment models. Fix a map γ:Z→{0,1}I assigning each allowed assignment a binary logrank group map. For each subject i, let (Ui(z),δi(z))∈[0,τ]×{0,1} be the full right-censored record under assignment z. Assume the record sharp null: for every i, the pair (Ui(z),δi(z)) is constant over all z∈Z. Fix before observing assignment or records a bounded logrank weight rule and the two-sided ordering T(z)=∣Uw(γ(z);U,δ)∣.

The inclusive assignment-tail p-value prand(z):=∑z′∈Zp(z′)1{∣Uw(γ(z′);U,δ)∣≥∣Uw(γ(z);U,δ)∣} is superuniform under the assignment law, so it is a valid finite-sample p-value for the record sharp null. If an auxiliary V is independent of the assignment and uniform on [0,1], replacing the inclusive tail by the strict-tail mass plus V times the tied-score mass gives an exactly uniform p-value. The result uses the actual assignment probabilities and asserts no validity under a weak average-effect null or under an equal-hazard null alone.

Facts & Assumptions

Given: A finite assignment law, a fixed binary group map for every allowed assignment, a fixed horizon, a predeclared weighted logrank ordering, a record sharp null, and optionally an independent uniform tie randomizer.

[F1]

Finite randomized treatment-assignment models: the experimental units and potential-outcome schedule are fixed, the assignment Z has the declared finite law p, and each unit's response under an assignment is defined for every allowed assignment.

[F2]

Fisher sharp null and predeclared test orderings: a Fisher sharp null fixes each unit's response under every allowed assignment, and the ordering score is fixed before assignment and response inspection.

[F3]

Two-group logrank and weighted logrank scores: for a fixed right-censored record and binary group map γ(z), the weighted score is the finite sum ∑jwj(Oj−Ej); the two-sided ordering uses its absolute value and includes event-time ties by the stated risk-set rule.

[F4]

Statistics and estimators: a statistic is a measurable map from the experiment's data space to its target measurable space.

[F5]

Fisher sharp-null randomization p-values are valid: for any predeclared real-valued ordering score in a finite assignment model, the inclusive weighted assignment tail is superuniform under the Fisher sharp null, and an independent uniform tie randomizer gives an exactly uniform value.

[F6]

Valid p-values: a p-value is valid for a null when its probability of being at most u is at most u for every u∈[0,1] and every law in that null.

[A1]

When the randomized-tie version is used, V is independent of the assignment and has the uniform law on [0,1].

Proof

1.1F1F2givenconstruct

Encode each record by the real number Ri(z)=Ui(z)+(τ+1)δi(z). The event-record range [0,τ] and censor-record range [τ+1,2τ+1] are disjoint, so this map is injective and Borel, with a Borel inverse on its image. Under the record sharp null, every encoded response Ri(z) is constant over all assignments. Hence the scalar schedule (Ri(z))i∈I satisfies the Fisher sharp null of [F2] within the finite assignment model [F1].

2.1F2F3F4step 1.1construct

On encoded response vectors whose coordinates lie in the image of the record encoding, decode the records and evaluate the fixed weighted logrank score using the candidate binary group map γ(z); define the score to be zero outside that image. This is a predeclared real-valued score on the finite assignment model. Its data space has the full power-set sigma-algebra, so every such map is measurable in the sense of [F4]. The absolute-score ordering includes ties and is fixed before assignment or records are inspected by [F2, F3].

3.1A1F5F6step 1.1step 2.1∎

Apply [F5] to this predeclared score and the actual finite assignment weights. Its inclusive tail is exactly the displayed prand, so for every u∈[0,1] its null probability of being at most u is at most u. Under [A1], the strict-tail mass plus V times the tied-score mass is exactly the randomized-tie p-value in [F5] and is uniform. By [F6], these bounds are precisely finite-sample p-value validity for the record sharp null. The proof uses no survival-law, censoring-independence, or Gaussian assumption; it makes no claim for a weaker null that does not fix every record.

Depends on

Used by

Dependency tree · two levels

20 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