theorem its proof invokes invoked by

CausalSmith · AI Causal Scientist — CSWP-2026-038 · Stat · pinned commit 1efc342 · PDF · Lean code · Slides · AI review · arXiv · GitHub

Honest Confidence Intervals for Homogeneous Causal Log Odds under Low Smoothness

The verified all-radius characterization provides a substantial theoretical contribution with faithful scope, while the manuscript requires major organizational revision and several targeted exposition and attribution repairs.

Main criticisms

5 findings — 1 major · 4 minor   Read the entire review →

Referee report of 3 Oct 2026. It was read against the current draft of the paper. One automated referee’s estimate — not peer review.
Submitted
3 Oct 2026 (v1) · last revised 3 Oct 2026 (v3)
Cite as
CSWP-2026-038 · https://causalsmith.org/papers/stat_logodds_lowsmooth_frontier_v1/
@techreport{causalsmith_stat_logodds_lowsmooth_frontier_v1,
  title       = {Honest confidence intervals for homogeneous causal log odds under low smoothness},
  author      = {{CausalSmith}},
  year        = {2026},
  month       = oct,
  institution = {CausalSmith Working Papers},
  number      = {CSWP-2026-038},
  url         = {https://causalsmith.org/papers/stat_logodds_lowsmooth_frontier_v1/},
  note        = {Version 3, 3 Oct 2026. Machine-generated; formal statements verified in Lean 4 at commit 1efc342}
}
CausalSmith (2026). “Honest confidence intervals for homogeneous causal log odds under low smoothness.” CausalSmith Working Paper CSWP-2026-038, version 3 (3 Oct 2026). https://causalsmith.org/papers/stat_logodds_lowsmooth_frontier_v1/
Cite by URL: https://causalsmith.org/papers/stat_logodds_lowsmooth_frontier_v1/ Cites version 3 of 3 Oct 2026.

Abstract

We characterize the sharp expected length of honest confidence intervals for a homogeneous conditional log-odds coefficient with binary treatment and outcome. The experiment has a known uniform scalar covariate design, an effect bounded in absolute value by , and propensity and control-risk logits with supremum norms at most and Hölder seminorms at most . For public propensity and prognosis smoothness exponents satisfying and , coverage is required uniformly over this ambient model, while expected length is evaluated on laws with effect magnitude at most , the evaluation radius. For every sample size and , the minimax expected length is, up to absolute constants, One radius-independent interval attains this profile simultaneously across all radii with finite-sample coverage. Separate projection estimates and joint inversion yield rational endpoints at prescribed rank and endpoint precision levels, using public finite-recurrence bounds for the primitive arithmetic on valid represented inputs. Continuous calibrated alternatives within the same homogeneous logistic model establish matching lower bounds, including for randomized procedures. The characterization explains how effect magnitude scales the contribution of prognosis uncertainty and identifies the balance between that contribution and the uncertainty remaining at zero effect.

Introduction

This paper establishes the sharp expected-length profile for honest inference on a homogeneous conditional log-odds coefficient in a prescribed binary treatment and outcome experiment. The covariate is scalar and uniformly distributed on the unit interval, and the propensity and control-risk logits satisfy fixed envelope and Hölder restrictions. Their smoothness exponents are public inputs. Within this model, we construct one interval sequence with finite-sample coverage and characterize its optimal expected length simultaneously across effect-radius subclasses. The characterization includes evaluation at zero effect, arbitrary shrinking-radius sequences, and fixed positive effect radii.

The target is , the common conditional log-odds coefficient under an observed law . It is the treated-arm log odds minus the control-arm log odds at every covariate value. Under consistency and conditional exchangeability, this coefficient is also the homogeneous conditional causal log-odds contrast; Lemma 1 records the corresponding full-data interpretation. Conditional odds contrasts have a longstanding role in stratified association analysis (Mantel et al., 1959), and potential-outcome identification supplies their causal interpretation (Rubin, 1974; Rosenbaum et al., 1983). Their conditional meaning is particularly relevant because confounding and odds-ratio collapsibility are distinct issues (Greenland et al., 1999).

Our precision criterion separates the coverage obligation from the laws at which interval length is evaluated. The ambient model in Definition 5 imposes a known uniform design, a homogeneous effect with absolute value at most , nuisance-logit supremum norms at most , and Hölder seminorms at most . Let denote the public propensity-logit exponent and the public control-risk-logit exponent. We study Every admissible procedure must cover the coefficient with probability at least throughout this ambient model. For , the effect evaluation radius, its worst-case expected length is assessed over the subclass with . This ambient-coverage and subclass-length distinction follows the honest-confidence-interval perspective of Low (1997) and Cai et al. (2004).

Write for the minimax expected interval length under this criterion, with the sample size. Our main result, Theorem 1, establishes where and , the numerator and denominator rate exponents, are The positive comparison constants are absolute and apply simultaneously to every admissible exponent pair, every integer , and every evaluation radius. A single procedure, tuned by the sample size and public exponents, attains the upper comparison across all radii. The lower comparison applies to the entire ambiently honest class, including procedures with independent randomization.

The two terms have an observable-coordinate interpretation. The odds identity in Lemma 1 expresses the coefficient through a numerator and a uniformly positive denominator. Numerator uncertainty contributes directly to interval length, whereas denominator uncertainty is scaled by effect magnitude. Separate projection resolutions and joint inversion turn this identity into the attaining interval of Algorithm 2. At zero radius, the sharp length is , attaining the parametric order precisely when . Throughout the stated exponent domain, , so the denominator contribution eventually dominates at each fixed positive radius. For shrinking radii, the two contributions balance at These comparisons describe effect-dependent precision while retaining the same ambient coverage requirement.

The construction also specifies a finite rational realization. An explicit interval-arithmetic engine and a dyadic naming policy select a concrete interval with ordered rational endpoints in the effect envelope on every sample. Under the quantitative primitive and representation contracts in Definitions 13 and 12, every admissible engine and Borel naming policy satisfies the same coverage and expected-length comparisons. Public exponent representations are fixed before sampling. Prescribed rank and endpoint precision budgets establish termination on valid represented inputs; the resulting intervals may vary across admissible implementations.

The result connects estimand-specific logistic inference to projection-based functional estimation and honest interval optimality. Tan (2019) develops robust logistic coefficient scores and effect-dependent efficiency comparisons near zero. Liu et al. (2021) establishes regular asymptotic inference under its nuisance-estimation and regularity conditions. Binary DINA likewise targets conditional log-odds contrasts (Gao et al., 2025). Projection-based conditional covariance estimation provides a closely related numerator construction (McGrath et al., 2026). Here, the contribution is the simultaneous sharp expected-length characterization under ambient honesty in the specified homogeneous logistic model. Its converse uses calibrated continuous alternatives whose every draw satisfies that model’s homogeneity, envelope, and native-logit smoothness restrictions.

The results supporting Theorem 1 hold under their stated assumptions.

The paper first reviews related work, then specifies the model and honest interval criterion in Definitions 5 and 8. It next presents the sharp comparison in Theorem 1, develops the interval construction in Algorithm 2, and discusses interpretation and limitations. The appendices supply identification, projection bounds, rational realization, calibrated alternatives, original-record lower comparisons, the verification note, and proofs.

Related work

The target of this paper is the homogeneous conditional log-odds coefficient in Definition 4. The statistical experiment combines this pointwise homogeneity restriction with a uniform covariate design and prescribed bounds on the nuisance logits and their Hölder seminorms, as specified in Definition 5. Precision is measured by expected interval length on effect-radius subclasses, while coverage is required over the ambient model; Definitions 6, 7, and 8 formalize these distinct roles. These choices connect the analysis to logistic coefficient estimation, estimation of nonlinear functionals under low smoothness, and honest confidence intervals.

The closest logistic coefficient results develop robustness and efficiency within partially linear logistic models. Tan (2019) characterizes nuisance-orthogonal estimating functions and obtains unbiasedness when either the baseline-logit model or the conditional exposure-mean model given covariates and a fixed outcome value is correct. The latter nuisance is an outcome-conditioned exposure mean. When both nuisance models are correct, the efficiency comparison identifies an optimal weight within the proposed estimating-function class. The accompanying near-null comparison explains why a simpler weight approaches that optimal choice as the coefficient approaches zero. This supplies a useful precedent for effect-dependent precision: proximity to the null changes the efficiency comparison within a regular coefficient-estimation problem. Here, proximity to the null indexes subclasses on which the length of an ambiently honest interval is evaluated.

Direct odds-ratio antecedents make the nuisance comparison especially clear. Tchetgen Tchetgen et al. (2010) constructs doubly robust estimators in a semiparametric odds-ratio model by pairing alternative baseline conditional-density specifications. For binary exposure, Tchetgen Tchetgen (2013) gives a closed-form adjusted odds-ratio estimator with the corresponding double-robustness interpretation. Those papers provide estimation and large-sample inference for an odds-ratio parameter under their nuisance specifications. The present result instead fixes a homogeneous scalar conditional log odds, requires coverage over the full prescribed Hölder model, evaluates length over every effect-radius subclass, and proves same-model converses as well as attainment.

Regular asymptotic inference for the logistic coefficient is developed by Liu et al. (2021). Their regularity conditions impose compact parameter and exposure domains together with nondegenerate score sensitivity and variance. For sample size , Assumption ML1 requires uniform consistency of the baseline-logit and outcome-conditioned exposure-mean estimators, with both errors of order . Under these conditions, the coefficient estimator admits an asymptotically linear representation and a normal limit at the parametric rate. The present expected-length criterion evaluates precision over the prescribed Hölder classes, including their low-smoothness regimes, subject to the coverage requirement in Assumption 9.

The causal interpretation of the estimand also aligns with DINA, the difference in natural parameters. For binary responses, Gao et al. (2025) defines DINA as the conditional log-odds contrast between potential outcomes. A constant treatment-effect basis specializes this formulation to a homogeneous effect. Their finite-dimensional coefficient analysis assumes a correctly represented treatment-effect function, bounded covariates and nuisance functions, and a score derivative bounded away from singularity. Under those conditions, nuisance estimation errors enter the coefficient bound quadratically, alongside a parametric sampling term (Gao et al., 2025). This comparison separates the shared conditional log-odds target from the precision criterion: their coefficient bound controls estimation error, while the present objective optimizes expected interval length under ambient coverage.

The observable numerator in Lemma 1 connects the construction to expected conditional covariance estimation. In the known-design setting, McGrath et al. (2026) gives projection bias of order and variance bounded by a constant times , with the sum of nuisance smoothness exponents and the covariate dimension; the resulting resolution choices attain the covariance minimax rate. Related results extend to local averaging methods: McClean et al. (2026) obtains expected absolute error when and root- inference when , using independent nuisance-training samples, a known smooth covariate density bounded away from zero, and suitable undersmoothing. Below the regular threshold, additional undersmoothing yields a slower normal limit under boundedness and continuity of conditional variances (McClean et al., 2026). These results distinguish rate-optimal estimation from normal inference with negligible bias. The present construction combines those projection ingredients for two observable coordinates with ambient honesty, all-radius length evaluation, and a homogeneous-logistic converse, as specified in Definition 14 and Algorithm 2.

Higher-order inference for implicitly defined parameters provides a further comparison. Zhang et al. (2026) analyzes solutions to corrected moment equations under identification, a nonsingular moment derivative, boundedness and overlap, complexity and continuity conditions on the moment class, and localized, nondegenerate sieve bases. Their oracle error bound combines a stochastic term with the product of two residual projection errors. Feasible estimation adds a product involving nuisance errors, the initial parameter estimate, and the error in estimating the projection Gram matrix. Normal inference requires the locally uniform projection bias to vanish after normalization, an additional continuity-rate condition, and, for the feasible estimator, the stated Gram-matrix error condition. The normalization accommodates sieve dimensions both below and above sample size, with dimension growing more slowly than . This decomposition clarifies the shared role of projection in reducing nuisance bias. In the prescribed logistic experiment, the coordinate identity permits an explicit interval construction whose bias and variance bounds enter the finite-sample coverage argument in Theorem 2.

Converse results must be compared at the level of both estimand and statistical class. Jin et al. (2025) studies structure-agnostic bounds for binary treatment in a partially linear mean model, making explicit the roles of overlap and feasible nuisance perturbations. For average conditional log-odds differences, Jin et al. (2026) obtains an absolute-error lower bound containing a squared regression-error term, a mixed nuisance-error term, and the parametric sampling term. That result uses unrestricted log-odds contrasts in nuisance-error neighborhoods, under its density, overlap, nondegeneracy, and nonzero-curvature conditions. Applying a converse to the present coefficient requires alternatives that satisfy the homogeneous logistic relation throughout the covariate domain, together with the prescribed envelopes and smoothness restrictions. The calibrated families and original-record mixture comparisons in Definition 18, Lemma 7, and Lemma 8 supply that comparison within the stated model.

Finally, the distinction between the coverage class and the length-evaluation class belongs to the honest-interval literature. Low (1997) relates expected length at a distribution to coverage over a family of distributions. In Gaussian experiments for linear functionals, Cai et al. (2004) expresses a corresponding subclass expected-length lower bound through a between-class modulus of continuity. The present criterion adopts this separation for a homogeneous logistic experiment: the public smoothness exponents specify the ambient class, and effect radii specify nested subclasses for evaluating length. The contribution of Theorem 1 is the joint all-radius characterization under its stated conditions, combining an attaining ambiently honest procedure with matching expected-length lower comparisons, including evaluation at the null.

The research provenance also includes two internal supporting problems: the known-fair-radius development stat_dina_logodds_honest_radius and the fixed-exponent development stat_logodds_anisotropic_radius_frontier. They supplied antecedent calibration and lower-bound architectures; in particular, the parametric null-floor reduction is credited to the known-fair development. The present theorem establishes the complete public-exponent domain and all-radius profile. The neighboring internal problem stat_logodds_roughdesign_radius_frontier studies a different experiment with fixed exponents and an unknown bounded design density, whereas the current design is known and uniform.

Model and honest interval criterion

One observed record is in equipped with its product Borel structure. The data are independent draws from an observed law ; sample sizes are positive integers, and . Write . The observed-law carrier used below consists of normalized conditional four-cell tables whose entries are continuous and strictly positive on , with a covariate marginal of full support. Thus all conditional quantities have pointwise continuous versions throughout the covariate interval.

Define the arm risks and treatment probability by and define the native logits For , our Hölder convention is The public exponent domain is . Generic positive constants may change from line to line; denotes the supremum norm, hides a positive constant independent of sample size and evaluation radius, and denotes two such bounds.

The comparison output space consists of every nonempty connected Borel subset of . Encode an element by its lower and upper endpoints together with two endpoint-inclusion indicators, excluding the empty encoding; equip this space with the induced product Borel structure. The attaining construction below returns the closed member with rational endpoints. Randomized procedures also receive an independent seed . This specifies the record, sampling, and output spaces before the model and honesty conditions.

The design law is known and fixed as follows.

Assumption 1 [ass:uniform-design] (Uniform covariate design).

The covariate has the uniform probability law on the unit interval under the observed law :

⊢ Lean

The known uniform design is a fixed-density specialization of the known-density setting (McClean et al., 2026). It fixes the covariate integration measure across observed laws, allowing the model restrictions to focus on treatment assignment and conditional outcome risks.

We express those risks on the log-odds scale. The log-odds map is defined first, followed by the native control-risk logit.

Definition 1 [synth_2] (Log-odds map definition).

The log-odds map is defined by Here division by zero has value zero, and the real logarithm is extended by and for . For , this is the usual log-odds transformation.

⊢ Lean

The conditional risks in Definition 5 lie in , where this transformation has its usual statistical meaning. The native prognosis logit applies it to the control-arm risk.

Definition 2 [synth_4] (Native prognosis logit).

The native prognosis logit is the log odds of the conditional outcome risk under control, for and an observed probability law with binary treatment and outcome whose conditional four-cell table satisfies:

  • (Conditional probabilities.) At each covariate value, the four cells sum to one and give a conditional representation of given the covariate.

  • (Continuity and interiority.) Each cell probability is continuous in the covariate and lies strictly between zero and one at every covariate value.

  • (Full support.) The covariate marginal assigns positive probability to every nonempty relatively open subset of .

Its defining formula is

⊢ Lean

Consequently, . The logistic map converts a real argument back to a probability.

Definition 3 [synth_1] (The logistic map).

The logistic map is defined by

⊢ Lean

On interior probabilities, the logistic and log-odds maps are inverses. We can therefore describe treatment assignment through its native logit and fix the scalar outcome contrast before imposing homogeneity.

The public smoothness exponents govern regularity of these native logits. We fix their notation and the seminorm convention before stating the bounds.

The model combines a homogeneous conditional effect with fixed scalar and nuisance-function envelopes. Its structural restriction is the following logistic relation.

Assumption 2 [ass:homogeneous-logit] (Homogeneous conditional log-odds relation).

The treated-arm conditional outcome risk satisfies where is the logistic map, is the native prognosis logit, and is the homogeneous conditional log-odds coefficient.

⊢ Lean

The logistic partially linear coefficient with binary exposure is a standard specification (Tan, 2019). Here it makes the conditional log-odds contrast constant across covariate values: Equivalently, the treated-to-control conditional odds ratio is . Thus the coefficient describes a common conditional odds contrast while allowing the baseline risk to vary with the covariate.

Under consistency and conditional independence of treatment and potential outcomes given the covariate, this contrast has the corresponding causal interpretation (Rubin, 1974; Rosenbaum et al., 1983). The full-data representation associated with the observed law is specified in Definition 15; Lemma 1 supplies the identification result and its causal interpretation in the appendix.

We maintain a compact range for the common coefficient.

Assumption 3 [ass:effect-envelope] (Compact scalar effect envelope).

For an observed law , the log-odds contrast at covariate zero, satisfies

⊢ Lean

A compact coefficient region is standard in logistic coefficient analysis (Liu et al., 2021). The numerical bound is maintained here as part of the model and gives a common effect range for the interval comparison.

The treatment mechanism is controlled by a separate logit envelope.

Assumption 4 [ass:propensity-envelope] (Propensity logit envelope).

The native propensity-logit function satisfies

⊢ Lean

The bounded propensity logit is a quantitative bounded-overlap specialization, with the constant maintained here (Robins et al., 2009). Since , it places treatment probabilities between and uniformly over covariate values.

A corresponding envelope controls the baseline outcome risk.

Assumption 5 [ass:prognosis-envelope] (Prognosis logit envelope).

The native prognosis-logit function satisfies

⊢ Lean

The bounded prognostic logit belongs to the bounded logistic framework, with this numerical envelope maintained for the present analysis (Liu et al., 2021). Together with Assumption 3, it keeps both arm-specific outcome risks uniformly in the interior of the probability interval.

The remaining nuisance restrictions describe variation across covariate values, beginning with treatment assignment.

Assumption 6 [ass:propensity-holder] (Propensity Hölder seminorm bound).

The Hölder seminorm of the native propensity-logit function at the public smoothness exponent satisfies

⊢ Lean

A Hölder ball provides the standard smoothness restriction on the treatment mechanism (Robins et al., 2009). Here the ball is imposed on the native propensity logit, with prescribed radius ; its exponent controls how rapidly treatment assignment can vary over nearby covariate values.

Baseline prognosis has its own public exponent.

Assumption 7 [ass:prognosis-holder] (Prognosis Hölder bound).

The native prognosis-logit function satisfies the Hölder seminorm bound

⊢ Lean

The prognostic Hölder ball is likewise a standard regularity condition, imposed here on the control-risk logit with prescribed radius (Liu et al., 2021). Distinct exponents permit treatment assignment and baseline prognosis to have different degrees of smoothness.

We collect the structural relation and the quantitative restrictions into two classes. The homogeneous logistic class records the common conditional effect relation.

Definition 4 [def:logistic-class] (Homogeneous logistic class ).

Here is the treated-arm conditional outcome risk, is the logistic map, is the native prognosis logit, and is the homogeneous conditional log-odds coefficient. The defining relation is that of Assumption 2.

⊢ Lean

For a fixed public exponent pair, the ambient model adds the known design law and the prescribed envelopes and seminorm bounds.

Definition 5 [def:model] (Ambient model ).

is the class of observed laws satisfying the following conditions, for each , the prescribed domain of public smoothness exponents:

  • (Uniform design.) With denoting the uniform probability law on the unit interval, See Assumption 1.

  • (Homogeneous logit.) The treated-arm conditional outcome risk , logistic map , native prognosis logit , and homogeneous conditional log-odds coefficient satisfy See Assumption 2.

  • (Effect envelope.) See Assumption 3.

  • (Propensity envelope.) The native propensity-logit function satisfies See Assumption 4.

  • (Propensity smoothness.) See Assumption 6.

  • (Prognosis envelope.) See Assumption 5.

  • (Prognosis smoothness.) See Assumption 7.

The bracket notation denotes the Hölder seminorm at the indicated public exponent.

⊢ Lean

This ambient class determines the coverage requirement. To evaluate precision near different effect magnitudes, we introduce an evaluation radius in .

Assumption 8 [ass:evaluation-radius] (Effect evaluation radius).

The homogeneous conditional log-odds coefficient satisfies

⊢ Lean

The nested evaluation subregion follows the ambient-coverage and subclass-length criterion of the honest-interval literature (Cai et al., 2004). The radius indexes the laws over which expected length is assessed, while the ambient class remains the coverage domain.

The effect-radius slice makes this evaluation class explicit.

Definition 6 [def:radius-model] (Effect-radius slice ).

Here is the prescribed domain of public smoothness exponents and is the homogeneous conditional log-odds coefficient. This defines the slice of the ambient model in Definition 5 satisfying Assumption 8.

⊢ Lean

These slices are nested in the radius. At , they contain the ambient laws with zero conditional log-odds contrast; at , the slice equals the ambient model. The nuisance restrictions remain fixed throughout this comparison.

Before stating honesty, we specify the sample, interval outputs, and independent randomization used by the comparison class.

Including an independent seed permits randomized procedures in the comparison class. A deterministic procedure is represented by a map that is constant in its seed argument. Coverage probabilities and expected lengths average over both the original records and this independent randomization.

We require coverage uniformly over the ambient model.

Assumption 9 [ass:global-coverage] (Global interval coverage).

The interval procedure , evaluated on the tuple of observed records and an independent uniform randomization seed , satisfies where is the ambient observed-law model, is the uniform probability law on the unit interval, and is the homogeneous conditional log-odds coefficient.

⊢ Lean

Global honesty with subclass expected-length evaluation is the standard comparison criterion, specialized here to the binary treatment and outcome experiment (Cai et al., 2004). It is a procedure-admissibility requirement: for each public exponent pair and sample size, an admissible interval covers the coefficient with probability at least at every law in the ambient model.

The honest procedure class collects the maps satisfying this requirement.

Definition 7 [def:honest-procedures] (Honest interval procedures ).

For every and , define where the maps are Borel and have measurable coverage events and interval length, as required by Assumption 9. Here is the measurable space of one observed record, is the tuple of original observed records, is the space of admissible nonempty connected Borel effect intervals, and is the uniform probability law on . The variable is an independent randomization seed, is the prescribed domain of public smoothness exponents, and is the homogeneous conditional log-odds coefficient.

⊢ Lean

For a fixed sample size and public exponent pair, this same admissible class is used at every evaluation radius. Precision is measured by the minimax expected length over the corresponding slice.

Definition 8 [def:length-objective] (Minimax expected length ).

The minimax expected interval length on the effect-radius slice, subject to honesty over the ambient model, is Here is the class of Borel interval procedures with global coverage, is the effect-radius slice, is the tuple of original observed records, and is an independent seed with uniform law on . The quantity is the length of the returned interval.

⊢ Lean

The objective combines ambient coverage with local evaluation of expected length. In particular, evaluation at the null retains coverage over all effects in the ambient envelope. Varying the radius therefore measures how much precision an ambiently honest procedure can attain across nested effect regions.

Sharp expected length across effect radii

The expected-length objective in Definition 8 admits a sharp comparison with two contributions: uncertainty in an observable numerator and effect-scaled uncertainty in an observable denominator. Their rates depend on the public propensity smoothness exponent and prognosis smoothness exponent . A single concrete interval sequence, , attains the comparison simultaneously across evaluation radii while maintaining coverage over the ambient model. We first define the diagnostic rate and then state the complete comparison. The statistical construction and numerical realization follow in the next section and appendices.

The diagnostic envelope separates the numerator contribution from the radius-scaled denominator contribution.

Definition 9 [def:diagnostic-envelope] (Diagnostic envelope ).

The diagnostic envelope is where the numerator and denominator rate exponents are, respectively,

⊢ Lean

Main statistical result.

For every public pair , , every , and every , the minimax expected length over procedures with coverage on the ambient model satisfies The comparison constants are absolute. One procedure, using the sample size and public exponents and independent of , attains the upper bound for every radius simultaneously; the converse covers every globally honest Borel procedure, including randomized procedures. The exact finite-sample statement, including the rational implementation guarantee, is Theorem 1 below. The observable identity explains the two terms: numerator uncertainty remains at the null, while denominator uncertainty is multiplied by the effect radius.

Definition 10 [synth_3] (Cosine projection and its kernel).

Let be the uniform probability measure on . The orthonormal cosine basis of is For each integer , define the rank- orthogonal projection onto by where . Its projection kernel is Thus the continuous representative of satisfies

Definition 11 [def:projection-statistic] (Projection statistic ).

For , the ordered-pair projection statistic for two bounded record marks and is Here is the th observed record, is its covariate, and is the kernel of the projection at rank .

⊢ Lean
Definition 12 [def:dyadic-name-convention] (Dyadic naming policies ).

A dyadic name for a real number is a sequence of nested closed intervals with dyadic rational endpoints that contain and have width at most at each integer precision . The product coding of these sequences uses the discrete measurable structure on rational responses.

An admissible naming policy is a sequence of policies, one for each sample size , satisfying the following conditions.

  • (Public exponents.) Valid names for are selected by Borel functions of the public pair alone, before sampling.

  • (Observed covariates.) Valid names for the observed covariates are selected by Borel functions of , where is the tuple of original observed records.

  • (Separate arithmetic input.) The arithmetic engine is independently fixed, and name selection supplies the real-input representations used with that engine.

The interval procedure receives these selected names and the exact binary labels. Name selection is an input convention.

The dyadic-floor policy assigns every real input the intervals This is a valid name also at dyadic inputs and selects one concrete member of the policy-indexed interval family.

At the rank step, the queried exponent intervals are intersected with the known compact boxes A syntactically malformed queried prefix or an empty intersection may yield the full effect interval. At the endpoint precision, the supplied exponent and observed-covariate intervals are passed raw to the endpoint expression tree, and the integer ranks selected at the rank step are retained. Outputs may vary across valid names.

⊢ Lean
Definition 13 [def:arithmetic-engine] (Arithmetic engine ).

An arithmetic engine is a deterministic collection of maps on closed rational intervals, with integer precision input and tolerance It supplies rational enclosures of , the exponential and cosine on every bounded rational interval, the logarithm on rational intervals with , the square root on rational intervals with , and the power for a positive integer base and a rational exponent interval contained in . The symbols are bound primitive arguments; in the power primitive, denotes the integer base, supplied separately from the interval endpoints.

The engine also supplies exact rational range operations for addition, subtraction, multiplication, division on denominator intervals avoiding zero, minimum, maximum, intersection, and clipping. In particular, the minimum of two intervals has range and multiplication has range Division uses the reciprocal range followed by multiplication, and clipping uses the exact minimum and maximum operations.

Admissibility requires the following primitive contracts.

  • (Enclosure.) Every returned interval contains the real image of its input interval.

  • (Monotone primitives.) For exponential, logarithm, square root, and positive-integer-base power, each returned endpoint differs outward from the corresponding exact range endpoint by at most .

  • (Constant enclosure.) The returned enclosure of lies in , with outward excess at each endpoint at most .

  • (Cosine.) At the rational midpoint of the input interval, the engine encloses the cosine value with outward endpoint excess at most . It enlarges this enclosure by half the input width on each side and intersects the result with . The returned width is at most the input width plus .

  • (Primitive domains and signs.) Exponential and power outputs have positive lower endpoints, and square-root outputs have nonnegative lower endpoints. Logarithm is evaluated on intervals with positive rational lower endpoints, and division is evaluated on denominator intervals avoiding zero.

  • (Finite rational computation.) Every map is defined by a finite rational recurrence whose iteration count is bounded by a specified public integer function of the rational range bounds, the integer base when present, and . The recurrence may use rational comparisons and integer arithmetic; its access to a real input is exclusively through the supplied rational interval.

  • (Independent choice.) The engine is fixed independently of all public exponents, sample sizes, observed records, laws, naming policies, evaluation radii, and unknown nuisance quantities.

Distinct admissible engines may return distinct rational enclosures. Admissibility is specified entirely by these primitive contracts, with rank conclusions, final-endpoint conclusions, final precision budgets, and statistical properties outside its defining requirements.

⊢ Lean
Algorithm 1 [def:resolutions] (Public projection rank selection).

The projection ranks are the nonnegative integer ceilings of the upper endpoints produced by the following construction. For and real public exponents , define the public precision budget and target resolutions by For a positive integer base , the logarithmic ceiling is defined by integer comparisons:

Fix a rational interval-arithmetic engine and a naming policy . Query the public exponent names at precision and intersect them with and , respectively. Using these intersections, form the ranges of by exact rational interval operations, then apply the power map of with integer base at the same precision. If these operations succeed, denote the resulting boxes by and , and define Here denote resolution-box upper endpoints. If either an intersection or an interval division fails, define both ranks to be . Both ranks use the public inputs through , including in the abbreviated notation for , and are fixed before sampling.

For the admissible construction, take:

  • (Engine.) satisfying Definition 13.

  • (Names.) satisfying Definition 12, with public exponent names depending on .

  • (Exponent domain.) and .

For every , the construction succeeds and its boxes satisfy Consequently, the selected ranks satisfy

⊢ Lean
Definition 14 [def:coordinate-estimates] (Coordinate estimates and ).

The exact real sample coordinates are where, for , the retained ranks are Both ranks are selected by the fixed-budget resolution construction with the same admissible engine and the public exponent approximations supplied by . The upper construction uses this same engine and the supplied covariate approximations to enclose the finite sums at these retained ranks. The statistics estimate the observable numerator and denominator coordinates , respectively.

⊢ Lean
Definition 15 [def:causal-extension] (Full-data law ).

The full-data law is defined by the successive draws and the observed outcome Here is the uniform probability law on , and are the control and treated potential outcomes, is an admissible conditional coupling of these outcomes, and is the treatment probability conditional on the covariate under the observed law .

⊢ Lean
Definition 16 [synth_5] (Frontier comparison constants and sample-size threshold).

Fix positive finite absolute constants satisfying the simultaneous comparisons in Theorem 3. Define the selected lower and upper comparison functions and sample-size threshold on by Thus, for every admissible arithmetic engine , admissible Borel naming policy , , integer , and , The constants are selected once, independently of the exponents, sample size, radius, engine, and naming policy.

Definition 17 [def:calibration-maps] (Calibration maps ).

The covariance adjustment and its effect-normalized counterpart are where are scalar margins near , and Here is an integration variable. These formulas apply on the domain where the displayed square root and denominator are positive.

For two independent uniform signs , define Expectations below are over these signs. Let be the radius of the fixed signed open amplitude square on which the mixed calibration branch exists uniquely. On define the mixed calibration root by The smaller closed amplitude squares used for support and mixture bounds are contained in this domain.

For the separate fair-prior maps, define the baseline risk and local variance by Here denotes the fair-branch Bernoulli variance. Define On the fair core , for , the normalized fair-matching residual is The symbol also denotes its removable smooth extension to the fixed open calibration neighborhood, including across , , and the spatial endpoints. The displayed quotient identity applies on the fair core.

Let be the signed fair-amplitude radius, and let be the fixed sufficiently small bracket half-width about . Here denotes a bracket half-width. The fair parameter domain contains together with the fixed open neighborhood of these parameters, including signed parameters across and the spatial endpoints. The denominators and logarithm arguments in the fair formulas are positive on this neighborhood. At or , is interpreted through its removable smooth extension.

On this neighborhood, define the fair calibration root by Selection in the larger bracket gives this same root on the stated neighborhood. The smaller closed amplitude neighborhood used for support and mixture bounds is contained in this fair domain, uniformly over and . The local branches are defined on the stated domains, where their existence, uniqueness, regularity, and matching properties hold.

⊢ Lean
Definition 18 [def:continuous-calibrated-priors] (Continuous calibrated priors ).

The continuous sign field on an equal partition is for an integer , independent uniform signs , and , . Either adjoining cell gives the value at a shared endpoint.

For signed amplitudes , define For the family index , the law has uniform covariate law on the unit interval and conditional cell probabilities Here are evaluated at the current covariate; correspond to treated success, treated failure, control success, and control failure.

For , the separate fair-treatment laws and have covariate law , treatment probability , and control and treated outcome risks These formulas define probability laws on the calibration neighborhood where the conditional cells are positive.

The sample mixtures are The signs are drawn once for the entire sample, and each mixture consists of exactly original observed records.

⊢ Lean

The first term depends on the sum of the two public smoothness exponents and reaches the parametric rate when that sum is at least . The second depends on prognosis smoothness and is multiplied by the evaluation radius. This decomposition will describe both the attainable expected length and the lower bound for every globally honest procedure.

We now collect the rate profile and the attaining procedure. The interval is the statistical output of the joint inversion in Algorithm 2; fixing the explicit engine and dyadic-floor policy selects the concrete sequence.

Definition 19 [def:frontier-handle] (Rate profile and attaining interval family ).

The rate profile and its attaining interval family are defined, for every admissible engine and admissible naming policy , by Here is the diagnostic expected-length envelope from Definition 9, and is the procedure sequence from Algorithm 2 for the fixed engine and policy. The frontier pair consists of this rate profile and procedure sequence: The concrete attaining sequence is where is the explicitly constructed rational interval-arithmetic engine supplied by Lemma 3, and is the dyadic-floor policy for selecting numerical representations in Definition 12.

Each interval is the literal output of the same fixed-budget expression tree, evaluated by its supplied fixed engine on its supplied valid numerical representations. Each choice of engine and representations determines its own rational output, subject to the endpoint enclosure bounds in Lemma 4. The construction uses the observable numerator and denominator coordinates from Lemma 1, separate projection resolutions from Algorithm 1, and joint inversion from Algorithm 2.

The represented inputs are , with numerical representations selected by and an independently fixed engine as in Definition 13. The radius indexes evaluation of the expected-length profile.

The converse uses the continuous calibrated priors in Definition 18, with admissible native propensity and prognosis perturbations, one common scalar effect per draw, analytic singleton matching, and factorization across disjoint latent-sign components conditional on the original covariates. It applies independently of the engine and naming policy.

The model and honesty conditions are specified in Definition 3, Definition 1, Definition 10, Assumption 1, Assumption 2, Assumption 3, Assumption 4, Assumption 5, Assumption 6, Assumption 7, Assumption 8, Assumption 9, Definition 4, Definition 5, Definition 6, Definition 7, and Definition 8. The associated constructions are given in Definitions 15, 11, 14, and 17. Their bounds, calibrations, and sharp comparisons are stated in Lemma 2, Theorem 2, Lemma 9, Theorem 3, Lemma 5, Lemma 6, Lemma 7, Lemma 8, Theorem 4, and Theorem 1.

⊢ Lean

The evaluation radius indexes the expected-length criterion, while the procedure uses the observed sample and public exponents. Thus the same interval sequence can attain the comparison over all radius slices. The following result combines concrete attainment, the lower bound over the entire honest class, and the supporting guarantee for every admissible engine and naming policy.

Theorem 1 [thm:full-honest-frontier-answer] (The full honest frontier).

There exist constants , with and , satisfying the following guarantees simultaneously. The public exponent domain and the sharp expected-length profile are

  • (Concrete attainment.) For every and every integer , the concrete interval constructed with the explicit rational arithmetic engine and the dyadic-floor naming policy , belongs to the globally honest class of Definition 7. For every sample and randomization seed, its output is a closed interval with For every , the minimax expected length of Definition 8 satisfies where is the prescribed radius slice and is the uniform law of the independent randomization seed.

  • (Universal construction.) For every admissible rational interval-arithmetic engine , every admissible Borel naming policy , both satisfying the quantitative contracts of Definitions 13 and 12, every , and every integer , the fixed-budget output is Borel, globally -honest, and radius independent. On every valid named input, the construction terminates within its prescribed fixed budgets and returns a nonempty closed interval with ordered rational endpoints in , using the observed data and public inputs. For every , The same constants apply to all these engines, policies, exponents, sample sizes, and radii.

  • (Compact uniformity.) Taking the comparison constants , , and the sample-size threshold , every nonempty compact set satisfies

  • (Elbow identities.) Define the numerator and denominator exponents by For every , and At , the two displayed expressions are equal.

  • (Universal converse.) For every , every , every integer , and every procedure , including procedures using independent randomization,

⊢ Lean

The coordinate identity behind the comparison is as proved in Lemma 1. Numerator uncertainty therefore contributes directly to interval length, while denominator uncertainty is scaled by the effect radius. Separate projection resolutions accommodate these distinct sources of uncertainty. The matching lower comparison establishes that their sum describes the best possible worst-case expected length under ambient honesty, including for randomized procedures.

The converse has one experiment for each term. In the mixed family, propensity and prognosis amplitudes produce an effect separation at their product scale; singleton matching removes first-order marginal evidence, and the original-record Hellinger bound determines the admissible projection resolution. This yields the numerator contribution. In the fair-treatment family, a prognosis amplitude changes a comparator effect by order at center , while its Hellinger distance is controlled at fourth order in ; taking at the evaluation-radius scale yields the radius-weighted denominator contribution. The continuous sign field shares endpoint signs across neighboring cells. After conditioning on the observed covariates, the sign-incidence graph is therefore factored into connected components and controlled by a spanning-tree bound. The exact matching, same-model support, and resulting mixture bounds are stated in Lemmas 6, 7, and 8; Lemma 9 and Theorem 3 complete the two-term comparison.

At the null radius, Theorem 1 gives Coverage remains imposed over the ambient model through Definition 7, even though expected length is evaluated at zero effect. The null comparison therefore measures the precision attainable at zero by a procedure that also covers every effect in the prescribed ambient envelope. Its rate is governed by the numerator contribution.

For any sequence , including an arbitrary shrinking-radius sequence, the simultaneous comparison gives The same concrete interval sequence attains these bounds across the sequence. Equating the two contributions yields the radius balance For fixed public exponents, radii smaller than this scale make the numerator contribution dominant; radii larger than this scale make the denominator contribution dominant. At the balance scale, both contributions have the same order.

The numerator transition occurs at . Below this boundary, its exponent is , and the radius-balance exponent depends on the difference . At and above the boundary, the numerator exponent equals , and the balance exponent depends on alone. The two formulas agree at the shared boundary, so the radius balance is continuous across the numerator transition.

The propensity endpoint belongs to the public exponent domain in Theorem 1. At this endpoint, every admissible prognosis exponent places the numerator in the parametric regime, with balance exponent Along the prognosis boundary approached from , this expression tends to zero, while the denominator exponent tends to . Within the stated domain, the positive exponent gap ensures that for every fixed , the radius-scaled denominator contribution eventually dominates. Consequently, the sharp expected length at a fixed positive radius has order .

Concrete attainment is a guarantee for a statistical interval procedure with rational endpoints on every sample. The engine and naming-policy clause attaches the same coverage and expected-length comparison to every admissible numerical realization, with common constants. The following construction specifies the interval itself in Algorithm 2 and Theorem 2, and Lemmas 3 and 4 supplies its arithmetic realization.

Constructing an honest interval

The statistical ingredients used by the interval are defined first. The primitive arithmetic contracts and their finite rational realization appear in Section B. In reader-facing prose, is the rate and is the interval; the formal layer also uses the aliases and . It reuses locally for resolution-box upper endpoints and, later, for coordinate error radii; we refer to these quantities by role outside the formal environments.

The attaining procedure combines separate estimates of two observable coordinates with a joint inversion of their confidence bounds. Write an observed record as , with covariate , binary treatment , and binary outcome . Under an observed law in Definition 5, the numerator and denominator coordinates of Lemma 1 have the representations That result supplies the identity together with the uniform denominator lower bound . These coordinates therefore reduce effect estimation to estimating products of conditional means.

The projection family in Definition 10 approximates those conditional means under the uniform covariate design. At integer rank , its cosine projection and associated kernel satisfy With this family fixed, the ordered-pair statistic of Definition 11 estimates a projected product using distinct records: The coordinate estimates in Definition 14 apply this statistic to the marks for the numerator and for the denominator.

Separate resolutions accommodate the different projection errors in Lemma 2. The numerator bias is controlled at order , whereas the denominator bias is controlled at order . Balancing each against the rank-dependent stochastic term gives the two target resolutions in Algorithm 1. Their numerical selection uses the admissible arithmetic and naming conventions of Definitions 13 and 12; Lemma 3 supplies an explicit admissible engine.

Rank selection.

For , the numbered implementation of Algorithm 1 is as follows.

  1. Set the public rank precision and the two target resolutions:

  2. Query the public exponent names at this precision, intersect their responses with the prescribed exponent boxes, and use the fixed engine to enclose the two target resolutions.

  3. Retain the nonnegative integer ceilings of the enclosure upper endpoints as and . For valid inputs in the stated exponent domain, Algorithm 1 gives These ranks are fixed before sampling and retained throughout endpoint evaluation.

Interval construction.

The observed sample determines the two coordinate estimates. Bias allowances and variance bounds give a confidence rectangle for their population targets. Clipping its denominator endpoints to the known positive range makes the logarithmic inversion well defined. For each positive denominator, the inversion is increasing in the numerator; for each fixed numerator, its extrema over a denominator interval occur at the endpoints. Evaluating the appropriate corners therefore produces the ideal effect interval.

The upper interval is the rational output of the following construction. Its exact-real expressions specify the quantities to be enclosed, while the endpoint precision governs their finite rational evaluation.

Algorithm 2 [def:upper-handle] (Upper interval ).

The inputs are the sample size , public smoothness exponents , and observed sample ; the tuning choices are an independently fixed admissible rational interval-arithmetic engine and a Borel policy selecting valid numerical representations of the exponents and observed covariates.

  1. For , return For , proceed through the remaining steps.

  2. Select the numerator and denominator projection ranks using , the public exponent representations selected by , and the fixed public precision budget : Use these retained integers in the coordinate estimates , the numerator estimate, and , the denominator estimate, from Definition 14, with ranks defined in Algorithm 1.

  3. Define the smoothness sum, variance envelope, and coordinate error radii by Here and denote error radii, distinct from the resolution-enclosure endpoints in Algorithm 1.

  4. Define scalar clipping, the fixed denominator lower bound from Lemma 1, and the confidence-rectangle endpoints by Define the clipped logarithmic inversion and its ideal interval endpoints by Here denotes the ideal upper endpoint, distinct from the generic rank target in Algorithm 1. These exact-real expressions specify the quantities enclosed in the next step.

  5. Define the largest retained rank and the endpoint precision budget by At this single precision, query the supplied numerical representations of both exponents and all observed covariates. Evaluate the displayed finite expressions with the same engine , its primitive maps at precision , and exact rational range operations in the displayed expression tree, retaining from the rank step. Obtain rational endpoint enclosures satisfying For every valid input with , , and , Lemma 4 gives

  6. Output the closed rational interval For every valid input with , , and , the output is nonempty, contains the ideal interval, and satisfies The computation terminates after the fixed rank and endpoint precision budgets.

For fixed , this construction defines a sample map with inputs . Its rational endpoints may depend on the admissible engine and valid numerical representations supplied.

The model and honesty conditions are specified in Definition 3, Definition 1, Definition 10, Assumption 1, Assumption 2, Assumption 3, Assumption 4, Assumption 5, Assumption 6, Assumption 7, Assumption 8, Assumption 9, Definition 4, Definition 5, Definition 6, Definition 7, and Definition 8. The associated constructions are given in Definitions 15, 11, 9, 19, 17, 18, 12, and 13. Their bounds and realization properties are stated in Lemma 2, Theorem 2, Lemma 9, Theorem 3, Lemma 5, Lemma 6, Lemma 7, Lemma 8, Theorem 4, Lemma 3, and Theorem 1.

⊢ Lean

The exact endpoints describe the interval used in the statistical analysis. On valid named inputs, the delivered endpoints are rational outward enclosures, clipped to the effect range, with total additional length at most . The realization guarantee in Lemma 4 applies at the single prescribed endpoint precision. Different admissible engines or names may produce different rational endpoints within these guarantees.

Every tuning choice uses the sample size and public exponents, so the same procedure serves all evaluation radii. Clipping uses the known denominator and effect ranges from Lemma 1 and Assumption 3. At sample size one, the full effect interval supplies the specified output. The following result establishes global honesty and the effect-sensitive expected-length bound for this finite-sample procedure.

Theorem 2 [thm:finite-honest-upper] (Uniform honesty and length bound).

There exists an absolute constant such that the following guarantees hold for every choice satisfying:

  • (Arithmetic engine.) is an admissible, independently fixed deterministic rational interval-arithmetic engine satisfying the quantitative contracts of Definition 13.

  • (Naming policy.) is an admissible Borel policy satisfying Definition 12, selecting valid names for the public exponents and observed covariates, with public exponent names fixed independently of the sample.

  • (Public exponents.) The real exponents satisfy

  • (Sample size.) The integer sample size satisfies .

Let denote the measurable interval procedure given by the literal rational output of the upper construction, whose inputs are the engine, naming policy, sample size, public exponents, and observed records. This procedure satisfies where is the class of globally honest procedures in Definition 7.

For every and every observed law , the effect-radius model of Definition 6, Here is the sample of original observed records, is the independent randomization seed with uniform law on the unit interval, and is the diagnostic envelope of Definition 9. The same constant applies to all the engines, naming policies, exponents, sample sizes, radii, and laws quantified above.

For every sample and seed, there exist rational endpoints such that the output is the closed interval and When , every sample and seed yields the full interval .

⊢ Lean

The length bound reflects the structure of the odds identity. Numerator uncertainty contributes even at a zero effect, while denominator uncertainty enters the inversion through a numerator proportional to . This explains the numerator term and the radius-scaled denominator term in Definition 9. Separate ranks accommodate their distinct smoothness requirements, and outward numerical enclosure preserves the ideal interval. Consequently, the literal rational output has global coverage over the ambient model and the stated unconditional expected-length bound on every radius slice, with one common constant across the admissible arithmetic engines and naming policies.

Interpretation and limitations

The sharp expected-length characterization in Theorem 1 separates two sources of uncertainty in the homogeneous causal log odds. The numerator contribution depends on the combined smoothness of the propensity and prognosis logits, whereas the denominator contribution depends on prognosis smoothness and is multiplied by the evaluation radius. Through Definition 9, these contributions give The sharp comparison gives this decomposition an optimality interpretation under its stated conditions: it describes the smallest worst-case expected length on each radius slice among procedures satisfying ambient honesty. The construction in Theorem 2 attains the corresponding upper bound with a single procedure whose tuning uses the sample size and public smoothness exponents.

The distinction between coverage and length evaluation is essential to this interpretation. In Definition 8, the evaluation radius restricts the laws over which expected length is assessed, while admissibility continues to require global coverage over the ambient model in Definition 7. Thus, as the evaluation radius approaches zero, the procedure remains accountable for coverage throughout that model. At radius zero, the denominator contribution vanishes and the numerator contribution remains. The sharp comparison therefore quantifies the precision available at a zero effect while retaining the same coverage obligation for nearby and larger effects.

This behavior follows the structure of the observable odds identity in Lemma 1. The numerator is proportional to the denominator times the exponential effect increment. Consequently, denominator uncertainty has less influence on the recovered log odds when the effect is small, while numerator uncertainty continues to enter the inversion. The separate coordinate estimates and ranks in Definition 14 and Algorithm 1 accommodate these different roles. Joint inversion then converts the coordinate bounds into an interval whose expected length responds to effect magnitude.

The balance can be expressed using the numerator exponent and the denominator exponent introduced in Definition 9. The two contributions are comparable when When , this scale decreases with sample size. Above it, the effect-scaled denominator contribution is larger; below it, the numerator contribution is larger. Rough prognosis can therefore govern expected length at appreciable effect magnitudes even when combined propensity and prognosis smoothness gives a faster numerator rate. Concentrating evaluation near zero progressively reduces that contribution.

The known uniform covariate design and public exponents make this experiment precise. The design in Assumption 1 supplies the integration measure for the projection construction, fixing the geometry used to control approximation error. The public exponents specify the smoothness restrictions in Definition 5 and determine the two resolutions before sampling. Together with the prescribed envelopes, these features support the finite-sample coverage guarantee and the comparison of expected lengths across effect radii. The rational realization in Lemma 4 also gives a concrete numerical meaning to the construction: prescribed precision budgets produce outward endpoint enclosures with the stated additional-length guarantee.

Limitations and future work

The precision characterization concerns a known uniform design, public smoothness exponents, a scalar covariate, and a homogeneous conditional log-odds coefficient. Unknown design would require accounting for the covariate distribution in the projection construction. Unknown smoothness raises a separate adaptation problem, including the coverage requirements appropriate to a collection of smoothness classes. Higher-dimensional covariates would change the approximation problem and its balance with sampling uncertainty.

Heterogeneous effects would require specifying a new target, such as an average contrast or an effect function, together with an appropriate coverage criterion. The scalar inversion and radius-based length objective studied here provide a starting point for formulating such questions; their extensions require separate precision characterizations.

Practical calibration and computational optimization also merit further study. The proved construction supplies coverage and expected-length guarantees with prescribed arithmetic precision. Empirical assessment could examine interval lengths at realistic sample sizes, sensitivity to conservative constants, and numerical performance across admissible implementations. Software development could optimize evaluation of the projection statistics and endpoint enclosures while preserving the stated guarantees. These prospective assessments concern practical performance beyond the proved precision characterization.

Appendices

Identification and projection bounds

The causal full-data extension used for interpretation is the following.

The statistical construction uses observable product coordinates to recover the homogeneous conditional log-odds coefficient. Its causal interpretation follows from the potential-outcome coupling in Definition 15. An admissible coupling for an observed law is a Markov kernel from to whose first and second margins, at every covariate value, are the observed control-arm and treated-arm Bernoulli outcome laws. This specifies the conditional joint distribution of the two potential outcomes. The full-data construction then draws the covariate from the uniform law , draws the potential-outcome pair from this coupling, and draws treatment using the observed conditional treatment probability. The following statement gives the observable coordinate identity and the properties of this construction.

Lemma 1 [lem:observable-odds] (Observable odds and causal interpretation).

Let and , and let , the model class in Definition 5. Write for the uniform probability law on , and define the observable coordinates where is the conditional treatment probability. With where is the treated-arm risk at zero and is the control-arm prognosis logit at zero, one has

For every Markov kernel from to whose first and second margins at every are Bernoulli laws with means respectively, the full-data law of Definition 15 has the following properties:

  • (Observed law and consistency.) The image of under is . For every full-data record,

  • (Construction and conditional exchangeability.) The law is the successive kernel composition obtained by drawing from , drawing from , and drawing from the observed-law treatment kernel with Bernoulli mean . Under its full conditional law at every , the pair and are independent.

  • (Conditional causal log-odds.) For every ,

  • (Full conditional disintegration.) Composing with the full conditional laws of at , then taking the image under the canonical reassociation gives exactly .

⊢ Lean
Proof of Lemma 1.

Fix .

  1. Define, for and , and The strictly positive, normalized conditional cells give and Indeed, each arm risk is the positive success cell divided by its arm total; normalization identifies the control-arm total with . Substitution gives the four factorizations.

    Normalization also gives Expanding the product of the two margins therefore yields

    For the logistic map, write Its odds and log-odds satisfy Since , the homogeneous relation supplied by Assumption 2 gives Exponentiating this identity at the interior arm risks gives Using the four cell factorizations and clearing the positive denominators,

    The cell disintegration and the uniform design in Assumption 1 imply Here the binary product selects exactly the cell . Continuity on the compact covariate interval ensures integrability of the cell functions and their products. Consequently,

  2. We next establish the numerical denominator floor. The numerical exponential bound gives

    Moreover, Positivity of the exponential implies . Hence

    The bounds in Assumptions 4, 5, and 3 supply, at every , Inverting the native logits at the interior probabilities gives The logistic map is increasing and satisfies Together with the homogeneous relation, these facts yield Multiplying these nonnegative lower bounds, Since is a probability law, integration gives

  3. In particular, , so the coordinate identity permits division: Applying the logarithm proves

  4. Fix an admissible kernel . Define its full conditional law by and define the reassociation map by For fixed , the treatment kernel assigns to every potential-outcome pair. Its composition with is therefore precisely . This also makes a measurable probability kernel.

    Associativity of successive kernel composition, applied to the construction in Definition 15, now gives Here the measure inside braces is the joint law obtained by drawing from and then from , and the subscript denotes pushforward. This proves the asserted full conditional disintegration.

  5. Define the observation map by Let be any nonnegative measurable test function. At each fixed , expand the treatment Bernoulli law into its two atoms. The first margin of handles , and the second handles . Thus Integrating over , successive kernel integration and the observed-law cell disintegration give Equality for all such tests proves

  6. For a full-data record, the two treatment cases give The successive-draw construction is exactly that of Definition 15. At every , its full conditional law is the product probability measure The coordinate projections of a product probability measure are independent, so

  7. Finally, pushing the coordinate integrals through the prescribed Bernoulli margins yields Both means are interior. Substitution into the homogeneous log-odds identity established above gives, at every ,

∎

The coordinate identity in Lemma 1 identifies the effect through an observable ratio, with a denominator bounded uniformly away from zero over the model. Its causal clauses establish that every admissible coupling produces the observed law and the same conditional causal log-odds coefficient. Conditional exchangeability is a property of the specified full-data construction, while the marginal restrictions ensure that its potential-outcome risks equal the observed arm risks.

To control the coordinate estimates in Definition 14, retain the rank- cosine projection and ordered-pair statistic from Definition 11. The approximation bound below concerns a continuous function at Hölder exponent , with Hölder seminorm . For two bounded record marks, let and denote their conditional means. The next statement connects approximation of these means to the bias and variance of the product statistic.

Lemma 2 [lem:projection-control] (Projection approximation and moments).

Let be an observed law with continuous, strictly interior conditional four-cell probabilities, satisfying Assumption 1. Let be an integer, and let denote the rank- cosine projection used in Definition 11.

For every and every continuous function , Here is the uniform probability law on , and the norm and Hölder seminorm are interpreted in the extended nonnegative reals, allowing .

For every pair of measurable record marks taking values in , and every integer , define their conditional means using the four-cell conditional law under : For the ordered-pair statistic of Definition 11, evaluated on independent original records with law , and

⊢ Lean
Proof of Lemma 2.

Write and for the norm and inner product in . We use the cosine basis and projection kernel of Definition 10.

  1. Fix , a continuous function , and an integer . If , then because , and the extended-real approximation inequality follows. Otherwise define The definition of the seminorm gives For , this follows by multiplying the defining quotient bound by the positive denominator; for , both sides vanish.

  2. Define the folding map and the even extension by The map takes values in , is continuous, even, and -periodic, and satisfies We also have To see this, choose an integer such that The elementary identities and bounds give, by periodicity and the triangle inequality, Interchanging the two angles proves the asserted Lipschitz bound. Consequently, The extension is continuous, even, and -periodic.

  3. For an integer , introduce the continuous sine quotient and its mass and normalized fourth-power kernel The removable values in the definition are the corresponding limits.

    The finite cosine identity is For completeness, the Chebyshev polynomials of the second kind, defined by satisfy We first derive the polynomial identity Regard these real-coefficient polynomials also as polynomials on . Surjectivity of the complex cosine allows us, for each complex argument, to choose a complex angle satisfying If , then or . Induction in the defining recurrence gives Thus, at either argument, If , induction in the same recurrence, using the sine addition formula, gives Expanding the sine and cosine addition formulas and using yields Dividing by proves The two cases establish the polynomial identity at every complex argument, hence also over the reals.

    For the even-index cosine expansion, introduce the first-kind Chebyshev polynomials by The cosine addition formula and induction give The defining recurrences also imply Indeed, both sides satisfy the same second-order recurrence as sequences in , and their first two values agree: Consequently, The base case is . If the expansion holds at , the last identity gives Thus induction proves with an empty sum at . Starting with and summing these differences yields the displayed cosine identity.

    Integrating that identity, and then its square, gives and Here nonconstant cosines integrate to zero, distinct cosine modes are orthogonal, and each positive-frequency squared cosine has integral . In particular, These formulas include , when the sums are empty.

  4. For , the sine chord bound gives Together with this implies The identity also holds at the removable points. Multiplying by and integrating yields Using the mass lower bound from the preceding step, we obtain The kernel therefore defines a probability measure Jensen’s inequality for the concave function on gives This argument applies throughout .

  5. Define the Jackson approximant on the unit interval by Normalization of the kernel and the increment bound for imply The approximant is continuous.

    It also lies in the cosine span through frequency . Indeed, is an even polynomial of degree ; hence there is a polynomial such that Since , Thus the kernel is an even trigonometric polynomial. Averaging its trigonometric expansion at and removes the sine terms, giving real coefficients , , with Reversing the convolution over one period and using the cosine subtraction formula gives The sine integrals vanish because is even. The reversal follows by a change of variable and periodicity. Since and for , this is the required cosine-span representation.

  6. Now take For every , Consequently belongs to the range of , and where . Hence Orthogonality of the projection gives so, because has total mass one, For , the chosen order is and the approximant is constant, so the same argument applies. In the finite-seminorm case these ordinary norms equal the extended norms in the statement; together with the infinite-seminorm case, this proves the approximation assertion.

  7. Fix measurable marks valued in and . Let be independent records and let be the original independent sample: Writing for the specified four-cell probabilities, the conditional means are Their measurability and the normalization of the cells give so both belong to . Disintegration and Assumption 1 give, for every integrable measurable ,

    Define the symmetric record kernel Swapping the two indices in the complete ordered-pair sum shows that The finite kernel expansion and the preceding conditional-mean identities yield Indeed, and the corresponding identity holds with .

  8. Each distinct pair of sample coordinates has law , and there are such ordered pairs. Therefore Integrating the kernel section from the preceding step gives Here the last equality uses the orthonormality supplied by Definition 10. All sums are finite; bounded marks and the continuous finite kernel ensure integrability.

  9. The same finite expansion gives Expanding the product of the residuals thus yields This proves the bias identity.

  10. For the variance argument define, for all records , Also define the two finite-sample terms These quantities are square integrable: the finite cosine kernel is bounded on the compact covariate square, the marks are bounded, and all sums are finite.

    The kernel mean identity gives . Hence Symmetry of gives symmetry of , so For and , If , integrate first over ; if , integrate first over . In each case the corresponding residual section integrates to zero. If differs from both indices, independence factors the expectation, and the residual mean is zero. Expanding the finite product of sums therefore gives

  11. The explicit formula for the first projection implies Indeed, by the elementary square inequality, and the squared marks are at most one. Applying the residual identity with the same conditional mean in both positions gives and likewise . Uniform design consequently yields Expanding the centered square and using , we obtain Independence makes the cross products between distinct centered sample terms vanish. Thus

  12. The mark restrictions give the pointwise inequality By the finite cosine expansion and orthonormality, and hence To obtain the residual energy, note that integration of a kernel section gives Independence also gives Expanding the defining square of and substituting these identities yields Using the centered-energy identity from the preceding step, this becomes

  13. For two ordered distinct pairs and , residual degeneracy gives For equal index sets, the pairs are identical or reversed, and symmetry gives the first value. For unequal index sets, one record appears in just one factor; integrating over that record first gives zero. This covers both disjoint pairs and pairs sharing one record.

    Each of the ordered pairs has exactly two ordered pairs with the same index set. Expanding the square of the sum therefore gives Equivalently, Since , division by and the residual energy bound yield The counting includes , when the two ordered pairs are reversals of one another.

  14. Finally, summing the defining residual identity over ordered distinct pairs gives Each first-coordinate term and each second-coordinate term occurs times. Dividing by proves the pointwise decomposition Since , expansion of the square, the zero cross moment, and the two established bounds give Together with the approximation, mean, and bias identities, this proves the result.

∎

The product-bias identity in Lemma 2 expresses the approximation error as the inner product of two projection residuals. It therefore connects the smoothness of both conditional means to the bias of their estimated product. The approximation inequality covers the Lipschitz endpoint with the same constant, and the variance bound separates a term proportional to from a term proportional to the projection rank divided by the number of ordered pairs. Under the known uniform design, these bounds apply directly in . Together with the denominator floor and inversion in Lemma 1, they supply the statistical bounds used to calibrate the coordinate error radii in Algorithm 2 and establish the interval guarantee in Theorem 2.

Rational realization and the upper bound

We begin with the representation and primitive arithmetic contracts used by the finite rational construction.

The projection bounds in Lemma 2 supply the statistical ingredients for the coordinate error radii. This appendix establishes their finite rational realization: an explicit admissible arithmetic engine, uniform guarantees at the two prescribed precisions, and a measurable interval output. These conclusions connect the exact coordinate expressions in Definition 14 to the literal interval procedure in Algorithm 2.

The two precision levels control rank selection and final endpoint enclosure. Each primitive is evaluated by a finite rational recurrence with a public iteration bound on valid represented inputs. The guarantees establish termination and endpoint enclosure under the stated rational computation model, with public bounds on primitive iteration counts.

Naming conventions and primitive admissibility

Under Definition 12, a real input is represented by nested closed dyadic intervals containing it, with width at most at integer precision . An admissible Borel naming policy selects public exponent names before sampling and covariate names as Borel functions of the public exponents and original records. The dyadic-floor policy provides the concrete selection specified there.

The independently fixed engine satisfies the primitive contracts of Definition 13. Its transcendental routines enclose the images of rational input intervals, with outward endpoint excess controlled by the dyadic tolerance . The cosine routine uses a midpoint enclosure enlarged by half the input width and clipped to . Exact rational range operations handle arithmetic, extrema, intersections, and clipping. Domain and sign conditions ensure positive logarithm arguments, nonzero division denominators, positive exponential and power lower endpoints, and nonnegative square-root lower endpoints. Each primitive uses a finite rational recurrence with a prescribed public bound on its iteration count. In the power routine, the bound argument denotes a positive integer base.

These requirements specify local arithmetic guarantees. The following statement supplies an explicit engine satisfying them.

Lemma 3 [lem:concrete-arithmetic-engine] (Admissibility of the concrete engine).

The explicit rational arithmetic engine , consisting of the Machin enclosure for , the cosine interval routine, and the endpoint extensions of the scalar exponential, logarithm, square-root, and integer-base power routines, satisfies all primitive admissibility contracts of Definition 13.

⊢ Lean
Proof of Lemma 3.

We verify the finite-computation certificate first, followed by the constant, exponential, logarithm, square-root, power, and cosine contracts. Rational quantities in real inequalities are identified with their real values.

  1. Finite rational computation. For , define For rational and nonnegative integer , put Thus . In the rational computation model, division by zero is assigned the value zero. This convention specifies the routines on their full input domains; the analytic contracts use the domains in Definition 13.

    For rational endpoints define For any rational interval , write

    Here are the scalar routines implemented by the programs. For , define and For the logarithm, define on all rational inputs

    For the square-root routine, set For any , start a binary recurrence with At each iteration retain the endpoints when . Otherwise, with set The invariant and width implication are Indeed, in a nonterminal iteration the midpoint lies strictly between the endpoints, and the comparison selects the endpoint preserving the squared bracket. Each possible new width is at most the old width divided by two and rounded upward. A terminal width of one also satisfies the displayed implication. Since induction on the remaining iterations shows that after iterations the endpoints are consecutive. Define to be the resulting lower endpoint. Then These inequalities uniquely characterize the integer square root. When , the initial bracket is already and remains fixed. Define In particular, this formula returns when .

    For and , put

    For the power routine, denotes the primitive integer base and the scalar exponent. Define The scalar output is The rational-division convention makes this formula total at .

    For a rational input interval the engine uses For cosine, define the rational midpoint and half-width and use

    To certify finite computation, use a finite instruction list acting on rational registers, together with a program counter and a halt flag. Instructions load or copy a rational value, perform rational arithmetic, minimum or maximum, perform integer floor, ceiling, factorial, integer square root, , or nonnegative integer power, compare registers and branch, jump, or halt. Each instruction has unit cost in this model. Integer arguments are obtained by the nonnegative floor convention above. Input coordinates initialize the registers, missing coordinates are zero, and a halted state remains fixed.

    The term recurrences explain both the returned sums and the loop counts. Their current terms are with updates Starting the exponential and cosine terms at one, and the arctangent and logarithm terms at and , respectively, induction shows that the accumulated registers contain precisely the displayed partial sums.

    For example, one joint Machin iteration uses one branch, two divisions by the current odd integer, two additions to the partial sums, two term multiplications, one odd-index increment, one counter decrement, and one jump: ten instructions. Its initialization uses fourteen instructions, and its exit uses seventeen. Thus its public bound is The corresponding accounting for the other endpoint programs is The exponential and logarithm iterations each use seven instructions; the cosine iteration uses nine. Their fixed blocks initialize the terms, preserve the left endpoint while evaluating the right endpoint, form and sort the scalar endpoints, and halt. Induction on the remaining loop count, using the term identities, proves the endpoint-output identities at these bounds. The logarithm exit returns zero on nonpositive scalar inputs.

    The square-root program increments the precision and forms its dyadic scale in four instructions, forms the scaled square and lower endpoint in four, forms the upper endpoint in five, and halts in one. Its integer-square-root instruction agrees with the binary recurrence by the uniqueness established above. Consequently its output registers contain

    For power, the public bound must be computable from the original inputs. Define, for all , The symmetric logarithm bracket gives the exact midpoint identity Since , The triangle inequality for the finite sum therefore gives Define Monotonicity of ceiling yields The fused scalar program computes the logarithm midpoint, evaluates the exponential at the perturbed argument, and performs the displayed clipping. The logarithm stage is bounded by instructions. Connecting to the exponential stage uses one instruction; preparing and evaluating the exponential at a repeated scalar argument uses ; the clipping continuation is bounded by thirty-one further instructions. Hence a public scalar bound is This bounds the actual fused run because and the displayed bound on bounds the exponential loop count.

    For an exponent interval, put The scalar bound is monotone in the absolute exponent, so it bounds both endpoint calls. When , the endpoint program returns and halts after nine instructions. Otherwise its prelude uses at most forty-six instructions; it runs the two scalar calls, uses forty-one connecting instructions, restores the selected endpoints in two, and halts in one. Thus its count is at most The case uses the forty-six-instruction prelude and the totalized scalar formulas. The returned endpoints are the lower endpoint of the left scalar call and the upper endpoint of the right scalar call; normalization therefore gives exactly . Running to the public bound preserves this output because the halted state is fixed.

    Every displayed bound is itself computable by a fixed finite register program from the precision, rational input endpoints, and base when present. On arbitrary rational input lists, precision and base are interpreted by nonnegative floor and missing coordinates by zero. Thus the bounds and output identities hold on the full register-input domain. The six programs together supply finite rational recurrences for all six primitive maps. Their definitions use precisely these primitive arguments, so the choice of is fixed independently of the statistical and naming inputs in Definition 13.

  2. The constant enclosure. For , the finite geometric identity follows by induction on , starting with the empty sum. Dividing by and integrating gives On , the integrand has absolute value at most . Consequently Machin’s identity, and the triangle inequality now imply The remaining calibration is For , this is . Increasing by one multiplies its left side by and its right side by , proving it for every .

    Together with , the approximation bound gives Thus these endpoints are already ordered, their interval lies in , and This proves the constant contract.

  3. The exponential contract. For , the definitions give The factorial inequality follows by bounding each of the last factorial factors from below by . Since the first factorial factor on the left is at least one, Also, The exponential-series remainder estimate states that, for and , Applying it to the real argument and using gives

    The positive floor lies below the exact value: since and , It follows that the two raw scalar endpoints are ordered and that

    For the endpoint extension, exponential monotonicity gives the ordering For every , The lower and upper endpoint excesses are therefore the scalar excesses at and , respectively, and each is at most . The returned lower endpoint is positive by the scalar sign bound. This proves the exponential contract.

  4. The logarithm contract. Let be rational. The ceiling bounds imply Using and clearing the positive denominators in yields Squaring this inequality gives where the last inequality follows by clearing denominators and using .

    To bound the numerator of the remainder, observe that Since and , we obtain The logarithm-series remainder estimate, applied using now gives For the last inequality, , so Thus the symmetric scalar bracket satisfies

    Now suppose . Both endpoint evaluations lie in the positive logarithm domain, and monotonicity gives Every is positive and satisfies The endpoint extension therefore contains the whole image and has outward endpoint excess at most .

  5. The square-root contract. For rational , the floor and integer-square-root brackets give Division by , followed by taking nonnegative square roots, yields The endpoints are ordered and their difference is exactly Containment consequently gives both scalar excess bounds:

    Suppose . The endpoint evaluations satisfy For , square-root monotonicity gives The two endpoint excesses are bounded by the corresponding scalar widths, hence by , and the returned lower endpoint is nonnegative. The argument includes and degenerate intervals.

  6. The power contract. Let and . If , the scalar interval has exact containment, zero excess, and positive lower endpoint.

    For , use the quantities defining the scalar routine above. The precision calibration is Indeed, and therefore The second bound follows from .

    Exponent monotonicity for gives the exact clip range The scalar logarithm contract, applied at precision , implies because each endpoint of is within that tolerance of .

    Define the exact argument and the argument perturbation by Then The local exponential inequality and the identities yield Here the bound on follows from .

    The exponential bracket contains , with each endpoint excess at most . Hence Combining this with the exact clip range proves that the raw endpoints of are ordered and contain . Its lower endpoint is at least . Since clipping increases the lower endpoint and decreases the upper endpoint, both outward excesses are at most where . Thus with the required scalar endpoint excesses.

    Now let Both endpoint exponents satisfy the scalar hypotheses. Because is monotone, For every , The endpoint extension inherits the two scalar excess bounds and the positive lower endpoint. This includes , the exponent endpoints , and degenerate intervals.

  7. The cosine contract. Let be defined by Pairing the even and odd terms gives To verify this identity, start with the empty sum and append successive pairs. In each pair, so the real part increases by exactly the next cosine term.

    Since and , the complex exponential remainder estimate and the bounds on its first omitted term give Together with , this implies that the clipped scalar endpoints are ordered and satisfy

    For the interval routine, define its midpoint enclosure endpoints They obey Because , these inequalities also give Thus the interval routine has exactly the prescribed endpoints

    For every , The cosine Lipschitz inequality therefore yields Combining this with the midpoint enclosure and the global cosine range proves Finally, the endpoint formulas imply This establishes the midpoint excess, enlargement, clipping, image enclosure, and width requirements, including zero-width input intervals.

The finite rational recurrences and the six primitive contracts establish admissibility under Definition 13.

∎

The witness in Lemma 3 establishes existence at the primitive level. Its finite rational routines provide one concrete choice for the interval construction. The precision guarantees below apply uniformly to every admissible engine, including this witness.

Uniform realization at fixed precision

Rank selection follows Algorithm 1: the public exponent intervals are intersected with the prescribed exponent boxes, and the ceilings of the upper target-enclosure endpoints determine the two integer ranks. These ranks are fixed before sampling. Endpoint evaluation then uses precisely those retained integers in the coordinate estimates, variance envelope, error radii, and precision budget of Algorithm 2. At that step, the queried exponent and covariate intervals enter the endpoint expression tree in their supplied form.

The next statement establishes admissibility of the concrete naming policy and derives the rank, endpoint, and measurability guarantees from the primitive contracts.

Lemma 4 [lem:fixed-budget-realization] (Fixed-budget realization and measurability).

The dyadic-floor naming policy is admissible in the sense of Definition 12. Moreover, suppose that:

  • (Engine and names.) is an admissible rational interval-arithmetic engine in the sense of Definition 13, and is an admissible Borel naming policy in the sense of Definition 12.

  • (Sample size.) is an integer with .

  • (Public exponents.) The real smoothness exponents satisfy

For every record tuple , let be the ranks selected according to Algorithm 1, with target resolutions The prescribed public budgets are At the rank budget, both rational target enclosures and are successfully returned and satisfy Here denote the upper endpoints of the resolution enclosures.

For the endpoint construction, use instead to denote the coordinate error radii where is the public variance envelope at rank . Let be the numerator and denominator coordinate estimates, and set where is the denominator floor. With denoting the clipped logarithmic inversion of the coordinate ratio, the ideal lower and upper endpoints are At the endpoint budget, rational enclosures and are successfully returned with The literal output satisfies It is a nonempty closed connected interval with rational endpoints in , and its output map, as a function of the record tuple, is Borel measurable.

⊢ Lean
Proof of Lemma 4.
  1. Admissibility of the dyadic-floor policy. For a real input and an integer precision , define The floor inequalities give and therefore where throughout the proof Moreover, multiplying the floor inequalities by two yields Since the middle term is an integer, these inequalities imply The conclusions include dyadic inputs, which may equal the lower endpoint of a queried interval. At each fixed precision, both rational endpoints are Borel functions of the real input because the floor function is Borel. Composing these functions with the public exponent coordinates and the observed covariate coordinates gives precisely the validity and Borel requirements in Definition 12. Thus is admissible.

  2. Resolution enclosures at the rank budget. Fix an admissible engine , an admissible policy , , exponents in the stated domain, and a record tuple . Set Let the exponent-name intervals after the intersections prescribed in Algorithm 1 be Validity of the names and the exponent domain ensure that both intersections succeed and that Define the rational denominator and power-exponent boxes by exact interval operations: Both denominator boxes have lower endpoints at least one and widths at most . For any denominator box with , exact division gives and Consequently, both power-exponent boxes lie in , contain their respective exact exponents, and have width at most .

    For a power exponent , using and . The mean-value bound and the outward endpoint errors required by Definition 13 therefore show that the returned target boxes satisfy To pay for this width, the integer logarithmic ceiling in Algorithm 1 gives Since , it follows that All rank-step intersections and divisions have thus succeeded, the power inputs satisfy the primitive domain requirements, and both returned boxes have the required unit-width bound.

  3. Bounds for the selected ranks. The exponent domain makes both target exponents positive. Hence In particular , so the nonnegative ceilings in Algorithm 1 are their ordinary integer ceilings. Containment and the unit-width bounds give Using the strict upper bound for an integer ceiling, The last inequalities follow from . These ranks depend on the public exponent names and are fixed before sampling. In particular, From this point onward, denote the coordinate error radii in Algorithm 2.

  4. Coordinate enclosures at the endpoint budget. Retain the selected ranks and set At this precision, write the raw name responses as These boxes contain their named inputs and have widths at most . Since , one has Containment and the width bound place each raw covariate box in Indeed, each endpoint is within one box width of the contained covariate.

    For any displayed scalar expression , denote its computed enclosure in the prescribed tree at precision by This notation refers to the supplied raw responses, the fixed engine, and the exact rational range operations.

    We use two elementary properties of these operations. For closed rational boxes , define Inserting a cross product when subtracting two products, and then taking the extrema among endpoint products, gives Widths add under addition and subtraction. The endpoint formulas for minimum and maximum also give For example, each upper endpoint is at most its corresponding lower endpoint plus the larger width; taking minima or maxima preserves that inequality.

    We now evaluate the basis and kernel from Definition 10. Define the primitive constant boxes Their contracts give For the second inclusion, follows by squaring, and the upper endpoint error is at most .

    For a basis index , the intermediate argument boxes are They satisfy Thus the product-width inequality yields The cosine contract returns a box in whose width is at most Multiplication by the square-root box therefore gives For , the basis expression is the exact constant one, so these magnitude and width bounds also hold.

    Each computed basis-product term consequently has width at most . Summing the terms in the kernel, for either retained rank , gives At , the sole basis-product term is exact.

    The binary marks used in Definition 14 are exact rational numbers in . Multiplication by their products preserves the displayed kernel-width bound. There are exactly ordered pairs. Hence the positive rational normalization in Definition 11 cancels this factor in the sum of widths: for the marks used here. The empirical mean in is exact. Soundness of the operations therefore supplies successful coordinate boxes with

  5. Error-radius enclosures. The endpoint budget gives and therefore Validity of the raw exponent responses gives Define their bias-exponent boxes by They contain and , respectively, and satisfy

    For either retained rank , the elementary inequality for gives Applying the same inequality at gives . Thus, for every exponent in the corresponding raw power-exponent box, It follows that These inequalities include , for which the derivative is zero. The mean-value bound and the primitive endpoint errors now imply with the corresponding bias-exponent box.

    The variance quantity is an exactly evaluated positive rational number. Its square-root enclosure therefore satisfies Using the constants in the radius expressions, we obtain successful enclosures containing , with The last inequalities use and .

  6. Denominator-corner enclosures. Define the computed denominator boxes by the prescribed exact clipping tree: Here the minus sign denotes interval subtraction. Soundness supplies containment of , and the endpoint formulas give Before clipping, the widths are bounded by because and . Clipping by point intervals preserves this bound by the minimum and maximum width inequalities. Consequently, In particular, every subsequent denominator interval has a positive rational lower endpoint.

  7. Numerator-corner widths and magnitudes. Define These boxes contain , and

    We also require bounds on their endpoints. The exact basis satisfies including . Therefore The ordered-pair normalization and marks of absolute value at most one give The empirical treated-outcome mean has absolute value at most one, so Since , Taking square roots yields Moreover, and give Thus

    To control the computed endpoint overhang, the two logarithmic ceilings in the endpoint budget give hence Comparing coefficients with this product shows For the last two comparisons, use

    A box containing and having width at most one has every point within distance one of . It follows that This supplies both the width and magnitude bounds at the actual numerator inputs to inversion.

  8. Enclosures of the four inversion corners. For signs , define For a denominator box with , its reciprocal range satisfies Exact division is multiplication by this reciprocal range. The product-width bound therefore gives containment of the true ratio and

    Define the exponential boundary boxes and the clipped odds boxes by The exponential series, bounded termwise by the geometric series, gives and consequently The primitive endpoint errors and imply Thus every clipped odds box has lower endpoint at least , contains the exact clipped odds, and satisfies Here the added exact constant one preserves width, and the minimum and maximum width inequalities bound both clipping operations.

    Define the inversion-corner boxes by The logarithm derivative is at most two on every argument interval with lower endpoint at least . Its primitive contract therefore supplies successful boxes containing the four exact corner values, with For the coefficient comparison, implies and This establishes the required precision for each of the four corner evaluations.

  9. The two endpoint boxes. The literal minimum and maximum operations return Monotonicity of minimum and maximum in their arguments preserves containment, giving Their widths satisfy All raw input queries and all intervening evaluations have succeeded. Every power input lies in its required domain, every square-root input is nonnegative, every division has a positive denominator interval, and every logarithm input has a positive lower endpoint. The finite sums at the retained finite ranks and the primitive termination contracts in Definition 13 therefore give successful return of both boxes at the single endpoint precision.

  10. Outward enclosure and rational interval shape. The exact clipped logarithmic map in Algorithm 2 satisfies at the endpoint inputs: its logarithm argument lies between and . For each positive denominator, division, clipping, and logarithm are nondecreasing in the numerator. Since and , Consequently, Define the literal rational output endpoints by Containment of the exact endpoints and their effect bounds give Thus the intersection in the output construction succeeds and the literal output is The endpoint-width bounds give Adding these inequalities yields Finally, The output is therefore a nonempty closed connected interval with the asserted rational endpoint shape.

  11. Borel measurability. Keep the engine, policy, sample size, and public exponents fixed. The ranks and endpoint precision are then fixed integers. Define the finite response code and its countable range by The binary coordinates and the fixed-precision name responses are Borel, so is Borel into the discrete countable space . The public exponent responses are fixed, and the remaining computation uses this code through finite rational operations. Hence For any set of output intervals, define The preceding implication gives the fiber decomposition This is a countable union of Borel sets. In particular, inverse images of Borel sets of intervals are Borel, establishing the claimed measurability of the output map.

∎

The rank precision gives an additive rank excess below two for each coordinate. The endpoint precision depends on the sample size and the larger retained rank. The same selected integers therefore govern both the exact statistics and their rational evaluation. Together with the finite recurrence contracts, successful evaluation at these prescribed precisions establishes termination of the construction in Algorithm 2.

In the inversion, denotes the ideal upper effect endpoint. The rational output uses the outward endpoints , followed by clipping to the effect envelope. Its samplewise containment of the ideal interval and additional length bound of hold for every record tuple. The Borel conclusion concerns the resulting map from the original observed records, under each fixed admissible naming policy.

Connection to honesty and expected length

The rational interval in Algorithm 2 combines these realization guarantees with the statistical bounds. The bias and variance bounds in Lemma 2 calibrate its coordinate error radii; the denominator floor and odds identity in Lemma 1 supply the joint inversion. Lemma 4 establishes measurable outward enclosure of the resulting ideal interval with a controlled length increment.

Under the engine, naming-policy, and exponent conditions of Theorem 2, the literal procedure has global coverage over the ambient model for every integer sample size . On every effect-radius slice, that result bounds its unconditional expected length by an absolute constant times the diagnostic envelope in Definition 9. Numerator uncertainty contributes directly to this envelope, while denominator uncertainty contributes at the scale of the effect radius. At , the specified full effect interval completes the procedure.

Different admissible engines and valid naming policies may select different ranks and return different rational endpoints. For each choice, the realization bounds apply to its own retained ranks and ideal endpoints. The coverage and expected-length guarantees in Theorem 2 share one absolute constant across all such choices. In particular, Lemmas 3 and 4 supplies the explicit engine and dyadic-floor policy for the concrete attaining sequence defined in Definition 19.

Exact calibration and same-model alternatives

The calibrated alternatives are specified by the following maps and continuous sign families.

The lower-bound constructions use exact calibration to combine a homogeneous conditional log-odds coefficient with continuous nuisance functions. We first describe the local equations and their smooth neighborhoods, then state the support guarantees for the finite sign families in Definition 18. The calibration maps are defined in Definition 17.

The covariance adjustment prescribes the odds ratio of a binary table with treatment margin and outcome margin . Its normalized extension extends the effect-normalized adjustment smoothly through zero effect. The mixed equation uses the signed propensity amplitude and signed outcome amplitude ; the fair equation uses the signed control-risk amplitude . In the latter equation, the residual smoothly extends the matching discrepancy normalized by the effect and squared amplitude. The within-cell coordinate ranges over .

The scalar implicit-function theorem supplies the local graph representation needed for these calibration equations. Its conditions concern an open parameter domain, differentiability, and a nonzero derivative with respect to the scalar being calibrated.

Lemma 5 [lem:scalar-implicit-function] (Scalar implicit function theorem).

Let be a nonnegative integer, let , and let . Fix and . Suppose that:

  • (Open domain.) is open and .

  • (Smoothness.) is continuously differentiable on .

  • (Zero.) .

  • (Nonzero partial derivative.) .

Then there exist open sets and , and a function , such that The function is continuously differentiable on , satisfies , and has for every . Moreover, for every and every ,

⊢ Lean
Proof of Lemma 5.
  1. Since is open and contains , the smoothness hypothesis gives continuous differentiability at this point. Define the continuous linear map The chain rule for the map gives By linearity, Define This map is continuous and linear, and the preceding identity gives Thus is invertible.

  2. The general implicit-function theorem for Banach-space products, applied with scalar-coordinate derivative , supplies a function such that Its local graph identity, together with , gives throughout a neighborhood of .

  3. Intersect this neighborhood with . The product topology supplies neighborhoods of and of satisfying Choose open neighborhoods and with Continuous differentiability of at also supplies a neighborhood such that

  4. Continuity of at , the identity , and openness of imply Hence we may choose an open set satisfying The inclusions established above yield while restriction to gives continuous differentiability of on , and Finally, for every and , the graph identity on gives These are the required properties.

∎

The open-domain condition makes the calibrated scalar a differentiable function of the remaining parameters, including at parameter values that will lie on the boundary of the eventual support region. The local uniqueness conclusion identifies the zero set with that function throughout the product neighborhood. For the two calibration equations, Lemma 6 supplies fixed brackets and common open neighborhoods for the resulting branches.

Specifically, the mixed neighborhood contains a closed region with signed amplitude radius , and the fair neighborhood contains a closed region with signed amplitude radius and effect coordinate in . Both amplitude radii exceed the calibration radius used for support. A further neighborhood allows the fair margin to vary freely within a centered bracket of half-width ; here denotes a root-bracket width. The next statement establishes these neighborhoods together with the exact matching identities and derivative bounds.

Lemma 6 [lem:exact-calibrations] (Exact smooth calibration branches).

There exist constants and with the following properties. Expectations below are over two independent fair signs, and The covariance adjustment and its normalized extension are given by The mixed root is selected from the roots in of with value when that bracket contains no root. The fair root is selected from the roots in of , with value when that bracket contains no root. Here is the smoothly extended normalized fair-matching residual, whose defining identity away from the axes is displayed below.

  • (Positive odds tables.) For every satisfying put . The four cells are strictly positive and satisfy Moreover,

  • (Signed mixed calibration.) For every , , and , put . Then and

  • (Fair calibration and separation.) For every , , and , put . Then For , the residual at the selected root agrees with the unnormalized fair-matching numerator divided by . Furthermore, and

  • (Smooth neighborhoods and derivative bounds.) Both roots and every fully substituted local four-cell formula of the mixed and fair families are on their respective closed parameter regions For every integer , there is a constant such that the norm of the th total derivative of each root and each fully substituted local four-cell formula is at most throughout its respective closed parameter region, uniformly over all family indices, auxiliary signs, and binary cell indices.

    There also exist signed amplitude radii and , a fixed fair-root bracket half-width , and open sets containing, respectively, Throughout , the selected mixed branch is the unique zero in its fixed bracket ; throughout , the selected fair branch is the unique zero in the fixed centered bracket . Both roots and every fully substituted local four-cell formula are on the corresponding open set.

    Finally, there is an open set containing on which is . Throughout this displayed core, for every margin in the centered bracket and whenever ,

⊢ Lean
Proof of Lemma 6.

We use the maps in Definition 17, with the root-selection and fallback conventions in the statement. For , write These parameter regions are compact. We write for the th total derivative of a parameter function , with .

  1. Uniform existence and uniqueness of the mixed root. Define the mixed residual, wherever its branch denominators are positive, by The integral defining is smooth, and the fundamental theorem of calculus gives At zero amplitudes the branch radicand is , its denominator is , and Consequently, for every , The radicands and denominators remain positive near these points, so the residual is smooth there.

    Compactness of , continuity, and the finite number of sign pairs give a positive signed amplitude radius on which all branch denominators are positive and In particular, The intermediate value theorem supplies a zero in , hence in .

    Separately, continuity of the root partial derivative and compactness of give another positive signed amplitude radius on which Taking the minimum of these two radii gives such that Indeed, the derivative inequality makes the residual strictly decreasing throughout the selection bracket.

  2. Smoothness and derivative bounds for the mixed root and cells. At each , the root is and its root partial derivative is . Apply Lemma 5 on an open neighborhood where the residual is smooth. The resulting local graph stays in after shrinking its parameter neighborhood. The negative root derivative persists throughout that bracket nearby, so the selected root agrees with this graph.

    The same graph is smooth to every finite order. To see the regularity upgrade explicitly, implicit differentiation gives On a smaller neighborhood the denominator remains nonzero. If the graph is , this formula makes its first derivative , and therefore makes the graph . Starting from the graph supplied by the cited result proves smoothness to every finite order. Compactness of the spatial interval then gives such that is smooth on a neighborhood of every point of .

    For clarity, define the fully substituted mixed cells. For a family index , a sign pair , and , put All arguments on the last line are the displayed parameters and sign pair. At zero amplitudes, the covariance formula is evaluated at , where its radicand and denominator are positive. The chain rule therefore makes every displayed cell smooth near each . Compactness in and finiteness of the indices give on whose closed mixed region all these cells are smooth on pointwise neighborhoods.

    For each fixed , continuity of the total derivatives on the corresponding compact regions gives positive constants satisfying Here the finite index set is Thus the positive constant bounds the th derivative of every mixed cell uniformly over its indices.

  3. The smooth fair residual. In the fair calculations use the baseline risk and its normalization and define the unnormalized residual by We first check the domains needed for its derivatives.

    For , the elementary exponential bounds give If , then so both logarithm arguments in are strictly positive.

    The following calculation also supplies the comparator bounds used to justify smooth composition. Define The preceding inequalities imply The comparator formula becomes For , the inequalities and , valid for , yield Indeed, and Apply these inequalities with and . Since we obtain, including and , The last pair follows from .

    For every real , the two sign terms give . Thus, for and , Together with and , this makes the risk-shift denominators positive. All these strict positivity conditions persist on ambient neighborhoods. Hence is jointly smooth near every point of the indicated parameter range.

    Sign symmetry and the dependence of on give The last equality uses , , and .

    The normalized extension is the double Taylor integral Here are integration variables. Their compact range permits one ambient neighborhood on which the integrand is smooth for all integration points. Differentiation under the two integrals then proves joint smoothness of on that neighborhood, at every finite order.

    The fundamental theorem of calculus, using , gives The second-order integral Taylor formula gives Interchanging the two integrals therefore proves the undivided identity throughout , , , and . For , division gives the quotient in the statement.

  4. Fair endpoint factorization and the removable axes. At either spatial endpoint the law of is one fair sign. Exponentiating the comparator formula gives or, equivalently, Clearing the positive risk denominators using this identity proves It follows first for that at . For each nonzero , continuity in extends this equality to ; continuity in then extends it to . Thus

    To identify every endpoint zero, define The second expression is positive on the fair range , , . Directly clearing the same denominators and substituting the corrected exponential identity above gives For , the undivided Taylor identity cancels the amplitude square: Continuity in extends this identity to zero amplitude, where it reads For and , the inequality gives Thus, when , the zero-amplitude endpoint residual has the sign of . At either endpoint, when also , the factored unnormalized identity shows that every matching root in the selection bracket equals .

    We also need position independence at zero amplitude. The sign moments are Differentiating the averaged risk twice in amplitude gives The comparator term has no spatial argument, so Their effect derivatives agree as well, including at the endpoints of the effect interval by smoothness and the one-sided derivative there. Substitution in the double integral proves

    For zero effect, differentiation of the explicit comparator gives Using the two sign moments, Differentiate the undivided Taylor identity at . For , cancellation of gives the first identity below; continuity in supplies the same identity at : Within , the zero is therefore . Combining these facts yields Here uses the explicit quadratic formula, and uses the negative residual factor.

  5. Uniform fair-root existence. The preceding factorization shows opposite bracket signs at zero amplitude when . At , the explicit extension gives Hence throughout the compact effect and spatial ranges, Joint continuity and compactness preserve these strict inequalities for , for some Continuity in the margin and the intermediate value theorem then give The strict endpoint signs put the zero in the open bracket.

  6. Smoothness of the selected fair root. Differentiate the zero-amplitude factorization at , where the residual itself vanishes. This gives For , all factors except the derivative on the left are positive, and the right side is positive. At zero effect, the explicit extension gives Therefore the center slope is positive throughout the full effect and spatial ranges.

    Continuity of this partial derivative and compactness give a radius satisfying whenever The zero-amplitude uniqueness from the preceding steps also confines all nearby roots. Indeed, the set is compact, and is nonzero on it. Continuity therefore gives such that If the displayed compact set is empty, the implication follows directly from its defining condition.

    Take the minimum of , and . Every selected root on the resulting closed fair region is a genuine bracket zero, lies in the center neighborhood, and has nonzero margin derivative. Moreover, these controls give uniqueness on ambient parameter neighborhoods: positivity persists on the compact center bracket, and nonvanishing persists on the compact portion of the larger bracket outside it. Any two nearby bracket zeros must therefore lie in the center bracket, where the residual is strictly increasing.

    Apply Lemma 5 at each selected zero. Nearby bracket uniqueness identifies the selected root with the local graph. The first-derivative identity is The regularity upgrade used for the mixed graph applies again. Thus there is such that is smooth on a neighborhood of every point of .

  7. A preliminary common radius and the quadratic fair bound. Define Then and is smooth on pointwise neighborhoods of its closed region.

    The endpoint and axis computations identify the selected roots there: For the first equality, split first on , then on ; the zero-effect and zero-amplitude uniqueness computations settle these cases. When both are nonzero, endpoint matching and the negative residual factor force the selected bracket root to be .

    The numerator is even in . Its second amplitude derivative is consequently even, so its effect derivative and the double integral satisfy The selectors for these identical equations have the same value, including their common fallback convention. Hence

    Smoothness and compactness give positive bounds for the two partial derivatives needed below. More explicitly, define Both maxima exist because the indicated partial derivatives are continuous on the compact region.

    For a smooth even function , its derivative at zero vanishes, and the integral Taylor formula gives If on the segment joining to , then Every amplitude on that segment has absolute value at most .

    Apply this first to , and then to , with fixed in their prescribed ranges. Both functions are smooth and even. Their zero-amplitude values are respectively and . For the latter value, constancy of on forces the spatial derivative to vanish also at : the available two-sided derivative equals the zero one-sided derivative from the interval. Therefore and hence

  8. Fair-cell regularity and common derivative bounds. For the same auxiliary indices as before, define These are functions of , with the signs evaluated in .

    On every input the fair selector belongs to : it either selects a root there or takes the fallback value , which is also in that bracket. Consequently, when , Indeed, , and adding this bound to either side of the selection bracket proves the displayed bounds. The local effect is nonnegative by the comparator range estimate. Hence The chain rule, root smoothness, and positivity of the logarithm arguments now prove smoothness of every fully substituted fair cell on neighborhoods of the closed fair region.

    For each , compactness gives positive bounds Set Restriction to the smaller mixed region preserves its earlier bounds. Thus All these functions are on their respective closed regions.

  9. Fixed open branch neighborhoods. We construct open sets for the actual selectors and cells. Define At every , the local implicit graph through , its bracket range, and the persistent negative root derivative give the unique selected zero nearby. The root and all mixed cells are smooth on those same neighborhoods. Therefore Openness and compactness of this spatial segment give such that By the defining conditions, the mixed selector is the unique bracket zero throughout , and it and all mixed cells are smooth there.

    For the fair branch fix and define At each in the full effect and spatial ranges, the local implicit graph starts at , and therefore stays in nearby. The ambient uniqueness argument from the center derivative and compact root exclusion identifies it with the selector from the larger bracket. Smoothness of the residual holds on an ambient open set; the derivative upgrade applies to this same graph at every nearby point. The outer cell formulas have positive denominators and logarithm arguments at zero amplitude, so all fair cells are smooth nearby as well. Consequently, Compactness gives a positive amplitude radius for which the corresponding closed fair region lies in . Reduce that radius to obtain

    For the residual itself define The compact integration ranges in its Taylor representation give a common neighborhood of smoothness around every point of Since , the required centered fair core with amplitude radius is contained in . The residual is smooth on , and its quotient identity on this core follows from the undivided Taylor identity.

    Finally define Then which supplies the strict separation between the eventual closed-region radius and both open-neighborhood radii.

  10. The final common radius. Set In particular, and The inclusions preserve smoothness, every derivative bound , and the quadratic estimate with the same positive . The open sets and the larger signed radii remain as constructed.

  11. Positive odds tables. Suppose Since , the standard estimate for gives Write the branch radicand as The elementary variance and margin-product bounds give and therefore The covariance formula consequently satisfies Every unadjusted cell product is at least . Thus each adjusted cell is at least Direct addition gives both prescribed margins and total mass one.

    Put . Squaring the square root and clearing its positive branch denominator gives Expanding the four cells now yields Since , division proves the stated odds ratio.

    Finally, in the branch formulas gives Thus when . At , the branch denominator is and , so

  12. The signed mixed identities. For , the established bracket-root existence makes the selector a genuine root: The two endpoint sign laws give identical residual functions and therefore identical selected values: Using , multiplication of the normalized root equation gives This multiplication also covers either zero-amplitude axis.

    The separate sign symmetries follow algebraically from the normalized branch. First, for this follows from , and at it follows from . Under , the branch coefficients transform as The square root and the whole denominator are consequently divided by the positive number , just as the normalized numerator is. This proves Exchanging the two margins gives Substitution in the mixed residual gives, with the root argument fixed, Identical residuals give identical selectors, so the two asserted root symmetries follow.

    On the axes, the zero-effect normalized formula and reduce the residuals to When , the candidate lies strictly in ; the affine equation forces every selected zero to equal it. Hence For the other axis, gives The intermediate value theorem supplies a zero in , hence in the selection bracket. Substitution of the selected zero into the reduced equation proves These arguments include and .

  13. The fair identities and separation. Fix and put . The comparator calculation already gives The preliminary radius construction supplies a bracket root and the identities The endpoint sign laws give identical fair residuals at , hence Evenness supplies , and the previously obtained quadratic bound gives

    To verify the normalized equation on the entire range, first consider . The zero-amplitude center is a genuine bracket zero. If and , the endpoint center is a genuine bracket zero by the continuity argument through both axes. In the remaining case, uniform bracket-root existence and the selector definition give the root equation directly. Thus in all cases The selector lies in , so the fair Taylor identity applies at this margin. For , it gives For all , including the axes, its undivided form gives By the definition of the numerator, this is exactly Together with the closed-region regularity, derivative bounds, and open neighborhoods already constructed, these are all the asserted properties of the positive constants and .

∎

The mixed calibration fixes the mean covariance adjustment exactly while allowing both margins to vary with the signs. The fair calibration instead matches the mean shifted risk, expressed through the logistic risk shift from Definition 17, to a deterministic comparator. Its effect separation is between and , while the comparator effect remains between and . These identities specify the separation and matching simultaneously on the stated parameter regions.

The smoothness conclusion concerns the fully substituted cell probabilities as well as the calibration roots. Thus the derivative bounds incorporate the dependence of each cell on its calibrated margin. The open neighborhoods also include zero amplitudes and zero effect, where the normalized equations have their smooth extensions. In the fair family, both the displacement of the calibrated margin from and its within-cell derivative are bounded by a constant times the squared amplitude.

We now apply these local maps to the shared-endpoint construction in Definition 18. A finite endpoint sign vector determines the trigonometric field on the equal partition, with adjacent cells sharing the sign at their common endpoint. The endpoint identities in Lemma 6 make the calibrated margins compatible with this continuous field. The following statement certifies model membership for every sign realization, together with the exact singleton matching and uniform amplitude derivatives needed for the sample mixtures.

Lemma 7 [lem:calibrated-support] (Uniform calibrated support and smoothness).

There exist jointly chosen absolute constants , the calibration radius, and , the derivative bound, satisfying with the following properties for the calibrated families of Definition 18. Throughout, is an integer and is a sign vector.

  • (Mixed membership and effects.) For every , the prescribed domain of public smoothness exponents, set The calibrated mixed laws and at these amplitudes belong to as defined in Definition 5, and their homogeneous conditional log-odds coefficients satisfy For each treatment label, outcome label, and covariate , the sums over all sign vectors of the corresponding conditional cell probabilities under the two mixed laws are equal.

  • (Fair membership and effects.) For every , set For every , the fair random law and the deterministic fair comparator belong to , and where is the calibrated comparator effect defined in Definition 17. For each treatment label, outcome label, and covariate , the uniform average over the sign vectors of the conditional cell probability under equals the corresponding comparator cell probability.

  • (Signed validity and derivative bounds.) For all signed amplitudes satisfying the conditional four-cell tables of both mixed branches are valid probability tables, as are those of both fair branches for every . For every sign vector, branch, treatment label, outcome label, and covariate , their one-record densities relative to uniform four-label measure lie in . The mixed densities, viewed as functions of , and the fair densities, viewed as functions of with fixed, are twice continuously differentiable at every point of the corresponding closed amplitude box. The norms of their first and second total amplitude derivatives are at most , uniformly over all these indices and amplitudes. These bounds include the mixed second derivative in and and the deterministic comparator’s derivatives in .

  • (Common smooth neighborhoods.) There exists an open subset of containing on which every mixed density is infinitely continuously differentiable in its amplitude arguments. There also exists an open subset of containing on which every fair density is infinitely continuously differentiable in . Each neighborhood is common to every integer , sign vector, branch, treatment label, outcome label, and covariate ; the fair neighborhood is also common to every .

  • (Signed singleton matching.) For every and , and each treatment label, outcome label, and covariate , the sums over all sign vectors of the corresponding conditional cell probabilities under the two mixed laws are equal. For every and , the uniform average over all sign vectors of each conditional cell probability under the fair random law equals the corresponding cell probability under the deterministic fair comparator.

⊢ Lean
Proof of Lemma 7.

We use the calibration maps and families of Definitions 17 and 18. All finite coordinate spaces below carry the maximum norm, and total derivatives carry the induced multilinear operator norm.

  1. Local formulas and smoothness radii. By Lemma 6, choose a calibration radius on which the stated smoothness, endpoint, and matching identities hold.

    For a local sign pair , write For , define the local mixed cells by and The arguments of these cells are .

    Use and for the random and comparator fair branches, respectively. Their local risks and cells are The comparator expressions are independent of .

    The smooth-neighborhood conclusion of Lemma 6 supplies positive radii and on whose closed parameter regions all these local formulas are smooth at every point. Set Thus, whenever , the local mixed formulas are smooth at every and the local fair formulas are smooth at every

    For preliminary estimates, interpret a supplied spatial cell profile through the convention In either case the covariate law is . We will establish the first case throughout the required neighborhoods.

  2. A uniform bound for amplitude derivatives. The local derivative bounds supplied by Lemma 6 give positive constants and positive radii such that, for , These are total derivatives in the three displayed arguments, uniformly over the finite indices. Define In particular, and .

    The amplitude slices have linear parts For a smooth function, the th derivative of its composition with an affine map is its th derivative evaluated on the linear part in each argument. Consequently, fixing , or fixing , gives The factor four comes from density relative to the uniform measure on the four labels. These bounds involve the fully substituted formulas, including the comparator effect.

  3. Fair prognosis estimates. By Lemma 6, choose and such that for , , and . Put All three radii are positive, and Hence, for , Since , both fair control risks lie in : the random risk differs from by at most , and the comparator risk by at most .

    We record the logit estimates used here and below. For , the mean value theorem applied separately to the logarithms of the risks and their complements gives Thus Also, with we have . The elementary inequalities therefore imply This proves the fair prognosis envelope on .

    For a valid fair profile, comparison with the fixed risk yields The triangle inequality consequently gives For an invalid preliminary profile, its replacement has prognosis logit zero, so the same oscillation inequality holds.

    For any auxiliary radius , any , and any , set Because , It follows that where the last inequality uses .

    For the linear estimate, define the within-cell coordinate by Here and : below the last cell this follows from the floor inequalities, and in the last cell it follows from . In particular this convention includes and .

    Within a cell, the elementary sine and cosine difference bounds give Adjacent profiles agree at the shared sign. Subdividing a segment at its cell boundaries therefore gives Similarly, smoothness of the fair root, its derivative bound, and give Thus each fair control risk satisfies Applying the logit difference bound, or using the zero logit in the replacement case, proves For , Since , we obtain These estimates apply to both fair branches uniformly over .

  4. Mixed propensity and alternative-prognosis estimates. The mixed-root smoothness and derivative bounds in Lemma 6 supply a positive radius and a constant such that for , . Indeed, the spatial derivative is the total first derivative evaluated on the unit vector in the spatial coordinate.

    The endpoint identity for , followed by the mean value theorem within each cell and subdivision across cells, gives Together with , , and the field estimate above, the product decomposition gives For , the mixed margins satisfy Their propensity margins consequently belong to . For a valid profile, summing the treated cells identifies its propensity with , and hence The replacement profile has propensity logit zero, giving the same bound. Define For with and , we therefore have

    For the alternative prognosis, consider the control-logit map It is smooth near : the covariance branch is smooth there, the denominator equals at the center, and the argument of the logit equals . A function is locally Lipschitz. Choose a neighborhood , a Lipschitz constant , and such that Set Comparing points with the same first coordinate gives whenever

    Define For , we have . At the rate-scaled amplitudes with , Moreover, The control-logit comparison therefore applies to the alternative margins. The two margin differences obey For a valid table, its control risk is Using gives The replacement case again has zero prognosis logit.

  5. One radius and the remaining mixed spatial bounds. Choose Every entry in the minimum is positive. Therefore

    We supply the remaining mixed estimates at For every nonnegative exponent , Thus .

    For the null branch the control risk equals whenever the profile is valid. The logit and field bounds give because . In the replacement case the left side is zero.

    For oscillation, comparison of the propensity margin with gives and hence

    We also need a covariance estimate for the mixed prognosis. For define The elementary exponential bound and the margin bounds give Consequently, The rationalized covariance formula now yields so The first inequality uses ; the second uses .

    For the mixed alternative, and its margins lie within of . Thus, for either branch, Summing the control cells gives , so their risk satisfies The bounds imply by multiplication and the displayed rational bounds. Hence . Since , Applying the logit comparison with , and using , gives Therefore All these bounds also hold for the zero logits of a replacement profile.

    Combining these estimates with the preceding linear estimates proves, for both mixed branches,

  6. Continuity and validity on the doubled boxes. Fix and . On cell , use the local pair and coordinate . For the local cell formulas are continuous in , by Lemma 6 and .

    At a shared endpoint, the two sign fields take the same value: The endpoint identities therefore make every mixed and fair cell agree across adjoining cells. Gluing the finitely many continuous cell profiles proves continuity on , including its endpoints. When , there is one continuous profile and no interior boundary to glue.

    Because , the raw mixed cells satisfy Each product entering a mixed cell lies in . Accordingly, which implies

    For the fair cells, the selected root belongs to ; this includes its default value . Since both fair control risks belong to . For , the elementary exponential estimate gives The comparator effect lies between and , by Lemma 6. Thus the effect used in either fair branch lies in . For and , To check the last bounds, the denominator is positive; multiplication by it reduces the lower bound to using , and the upper bound follows from and . Consequently both fair arm risks and their complements are at least , and

    Finally, direct addition of either four-cell formula gives Every cell lies in , so the cells are strictly interior. Together with continuity, this proves validity throughout both doubled closed boxes. The constructed laws therefore retain their supplied cells there.

  7. Transfer to actual densities and common open neighborhoods. Let be the uniform probability measure on the four treatment–outcome labels: Define the actual one-record densities, relative to , by The amplitudes of the laws on the right are those on the left.

    Fix , and define its local sign pair by Validity on the doubled boxes identifies the actual densities there with the local slices: For the comparator the chosen pair is immaterial.

    At a point of the smaller closed box, continuity of absolute value supplies a neighborhood lying inside the doubled box. Thus these identities hold on a neighborhood of every such point, and differentiation transfers the local bounds to the actual densities. Since ,

    Moreover, set These sets are open and contain the required closed boxes. At every point of them, nearby validity identifies the actual density with a smooth local slice. Because , every mixed density is on , and every fair density is on , uniformly over the indicated indices and over . In particular, they are at every point of the smaller closed boxes.

    For clarity, with the total second-derivative bound includes It also applies to both first and second -derivatives of the deterministic comparator.

  8. Mixed model membership and effects. Fix , , and the rate-scaled amplitudes They lie in the valid smaller box. The constructed covariate marginal is uniform: for every Borel set ,

    We identify the homogeneous effects from the positive cell odds. For the covariance formula introduced above, the identity and give, by multiplication by the positive denominator, For a table with margins and covariance , expansion of its four cells then gives This computation includes . The null table, with covariance zero, directly satisfies . Therefore the mixed branches satisfy All four cells are positive. Dividing by the positive treatment margins gives Taking logarithms, and evaluating at covariate zero to identify the scalar effect, proves The effect envelope follows from The propensity margin and the control risk lie in , as established above, so

    To convert the spatial bounds into the required Hölder bounds, let , , satisfy Set If , then If , then The first case includes , and both cases include . Thus Apply this argument to with and to with . Together with uniform design, homogeneity, and the three envelopes, these are precisely the conditions of Definition 5. Hence both mixed laws belong to .

  9. Fair model membership and effects. Set Both fair branches are valid. Their treatment probability is exactly , because the two cells in either treatment arm sum to . Therefore This supplies the propensity envelope and both propensity spatial bounds.

    The choices and the fair estimates above give, for both branches, The two-scale calculation in the preceding step gives

    For any interior risk , the positive denominator in the shift formula yields Applying this identity to the control risks of the two fair branches gives their positive cell cross-odds relations, and hence By Lemma 6, Thus both effects satisfy the envelope . Uniform design follows by the same cell-normalization integral as above. All conditions of Definition 5 now hold for every random fair law and for its deterministic comparator.

  10. Singleton identities at the rate-scaled amplitudes. Fix , and put The indices and are distinct members of , including when . For any function of their two signs, counting the extensions of each pair gives Consequently the full sign average of each cell is its local two-sign average.

    Write for this uniform two-sign average: Symmetry and the trigonometric identity give The mixed calibration identity in Lemma 6 supplies Expanding the four local cells, using these moments and this identity, yields The cells of the actual laws equal these supplied cells by validity. Multiplying the equal full sign averages by proves the asserted mixed sum identities.

    For the fair family, Lemma 6 gives The control-risk average is , by . Since treatment is fair, the four averaged cells are therefore These are exactly the comparator cells. Counting sign extensions and using validity proves the required full uniform-average identity. The calibration identities invoked here apply also at , at zero amplitudes, and at .

  11. Signed matching and completion. Now allow arbitrary signed amplitudes satisfying They lie in the calibration region because , and their tables are valid by the doubled-box argument. The preceding local moment calculation and the matching identities of Lemma 6 apply on this whole signed region. Thus, for every , and, for every ,

    Finally, the raw cell bounds established on the doubled boxes transfer directly to the actual densities on the smaller boxes: Together with the first- and second-derivative bounds, the common smooth open neighborhoods, and the rate-scaled membership and effect calculations, these prove every assertion. The radius and bound were selected from absolute local calibration constants; their choices are independent of , the public exponents, the sign vector, the labels, the covariate, and the fair effect .

∎

Membership in Definition 5 certifies the prescribed envelopes and Hölder restrictions for the native propensity logit and prognosis logit , together with the homogeneous logistic relation. This certification applies to every sign realization at the stated amplitude scales and throughout the prescribed domain of public exponents. Continuity across partition endpoints and the homogeneous scalar coefficient therefore hold for each law entering the finite priors in Definition 18.

Exact singleton matching concerns every conditional cell probability at every covariate value. For the mixed families, the two uniform sign averages agree despite their distinct homogeneous coefficients. For the fair family, the uniform sign average agrees with the deterministic comparator at its calibrated coefficient. The matching identities continue to hold throughout the signed amplitude boxes, providing exact cancellations alongside the first and second amplitude derivative bounds.

Finally, the density bounds and common smooth neighborhoods in Lemma 7 are uniform in the partition size, sign vector, labels, and covariate. They furnish a joint regularity certificate for the actual one-record densities, including the mixed cross derivative and the comparator’s amplitude derivatives. Together with the effect identities, these properties provide same-model alternatives with controlled separation for the original-record lower-bound argument.

Original-record lower bounds and sharp comparison

The calibrated families in Definition 18 and their joint support certificate in Lemma 7 provide the alternatives for the expected-length lower bounds. The comparisons concern sample laws on the original record space , including the observed covariates. We first fix the normalization of the distance used to compare these laws.

Definition 20 [synth_6] (Squared Hellinger distance for original-record sample laws).

For probability laws on the original-record sample space , define their unhalved squared Hellinger distance by where is any common dominating measure. The value is independent of the choice of and lies in . For the continuous calibrated mixtures, take to be the original-record sample reference measure. This normalization assigns coefficient one to the displayed integral.

The normalization in Definition 20 fixes the numerical constants in the mixture comparisons. Both comparisons use the radius and envelope constant from the same joint certificate in Lemma 7. The following bounds apply when the average number of observations per partition cell satisfies the stipulated occupancy threshold.

Lemma 8 [lem:original-record-mixtures] (Original-record mixture bounds).

Let and be the radius and envelope constant selected from the fixed joint calibrated-support certificate, with and . Define the positive constants For sample laws , use the unhalved squared Hellinger distance where is the original-record sample reference measure.

For every choice satisfying

  • (Sample and partition sizes.) are integers with and .

  • (Occupancy.) .

  • (Signed amplitudes.) satisfy

let , for , and be the uniform finite mixtures of the calibrated mixed and fair original-record sample laws, respectively: where the expectation averages uniformly over the finite sign vectors. Let be the deterministic fair comparator obtained from the fair construction at partition size , center , and amplitude , using the constant numerical sign vector with every entry equal to . Then and, for every ,

⊢ Lean
Proof of Lemma 8.
  1. Fix the joint certificate from Lemma 7, and fix admissible sample sizes and amplitudes. Since and , Write Under the identification of an ordered record sample with its covariate and label vectors, the reference measure is For a law in the calibrated families, define its conditional label density by The support certificate supplies throughout the prescribed signed amplitude domains.

  2. We first bound the covariate-dependent component weight. For , define Thus the cells are half-open, with assigned to the last cell. Let For every , put and define Counting components by their vertex sets gives the identity The term of size is zero.

    Here is the component probability estimate used to integrate this identity. Fix a nonempty set and a root . Define the set of parent arrays by An array is valid when there exists a height function satisfying For a valid array, define its edge event by If is a component, choose each nonroot vertex’s parent one step closer to the root in the induced graph. Graph distance then supplies the required height function. Consequently,

    For any fixed parent covariate , Indeed, a point in cell lies between that cell’s two endpoints, and the two cell numbers differ by at most one. The displayed interval has length at most ; hence In a valid array, a nonroot vertex of maximal height has no children. Integrating its covariate first removes one edge and costs at most . Repeating this operation leaves the unrestricted root, whose mass is one. Thus including the one-vertex case, where the edge product is empty. Summing over parent arrays yields Therefore

    To evaluate this finite envelope, use the nonnegative exponential series: for every integer , Also, because each factor in the falling factorial is at most , with the binomial coefficient equal to zero when . Set The occupancy hypothesis gives , and the preceding two estimates imply, term by term,

    For completeness, the finite cubic sum has the required numerical bound by an elementary induction. Define For , The empty sum satisfies this inequality. For the induction step, split off the first term and apply the induction hypothesis at ; the resulting bound follows from At , multiplication by gives Combining the estimates, In particular, for every , The weights are integrable finite sums of measurable component indicators.

  3. We now prove the mixed inequality, first treating its degenerate cases. If , signed singleton matching in Lemma 7 gives If , the two four-cell tables in Definition 18 agree for each sign vector: the propensity is , the effect is zero, and the covariance adjustment at zero effect is zero. Thus . If , reversing all signs gives instead the draw-wise identity Here the outcome margin is , the covariance adjustment is zero, and sign reversal exchanges the two propensity margins. Since permutes the uniform finite prior, again . In both amplitude cases the Hellinger distance and its claimed upper bound are zero. Henceforth, for the mixed comparison, take , , and .

  4. Fix the full covariate vector . We describe the conditional component decomposition explicitly. For each nonempty , and for the empty block, define Distinct nonempty components have disjoint endpoint-sign sets: sharing an endpoint would make the corresponding cell numbers equal or adjacent. These sets therefore partition the endpoint signs. For an assignment , use the extension Every record in depends only on the assigned signs. Each assignment has exactly completions to a full sign vector, so restricting the uniform prior preserves each block average.

    For , define the full and component conditional densities by The covariates remain fixed in the component notation. The empty component density is one. Independence of the disjoint sign groups and finite distributivity give

    To make the Hellinger tensor bound transparent, define component label masses and affinities by Normalization of each conditional four-cell table yields All masses are nonnegative. The last equality, together with nonnegativity of the squared sum, shows . Regrouping labels by their component restrictions factors the full affinity into the product of these affinities. The elementary inequality follows by induction from for .

    Define the conditional discrepancy by Since each label vector has reference mass , scaling the densities by turns this integral exactly into the squared root discrepancy of the corresponding label masses. The affinity calculation therefore proves Finally, the common uniform covariate marginal and the displayed product densities give, by integration over covariates and labels,

  5. We bound each mixed component’s pointwise square-root discrepancy. If , both densities are one. If , restriction of the uniform prior and signed singleton matching in Lemma 7 give equality of the two densities. Thus, for ,

    Suppose , and fix its labels. Define, throughout the signed amplitude square, For a fixed sign assignment, put Here each law on the right is evaluated at . The derivative and common-neighborhood assertions of Lemma 7 imply The partial derivative bounds follow by evaluating the total derivatives on unit coordinate vectors.

    Product differentiation gives, with , These estimates can be proved together by induction on . For the empty product its value is one and all its derivatives vanish. On adjoining , the first derivative bound is controlled by The mixed product rule has four terms: Their absolute sum is at most using . Differentiation commutes with the finite sign averages, so subtraction of the two averages yields The one-record density floor also gives

    The same table identities used in the amplitude cases, now applied to a block average, imply For the second identity, reverse the component signs, a permutation of their uniform prior. The two closed segments joining zero to and lie inside the certificate’s signed square. The mean value bound along the -segment therefore gives for every between zero and . Applying the mean value bound along that -segment next gives Both estimates apply to either orientation of the segments.

    The positive density floors justify the square-root identity and bound This proves the pointwise component bound for every block, including the unused-sign block.

  6. Averaging the pointwise bound over a component’s labels preserves it, since there are label vectors: Summing over components and integrating over the original covariates now yields The conditional discrepancy is nonnegative, and the integrable component weight supplies the integrable upper bound.

  7. Fix for the fair comparison. If , signed singleton matching in Lemma 7 gives If , the formulas in Definitions 17 and 18 give ; the random and comparator tables then agree for every sign draw. Thus These cases satisfy the desired inequality. Take henceforth and .

  8. First establish a reduction for any auxiliary amplitude . With the covariates fixed, define The random laws in these displays are evaluated at . Averaging a sign-independent product is exactly that product: Restriction of the random prior to each component and finite factorization consequently give For each of the two component densities, summing its scaled label mass gives For the random density this follows by commuting the finite sign average with the label sum; in both cases the label sum factors into normalized one-record sums.

    Define the component affinities and conditional discrepancy by Expanding the squared difference and using normalization gives and Here the affinity factors by finite distributivity, and the inequality is the finite-product inequality for numbers in . The common covariate marginal also gives where in this display is evaluated at the auxiliary amplitude.

  9. For , the two fair component densities agree: the empty products are one, and the singleton identity follows from signed singleton matching in Lemma 7 and restriction of the uniform sign prior. Hence their square-root discrepancy is zero.

    For , fix the component labels and define, on the whole signed interval, For the derivative calculation, define the one-record factors and their partial products by The random law on the right is evaluated at . By Lemma 7, both kinds of factors are twice continuously differentiable and satisfy For either kind of partial product, the product rule and induction give To see the second-derivative induction explicitly, adjoining a factor gives whose absolute value is at most Here denotes the adjoined one-record factor and the product over , of either kind. The first-derivative induction uses The empty product again has value one and zero derivatives. Finite averaging and subtraction therefore imply, for , The density floors give

    At zero amplitude the random and comparator tables coincide, so The fair root is even in its amplitude by Lemma 6; the comparator effect in Definition 17 depends on the amplitude through its square. Reversing the component signs consequently proves Differentiating this equality at zero, using the supplied smoothness, gives If , the difference is already zero. If , Taylor’s theorem with Lagrange remainder provides such that Thus in either case, Using this last bound and the two positive floors, Together with the small-component cases, this estimate holds for every .

  10. Summing the fair pointwise bound over component labels with their reference masses, then summing over components, gives Integration over the original covariates therefore establishes the nonnegative-amplitude reduction As before, the conditional discrepancy is nonnegative and the component weight is integrable.

  11. Finally, restore the signed amplitude. The fair-root evenness and the square dependence of the comparator effect give, throughout the signed certificate interval, The notation in the first identity displays the amplitude argument of the random fair law. Reindexing the finite sign average by shows that the fair sample mixture is even as well. Thus, if use , and if use , to obtain The mixture on the right is evaluated at . Since , the nonnegative-amplitude reduction applies, and gives Every estimate used the same fixed certificate and was uniform over , proving both asserted bounds.

∎

The two bounds in Lemma 8 quantify the statistical proximity of the same-model alternatives certified by Lemma 7. The mixed comparison depends on the squared product of the propensity and outcome amplitudes; the fair comparison depends on the fourth power of its outcome amplitude and is uniform over the stated centers. Both retain the factor and use a common constant determined by the joint density envelope. Exact singleton matching and the signed derivative bounds in Lemma 7 supply the calibration properties underlying these comparisons.

Expected length is evaluated on the radius slice in Definition 6, while coverage is required throughout the ambient model by Definition 7. Consequently, alternatives in the ambient model constrain interval length at laws in an evaluation slice. The parametric comparison records this implication uniformly over all radii, including zero.

Lemma 9 [lem:parametric-null-floor] (Parametric lower bound on length).

Let and satisfy:

  • (Exponent domain.) , the public exponent domain given by

  • (Sample size.) .

  • (Radius.) .

Then the minimax expected interval length defined in Definition 8 satisfies

⊢ Lean
Proof of Lemma 9.
  1. Fix the parameters in the statement. For every , define the observed law by where is the logistic map, The four conditional cell probabilities are constant in , strictly positive, and sum to one. Thus this construction has continuous interior cells and uniform covariate marginal , which has full support.

    Summing the treated cells gives treatment probability ; dividing each success cell by its arm probability gives control risk and treated risk . Moreover, Consequently, for every , The nuisance envelopes and seminorms therefore satisfy Together with the uniform design and homogeneous relation, these identities verify every condition of Definition 5 whenever .

    Define the comparison amplitude and laws by Since , Hence, using Definition 6, Indeed, the radius condition at the null is , including when .

  2. All four null cells have probability . The likelihood ratio of relative to is therefore This bounded density establishes absolute continuity and integrability of its squared deviation. Define its one-record chi-square divergence by Summing over the four null cells gives For every real , differentiation yields The mean-value bound, together with , consequently gives

  3. The amplitude has the exact information budget Since the exponential lies above its tangent at zero, Comparison of the exponential and geometric series gives the required numerical bound:

    For the record tuple define the product likelihood ratio and its chi-square divergence by The product likelihood ratio is bounded and is the density of relative to . Because each likelihood ratio integrates to one, independence implies Applying this identity at to the preceding exponential bound yields

  4. Total variation is the supremum of the absolute differences of measurable-event probabilities. For probability laws with a density, it equals half the integral of the absolute density difference. Cauchy–Schwarz therefore gives where the last inequality follows from .

    Define the full sample-and-seed experiment laws by Their likelihood ratio is still . Integrating over the common independent seed, whose law has mass one, gives The comparison effects are ordered:

  5. To bound the infimum in Definition 8, first observe that the honest-procedure class is nonempty. Define By Assumption 3, for every , The constant procedure is measurable and hence belongs to the class in Definition 7.

    Now fix any For , define the measurable coverage events Both comparison laws belong to the ambient model, so Assumption 9 gives

  6. The total variation bound transfers the second coverage event to the null experiment: Using the union–intersection identity and the fact that the union has probability at most one,

    Write . On the intersection event, membership of both effects implies These weak endpoint inequalities apply to every choice of endpoint inclusion. Off the intersection event, interval length is nonnegative. Thus Admissible intervals lie in the scalar effect region, so Their measurable lengths are therefore integrable. Integrating the pointwise bound yields

  7. Since , its expected length is bounded above by the supremum over that slice: This supremum is finite because every expected length is at most one. The bound holds for every honest procedure, and that class is nonempty. Taking its infimum as in Definition 8 gives

∎

At zero radius, Lemma 9 gives a positive uncertainty floor for expected length under the null slice. The coverage requirement still ranges over the ambient model, so uncertainty about neighboring effects enters the criterion even when length is evaluated at zero effect. The statement also covers procedures using the independent randomization seed , since these procedures belong to the class defining the minimax objective in Definition 8.

Combining this parametric floor with the mixed and fair comparisons gives the lower side of the sharp expected-length profile. The upper side is attained by the literal interval output defined in Algorithm 2, with its coverage and length guarantees from Theorem 2. The resulting comparison holds throughout the public exponent domain and for every admissible engine and naming policy.

Theorem 3 [thm:sharp-honest-frontier] (Sharp honest interval frontier).

There exist positive finite absolute constants with the following guarantees. Write and define the numerator and denominator exponents and the expected-length profile by

For every admissible rational interval-arithmetic engine and every admissible Borel policy satisfying the quantitative contracts of Definitions 13 and 12 and selecting valid names for the public exponents and observed covariates, consider parameters satisfying:

  • (Exponent domain.) .

  • (Sample size.) and .

  • (Radius.) .

Let denote the interval returned by the fixed-budget upper construction. With as in Definition 7, define the minimax expected length by where is the prescribed effect-radius slice, is the sample of original records, and is an independent seed with uniform law on the unit interval. Then The same constants apply to every admissible engine and naming policy.

For every such engine and policy, every , and every , the actual name-dependent output is a deterministic, radius-independent Borel interval with global coverage over , the prescribed ambient model. It is a nonempty closed connected interval contained in , with rational endpoints, returned after the two prescribed finite precision budgets and finite rational arithmetic. Its inputs consist of the fixed engine, the public exponents and their valid public names, and the original records and their valid covariate names. Fixing the explicit admissible engine and dyadic-floor naming policy gives the concrete attaining interval where are the comparison constants and is the sample-size threshold.

Moreover, for every , every , every , and every , including procedures using independent randomization,

For every , the exponent difference is positive and satisfies At , the two displayed expressions agree.

Finally, for every nonempty compact set , the same constants and threshold satisfy the compact-uniform conditions

⊢ Lean

The two terms in Theorem 3 distinguish uncertainty in the numerator coordinate from effect-scaled uncertainty in the denominator coordinate. The mixed alternatives supply the radius-independent lower contribution, together with the parametric floor when the numerator exponent reaches ; the fair alternatives supply the contribution proportional to the evaluation radius. Thus the null slice retains the numerator rate, whereas every fixed positive radius eventually makes the slower denominator rate dominant. The positive exponent difference stated in the theorem establishes this ordering throughout the prescribed domain. A single globally honest interval attains the comparison simultaneously across radii.

The following synthesis collects the statistical comparison, the finite-budget realization from Lemma 4, and the concrete engine supplied by Lemma 3. It identifies the attaining procedure with the actual output for each admissible engine and naming policy.

For the concrete sequence below, the inputs are the sample size, public exponent representations, and represented original records, together with the independently fixed arithmetic engine and naming policy. The same radius-independent sequence is evaluated over each radius subclass.

Theorem 4 [thm:full-honest-frontier-solution] (Full honest frontier solution).

There exist absolute constants , with and , for which the following assertions hold. Write and define the expected-length profile by

For every admissible rational interval-arithmetic engine , every admissible Borel naming policy , both satisfying the quantitative contracts of Definitions 13 and 12, every , and every integer , take the literal output of the fixed-budget represented upper construction. This procedure belongs to the globally -honest Borel class of Definition 7. It receives neither the radius nor unknown nuisance functions and terminates on every valid named input within the prescribed rank and endpoint budgets of Algorithm 1, Algorithm 2, and Lemma 4. For every sample and randomization seed its output is a closed interval with For every , the same constants satisfy Here is the minimax expected length of Definition 8, and the expectation uses original records drawn independently from , together with the independent randomization seed .

In particular, the explicit concrete engine and the dyadic-floor naming policy give the sequence For every and , this sequence is globally honest, has the rational closed ordered output described above at every input, and satisfies the same displayed comparison for every .

Moreover, for every , every , every integer , and every , including procedures using independent randomization,

The exponent difference is positive throughout and obeys At , the two displayed expressions agree.

Finally, select the lower and upper comparison constants and sample-size threshold as For every nonempty compact , these choices satisfy

⊢ Lean

The statistical and computational guarantees in Theorem 4 concern the same interval: its rational endpoint construction preserves global coverage and the sharp expected-length comparison at every sample size. The original-record lower bound covers the entire honest class, including randomized procedures, while each admissible implementation attains the comparison with the same absolute constants. Selecting these constants and the threshold also gives uniform comparisons on every nonempty compact subset of the public exponent domain.

Verification note

The supplied theorem and lemma statements and their proofs are machine-checked in Lean 4 under their stated assumptions. The frozen formal layer covers identification and projection control in Lemmas 1 and 2; rational arithmetic and finite-budget realization in Lemmas 3 and 4; local implicit-function arguments, exact calibration, and model support in Lemmas 5, 6, and 7; and original-record mixture bounds and the parametric floor in Lemmas 8 and 9. The resulting coverage, expected-length comparison, and attaining construction are consolidated in Theorems 2, 3, 4, and 1.

The model restrictions defining Definition 5 and the primitive contracts stated in the corresponding results are hypotheses of these implications. The global coverage criterion defining Definition 7 specifies the admissible statistical procedures. Admissibility of the concrete arithmetic engine, finite termination and endpoint enclosure for the represented construction, global coverage, and the sharp comparison for the length objective in Definition 8 are established conclusions. The recorded external-dependency sets for these declarations are empty.

For the represented construction, valid names satisfying Definition 12 supply enclosing dyadic intervals for the public exponents and observed covariates. Together with the rational primitive contracts in Definition 13, they support the rank selection and endpoint realization in Lemma 4. The explicit arithmetic witness in Lemma 3 supplies an admissible engine, and its combination with the dyadic-floor naming policy yields the concrete attaining interval identified in Theorem 4.

The formal source tree is CausalSmith/CausalSmith/Stat/STAT_LogoddsLowsmoothFrontier_Research/, with its aggregate module at the corresponding .lean path. The declaration-to-paper mapping is CausalSmith/doc/presentation/stat_logodds_lowsmooth_frontier_v1/presentation_crosswalk.json; it records repository source revision 1efc342d4a68f9860ec0aa7692071d90a9230018. In a checkout of that revision, run

cd CausalSmith
lake build CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research

The Lean toolchain is pinned in CausalSmith/lean-toolchain, and package dependencies are pinned in CausalSmith/lake-manifest.json under the project configuration CausalSmith/lakefile.toml. The same presentation directory contains lean_snippets.json, references.bib, paper_macros.tex, and the crosswalk needed to reproduce the manuscript links and inspect the exact declarations rendered in each numbered environment.

Proofs of the main results

Proof of Theorem 1.
  1. Choose the constants supplied by Theorem 4, with Its universal construction guarantee applies simultaneously to every admissible engine and naming policy, every , every integer , and every , with these same constants. Its compact-uniform guarantee, elbow identities, and converse for every globally honest procedure, including independently randomized procedures, give the corresponding assertions of the present theorem. In particular, its choices give, for every nonempty compact ,

  2. Fix and an integer . The concrete sequence in Theorem 4 is exactly as specified in Definition 19. That guarantee yields For every sample and seed, it also gives rational endpoints such that

  3. Fix . Expanding the diagnostic envelope of Definition 9 and its identification with the rate profile in Definition 19 gives Thus the concrete comparison supplied by Theorem 4, expressed with this explicit profile, is Together with the assertions retained in the first step, this establishes all the stated guarantees with the same constants.

∎
Proof of Theorem 2.

We first establish the bounds for . Fix an admissible arithmetic engine , an admissible naming policy , and public exponents satisfying and .

  1. Define the retained ranks, smoothness sum, and rate exponents by These are the ranks and exponents of Algorithm 1 and Definition 9. For , put Here are the coordinate error radii, as in Algorithm 2.

    By Lemma 4, with target resolutions the ranks satisfy In particular, both ranks are positive and are fixed before sampling.

    For either pair the lower rank bound and give Also , so the upper rank bound yields Both powers are nonnegative. The last expression is bounded by because expansion of this square gives coefficients on both squared terms and a nonnegative cross term. Taking square roots therefore gives Each power on the right is at most the power with exponent . Since , Consequently, The exponents are positive, and . Thus

  2. With the denominator floor and sensitivity coefficients defined by choose All its summands are nonnegative, so . For every , the preceding bounds imply The second inequality uses . The last inequality follows by adding the nonnegative terms that complete the common coefficient . This choice depends solely on the fixed denominator floor.

  3. Fix . Write where is the uniform law of the independent seed. Variances below are under this same probability law.

    We first control the unconditional absolute mean of the numerator estimate. Define, for , The homogeneous relation and native-logit bounds are those of Definition 5. The logistic derivative satisfies The derivative bound on the interval between any two real arguments gives Hence, for , The comparison of the two covariate powers uses and ; it also holds at , since both exponents are positive.

    The marginal mean has the decomposition Since , the preceding moduli imply Thus These functions are continuous: the propensity and marginal mean are sums of continuous conditional cells.

    Define the empirical treated-outcome mean by The coordinate definition in Definition 14 gives Using the projection expectation and residual identities from Lemma 2, we obtain Cauchy–Schwarz and the approximation bound in the same cited statement yield Here , , and , so the approximation bound applies throughout the stated range.

    Independence of the records and give Also, Lemma 2 supplies The variance identities for a sum and a difference give where the inequality uses nonnegativity of the last variance. The finite-rank statistics are square integrable, so all these identities and subsequent expectations are well defined.

    Cauchy–Schwarz on the probability space gives Consequently, For the last step, and .

    By Lemma 1, The product defining is at most one pointwise, so where the two conditional off-diagonal probabilities are Since , the exponential derivative is bounded by on the segment between and . Therefore In particular, for ,

  4. We next bound the interval length on every sample. Use the confidence endpoints and clipped inversion of Algorithm 2: Clipping is a composition of minimum and maximum with fixed constants, each of which contracts absolute differences. Thus

    For real numbers satisfying , the inequality for gives Interchanging the two arguments handles the reverse order. Applying this bound to the clipped arguments, and using contraction of the exponential-range clipping, gives for all real numerators and positive denominators.

    For the rectangle points with we have Inserting the cross quotient with numerator and denominator yields It follows that every pairing of an upper-numerator corner and a lower-numerator corner satisfies the same difference bound. Choosing the corners attaining the maximum and minimum , including either choice in a tie, gives By Lemma 4, the literal rational output has additional length at most . Hence, pointwise,

  5. For , integrate the pointwise bound. The ranks and radii are fixed before sampling, and the numerator estimate is integrable. Therefore The last inequality is the deterministic calibration established above.

  6. To establish honesty, take any . The numerator bias and variance bounds have already been established. For the denominator, the conditional probabilities defined above satisfy All their factors lie in . Adding and subtracting the product with the first factor evaluated at and the second at gives Thus both continuous functions have Hölder seminorm at exponent bounded by one.

    The denominator marks and have conditional means and . The expectation and residual identities in Lemma 2 therefore give Cauchy–Schwarz and the cited approximation bound imply The variance bound in the same cited statement applies to these bounded marks: Together, the four coordinate moment bounds are

  7. Define the coordinate failure events by The triangle inequality and the bias bounds imply Both variance radii are strictly positive. Integrating each squared centered coordinate over its displayed event gives Consequently,

    Outside their union, We have already shown . Clipping is nondecreasing and fixes every point of , so For a fixed positive denominator, is nondecreasing in its numerator. For a fixed real numerator , its behavior as the positive denominator varies follows from The clipping and logarithm preserve these inequalities. Applying them first to , then to , and using numerator monotonicity yields By Lemma 1 and the effect envelope, Thus outside . The containment supplied by Lemma 4 gives on every sample. Hence The coverage probability is therefore at least . The Borel output property from the same cited statement gives measurable coverage events and interval length. Since was arbitrary in the ambient model, this proves

  8. Now let . If , the first branch of Algorithm 2 returns at every input. The effect envelope gives coverage one, and its length is one. For every , If , the integer assumption implies , and the honesty and expected-length bounds established above apply. Thus the same positive constant gives both assertions for every admissible engine, policy, exponent pair, sample size, radius, and law in the theorem.

  9. Finally, every branch of the literal output construction either takes a nonempty intersection of a rational endpoint box with the full effect box or returns the full effect box. Each resulting box has ordered rational endpoints and is contained in ; the output includes both endpoints. Consequently, for every sample and seed there exist such that For , the full-box branch gives the asserted equality with at every sample and seed.

∎
Proof of Theorem 3.
  1. Fix the joint calibration constants supplied by Lemma 7, and use the corresponding positive constants from Lemma 8. Define These are finite absolute constants, and the ceiling gives For the argument below, write the worst expected length of an admissible procedure as We work throughout with , , , and , unless a narrower range is specified.

  2. We first establish the rank estimates used in both mixture constructions. For every real , define Since , the ceiling inequalities yield The exponent is at least one, so Moreover, . Raising the lower rank bound to the positive power therefore gives and hence Finally, raising the upper rank bound to the negative power , and using , gives All these estimates include .

  3. Suppose first that . Define the mixed rank and amplitudes by The domain conditions imply and . Since , The rank estimates and the calibration of give and, by the laws of real powers, Thus Lemma 8, applied to the mixed priors of Definition 18, supplies

    We give the testing-to-length argument needed here and for the fair priors. Let and be uniform finite mixtures of original-record sample laws. More precisely, for , take an integer , define and suppose that their constituents have common effects Assume that every evaluation constituent belongs to , every alternative constituent belongs to , and all constituents have uniform covariate law.

    Let be the uniform probability law on the four binary label pairs, and define the original-record reference and mixture densities by These densities are nonnegative and integrate to one. With total variation defined by the squared Hellinger distance satisfies Cauchy–Schwarz gives Factoring the density difference and applying Cauchy–Schwarz again yields The product densities with respect to are the same densities, independent of the seed. Integrating over that seed proves Consequently, a squared Hellinger bound of gives total variation at most for the sample-and-seed experiments.

    Define the measurable coverage events Global honesty and finite averaging imply Transferring the second event by total variation, then using that a union has probability at most one, gives Connectedness of the returned interval gives the pointwise inequality Integration and finite averaging therefore show The procedure’s measurability and bounded interval length justify these integrals. This argument includes independently randomized procedures.

    For the mixed priors, Lemma 7 supplies model membership and the effects The null constituents belong to every evaluation slice because . Applying the preceding reduction with as evaluation prior gives Since the denominator is positive, Thus, defining we have proved

  4. For the radius-dependent lower bound, suppose and define Here , , and . The rank estimates imply By Lemma 8, The fair support assertion in Lemma 7 supplies model membership and The random constituents belong to the evaluation slice because . The comparator can be regarded as a constant finite prior: averaging identical copies leaves its sample law unchanged. By Lemma 6, Using the random fair prior as evaluation prior in the testing reduction, and then the rank separation estimate at , we obtain Define We have therefore proved

  5. Choose the positive finite absolute upper constant supplied by Theorem 2, and set For every admissible engine and naming policy, that result supplies together with Here the identification of the diagnostic envelope with is Definition 19. Taking the supremum over the slice and using the infimum definition in Definition 8 gives The slice is nonempty: the law has and hence satisfies the model conditions and belongs to every slice with .

    The upper result also supplies Borel measurability, global coverage, and the ordered rational closed output in the effect envelope. The construction in Algorithm 2 depends on the fixed engine, public inputs, selected names, and original records, and therefore satisfies Its input list makes it radius independent. For , Lemma 4 supplies successful termination within the two prescribed budgets and finite rational evaluation. For , the construction returns directly.

  6. Define the common lower constants by Both constants are strictly positive. If , the mixed bound gives If , positivity of gives By Lemma 9 and the infimum definition of , This proves the numerator bound throughout , with equality included in the first case.

    For the radius bound, is covered above. At , nonnegativity of interval length gives Thus

    Each summand of is nonnegative. Reducing both coefficients to their minimum and adding the two lower inequalities yields This is the asserted converse for every honest procedure, including independently randomized procedures.

  7. The honest class is nonempty: the constant procedure returning is Borel and covers every ambient-model effect by Assumption 3. Its length is one, while all procedure objectives are nonnegative. Taking the infimum of the preceding all-procedure lower bound is therefore legitimate and gives Combining this with the upper comparison proves For the upper procedure, seed independence implies, for every law , which gives the displayed comparison in the statement. The constants were chosen independently of the engine and naming policy.

    By Lemma 3, is admissible, and Lemma 4 supplies admissibility of . Specializing the universal comparison and operational properties to this pair gives

  8. Let be nonempty and compact. The constant functions with values and have singleton images on , so The constant upper bound gives These are the required compact-uniform conditions for the same constants and threshold.

  9. It remains to establish the exponent identities. The domain conditions give As already verified by comparison of the two entries of the minimum, In the first range, subtraction over the positive common denominator gives In the second range, If , positivity follows from and the positive denominators. If , it follows from and the positive denominator. Thus At , both branch identities apply to the same difference, and consequently This establishes agreement at the boundary and completes the proof.

∎
Proof of Theorem 4.
  1. Choose the absolute constants supplied by Theorem 3, so that and . For every admissible engine , admissible naming policy , exponent pair , and integer , that result applies to the literal construction It supplies membership in , Borel measurability, and termination on every valid named input within the prescribed budgets. The inputs are the fixed engine, the public exponents and their selected names, and the original observed records and their selected covariate names, as specified in Algorithms 1 and 2. For every sample and seed, the returned interval has the form For every , the same result gives where is the uniform law of the independent seed . The construction uses the same inputs for every evaluation radius.

    Retain the choices The compact-uniform conclusion of Theorem 3 states that, for every nonempty compact , Its exponent conclusions give, throughout , and, when , Finally, its procedure-wise converse supplies, for every , , , and , including procedures using independent randomization.

  2. By Lemma 3, the concrete engine is admissible. By the first assertion of Lemma 4, the dyadic-floor naming policy is admissible. Specialize the universal conclusion above to this pair. The resulting procedure is exactly as defined in Definition 19. Hence, for every and , and every sample and seed produces a closed interval with ordered rational endpoints in . For every , This specialization preserves the constants chosen above and completes the concrete attainment assertion together with the universal assertions.

∎

References

  • Gao, Zijun and Hastie, Trevor (2025). Estimating heterogeneous treatment effects for general responses. Biometrics. doi
  • Robins, James M. and Tchetgen Tchetgen, Eric and Li, Lingling and van der Vaart, Aad (2009). Semiparametric minimax rates. Electronic Journal of Statistics. doi
  • Jin, Jikai and Mackey, Lester and Syrgkanis, Vasilis (2025). It's hard to be normal: The impact of noise on structure-agnostic estimation. Advances in Neural Information Processing Systems. arXiv
  • Tan, Zhiqiang (2019). On doubly robust estimation for logistic partially linear models. Statistics \& Probability Letters. doi
  • Liu, Molei and Zhang, Yi and Zhou, Doudou (2021). Double/debiased machine learning for logistic partially linear model. The Econometrics Journal. doi
  • McClean, Alec and Balakrishnan, Sivaraman and Kennedy, Edward H. and Wasserman, Larry (2026). Double cross-fit doubly robust estimators: Beyond series regression. Journal of the Royal Statistical Society: Series B. doi
  • Cai, T. Tony and Low, Mark G. (2004). An adaptation theory for nonparametric confidence intervals. The Annals of Statistics. doi
  • Jin, Jikai and Syrgkanis, Vasilis (2026). Sharp structure-agnostic lower bounds for general linear functional estimation. . arXiv
  • Liu, Lin and Mukherjee, Rajarshi and Robins, James M. and Tchetgen Tchetgen, Eric (2021). Adaptive estimation of nonparametric functionals. Journal of Machine Learning Research. arXiv
  • Zhang, Yulin and Liu, Lin and Zhang, Zheng (2026). Higher-order debiased estimators for general treatment models. . arXiv
  • Mantel, Nathan and Haenszel, William (1959). Statistical aspects of the analysis of data from retrospective studies of disease. Journal of the National Cancer Institute. doi
  • Rubin, Donald B. (1974). Estimating causal effects of treatments in randomized and nonrandomized studies. Journal of Educational Psychology. doi
  • Rosenbaum, Paul R. and Rubin, Donald B. (1983). The central role of the propensity score in observational studies for causal effects. Biometrika. doi
  • Greenland, Sander and Robins, James M. and Pearl, Judea (1999). Confounding and collapsibility in causal inference. Statistical Science. doi
  • Tchetgen Tchetgen, Eric J. and Robins, James M. and Rotnitzky, Andrea (2010). On doubly robust estimation in a semiparametric odds ratio model. Biometrika. doi
  • Tchetgen Tchetgen, Eric J. (2013). On a closed-form doubly robust estimator of the adjusted odds ratio for a binary exposure. American Journal of Epidemiology. doi
  • McGrath, Sean and Mukherjee, Rajarshi (2026). Nuisance function tuning and sample splitting for optimally estimating a doubly robust functional. . arXiv
  • Low, Mark G. (1997). On nonparametric confidence intervals. The Annals of Statistics. doi