Finite-horizon, expected-time, and scale-identification impossibility statements for strict methods.

noncomputable def V7.DeterministicFiniteHorizonImpossibilityStatement : Prop

U04--U07: eps is fixed before the method; the hard transition length and objective are existential only after the finite transcript/output map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.RandomizedFiniteHorizonImpossibilityStatement : Prop

U08: a single deterministic H and hard instance is chosen after the whole seed-indexed method, never separately for each seed.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.InfiniteWorstCaseExpectedHittingTimeStatement : Prop

U09: the supremum of the actual expected queried-or-returned hitting time over normalized strict instances is infinite.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.OneDimensionalInteriorLpTransferStatement : Prop

U10: the real-line obstruction applies for every fixed interior exponent because the one-dimensional ell_p and ell_q norms are absolute value.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.ScaleIdentificationImpossibilityStatement : Prop

Source carrier for thm:impossibility; its deterministic, randomized, expectation, and all-p clauses remain separate conjuncts.

Equations

• One or more equations did not get rendered due to their size.