Adaptive Early Stopping Limits

Abstract

Adaptive early stopping lowers a concrete expected count while preserving the adaptive worst-case information bound and the fixed answer alphabet.

Theorem 1.1 (Early stopping retains the adaptive worst-case lower bound).

$$\begin{array}{r}\forall Question,X:\mathrm{Type},[\mathrm{Fintype}(X)],\\ \forall B:\mathbb{N},\\ \forall q:Question\to \left(X\to \mathrm{Fin}(B)\right),\\ \forall identifiable:\exists depth:\mathbb{N},\mathrm{ExactAtDepth}(q,depth),\\ \mathrm{clog}(B,\mathrm{card}(X))\le \mathrm{adaptiveIdentificationDepth}(q,identifiable).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.adaptive_worst_case_depth_information_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The imported adaptive protocol already permits a leaf under any remaining budget. Its logarithmic lower bound therefore applies directly for positive branching, while the totalized base-zero logarithm is zero.

Theorem 1.2 (Full transcript spaces attain the worst-case lower bound).

$$1<B⟹\mathrm{adaptiveIdentificationDepth}(\mathrm{TranscriptSpace}(B,h),\mathrm{coordinateReadout}(B,h))=h.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.adaptive_worst_case_depth_lower_bound_is_tight (✓ std3). ∎

Source. Repository-derived.

Commentary.

For more than one possible answer, coordinate questions identify all B-valued transcripts of length h. The imported cardinality equality and the lower bound force the least adaptive depth to equal h.

Lemma 1.3 (Nonunary branching is necessary for positive-depth tightness).

$$\mathrm{adaptiveIdentificationDepth}(\mathrm{TranscriptSpace}(1,1),\mathrm{coordinateReadout}(1,1))=0\wedge \mathrm{adaptiveIdentificationDepth}(\mathrm{TranscriptSpace}(1,1),\mathrm{coordinateReadout}(1,1))\ne 1.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.branching_gt_one_is_necessary_for_positive_depth_tightness (✓ std3). ∎

Source. Repository-derived.

Commentary.

At B=1 and nominal depth one, the transcript state space is a singleton. A root leaf identifies it at depth zero, so equality with depth one is false.

Theorem 1.4 (One experiment has at most B attained answers).

$$\mathrm{card}(\mathrm{singleExperimentOutputs}(q))\le B.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.single_experiment_output_count_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every adaptive query returns a value in Fin B by definition. The attained image is a subset of that fixed alphabet, so its cardinality is at most B independently of how later questions are selected.

Lemma 1.5 (The single-experiment output bound is attained).

$$\mathrm{card}(\mathrm{singleExperimentOutputs}(\mathrm{identityOn}(\mathrm{Fin}(B))))=B.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.identity_experiment_attains_output_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity experiment on Fin B realizes every output. This also covers B=0, where both the state space and attained output set are empty.

Lemma 1.6 (Empty and unary experiments have the expected output counts).

$$\mathrm{card}(\mathrm{singleExperimentOutputs}(emptyToFinZero))=0\wedge \mathrm{card}(\mathrm{singleExperimentOutputs}(unitToFinOne))=1.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.single_experiment_degenerate_audit (✓ std3). ∎

Source. Repository-derived.

Commentary.

An experiment on Empty with an empty alphabet attains no answer. A constant unary experiment on Unit attains exactly its sole answer.

Lemma 1.7 (Zero depth and constant-readout boundaries are explicit).

$$\mathrm{ExactAtDepth}(qEmpty,0)\wedge \mathrm{ExactAtDepth}(qUnit,0)\wedge \mathrm{clog}(1,1)=0\wedge \forall h,\neg \mathrm{ExactAtDepth}(\mathrm{constantZero}(2),h).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.protocol_degenerate_audit (✓ std3). ∎

Source. Repository-derived.

Commentary.

Imported named audits identify Empty and Unit at depth zero and rule out identifying Bool with a constant binary readout. Unary clog is zero.

Lemma 1.8 (Doing every experiment removes the average saving).

$$\mathrm{expectedExperimentCount}(\mathrm{pure}(M0))=2.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.all_experiments_required_has_no_average_saving (✓ std3). ∎

Source. Repository-derived.

Commentary.

The imported three-model example has a point mass on a branch that cannot stop after the first question. Its adaptive count is exactly two, matching the static count.

References

• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.adaptive_worst_case_depth_information_lower_bound
• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.adaptive_worst_case_depth_lower_bound_is_tight
• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.all_experiments_required_has_no_average_saving
• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.branching_gt_one_is_necessary_for_positive_depth_tightness
• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.identity_experiment_attains_output_bound
• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.protocol_degenerate_audit
• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.single_experiment_degenerate_audit
• Truth anchor: D5/S3/Observer/Budget/AdaptiveEarlyStoppingLimits.single_experiment_output_count_le
• Dependency: D5/S3/ConceptDynamics/ExperimentDesign/AdaptiveEarlyStopping
• Dependency: D5/S3/Observer/Budget/WorstCaseDepthInformationLowerBound