Formalization: Honest Confidence Intervals for Homogeneous Causal Log Odds under Low Smoothness
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs. Note: this index was generated at a different commit than the paper's audited pin (1efc342) — statements may have moved since the audit.
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Basic 56 declarations Concrete binary records, continuous conditional cells, the prescribed native-logit model, randomized interval procedures, and the expected-length objective.
Continuous observed laws and honest interval decisions
Concrete binary records, continuous conditional cells, the prescribed native-logit model, randomized interval procedures, and the expected-length objective. The Hölder seminorm is extended nonnegative, so a continuous non-Hölder function has infinite seminorm rather than the junk value of an unbounded real supremum.
[The covariate interval.
The concrete observed record space.
First coordinate.
Binary treatment as a real.
Definition (Lean source)
Binary outcome as a real.
Definition (Lean source)
Public uniform design, as Lebesgue measure pulled back to the unit interval.
Logistic map.
Definition (Lean source)
Log odds, used only at interior probabilities.
Definition (Lean source)
Reconstruct the joint law from its covariate law and conditional cell functions.
An ambient probability law includes its unique continuous interior conditional cells.
Definition (Lean source)
Public exponent domain.
Definition (Lean source)
The propensity, pinned to the law.
Arm risks, pinned to the conditional table.
Native propensity logit.
Definition (Lean source)
Native prognosis logit.
Definition (Lean source)
Effect is defined literally at covariate zero.
Definition (Lean source)
Conditional cells expressed through propensity and arm risks.
Definition (Lean source)
Conditional outcome mean.
Expected conditional covariance under uniform design.
Definition (Lean source)
Integrated off-diagonal product.
Definition (Lean source)
Public denominator floor.
Definition (Lean source)
The generic Hölder exponent has precisely the paper's domain.
Definition (Lean source)
The generic real function on the covariate interval is continuous.
Definition (Lean source)
Extended Hölder seminorm, including infinite values. Its paper domain is HolderExponentDomain γ together with ContinuousFunctionDomain f.
Known uniform covariate design.
Definition (Lean source)
A single homogeneous conditional log-odds coefficient.
Definition (Lean source)
Compact scalar effect envelope.
Definition (Lean source)
Propensity native-logit envelope.
Definition (Lean source)
Prognosis native-logit envelope.
Definition (Lean source)
Propensity native-logit Hölder radius.
Definition (Lean source)
Prognosis native-logit Hölder radius.
Definition (Lean source)
The public evaluation-radius parameter has exactly the frozen range.
Definition (Lean source)
Radius restriction used only for length evaluation.
Definition (Lean source)
The unrestricted homogeneous logistic class.
Definition (Lean source)
Exactly the seven prescribed law properties.
Definition (Lean source)
The radius slice inherits the whole model and adds only the effect bound.
Definition (Lean source)
An interval encoded by endpoints and their inclusion flags.
All nonempty connected Borel intervals in the effect region.
Definition (Lean source)
Interval membership, respecting endpoint inclusion.
Definition (Lean source)
Interval length is supremum minus infimum.
Definition (Lean source)
Exactly n original observations and an independent uniform seed.
Reuse the substrate's finite iid law and tensor the seed.
Definition (Lean source)
Borel interval procedures, including randomized procedures.
Definition (Lean source)
Global finite-sample ninety-percent coverage.
Definition (Lean source)
Honest procedures are bundled through their sole member property.
Definition (Lean source)
Expected length, with the seed included.
Definition (Lean source)
Worst-case expected length on the prescribed radius slice.
Definition (Lean source)
Infimum of worst-case length over globally honest procedures.
Definition (Lean source)
Numerator rate exponent.
Definition (Lean source)
Effect-scaled denominator rate exponent.
Definition (Lean source)
Explicit diagnostic profile.
Every encoded interval has nonnegative length. the stated conclusion holds.
Formal statement
Proof (Lean source)
Expected interval length is nonnegative under any observed law. the stated conclusion holds.
Formal statement
Proof (Lean source)
The worst-case length is nonnegative, including an empty radius slice. the stated conclusion holds.
Formal statement
Proof (Lean source)
Any honest procedure upper bounds the minimax objective. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
An all-procedure lower bound transfers to the minimax objective. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Defs.Calibration 52 declarations Local root selectors are totalized outside their brackets.
Scalar calibrations, continuous sign priors, and full-data extensions
Local root selectors are totalized outside their brackets. Probability laws are constructed from the displayed cells, with a fixed harmless default outside the positive-cell neighbourhood; neighbourhood validity is a theorem obligation.
[Uniform design is a probability measure. the stated conclusion holds.
Formal statement
Proof (Lean source)
The anonymous instance result states the corresponding mathematical identity, bound, or structural property.
Definition (Lean source)
Continuous, normalized, strictly interior conditional cells.
Marginal of the explicitly constructed cell law. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
The law of valid cells is a probability law. Under the stated assumptions.
Formal statement
Proof (Lean source)
The explicitly constructed law has the required disintegration identity. Under the stated assumptions.
Formal statement
Proof (Lean source)
Uniform laws have full support. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Pack the concrete cell construction into the ambient carrier.
Definition (Lean source)
A fixed interior table for totalization outside the calibration neighbourhood. the stated conclusion holds.
Formal statement
Proof (Lean source)
Total cell-law constructor; on valid cells it is literally the given cell law.
Definition (Lean source)
Smooth exponential divided difference through zero.
Definition (Lean source)
Binary-table covariance branch with the prescribed positive square root.
Smooth normalized covariance branch.
Definition (Lean source)
A sign as a real number.
Definition (Lean source)
Two auxiliary signs at a within-cell coordinate.
Expectation over the two auxiliary independent fair signs.
Normalized mixed-prior root equation.
Definition (Lean source)
Choose the local mixed root in its prescribed bracket, otherwise use one.
Definition (Lean source)
Logistic risk shift.
Fair comparator effect.
Numerator of the normalized fair equation.
Definition (Lean source)
Double-integral Taylor form is the removable extension, including both zero axes.
Definition (Lean source)
Choose the local fair centering root; outside its neighbourhood use 2/5.
Definition (Lean source)
All seven calibration maps, with their literal defining formulas.
Definition (Lean source)
Cell number, taking the left cell at the rightmost endpoint.
Within-cell coordinate.
Endpoint signs are extended by zero-index fallback only for k=0.
Definition (Lean source)
Continuous shared-endpoint sign field.
A four-cell table from margins and covariance.
Definition (Lean source)
Mixed-prior conditional cell formula.
Definition (Lean source)
Fair random and deterministic-comparator cells.
Definition (Lean source)
Construct the ambient mixed law from its explicit conditional cells.
Definition (Lean source)
Construct a fair random law from its explicit cells.
Definition (Lean source)
Deterministic comparator, whose cells do not depend on the supplied sign vector.
Definition (Lean source)
Uniform finite mixture with signs drawn once for the whole iid sample.
Mixed original-record mixture.
Fair original-record mixture.
Definition (Lean source)
Both mixed and fair prior experiments contain exactly n original records.
Definition (Lean source)
Full data contain two binary potential outcomes and a treatment.
Potential control outcome.
Definition (Lean source)
Potential treated outcome.
Definition (Lean source)
Observation by literal consistency.
Definition (Lean source)
Binary law at a success probability.
A coupling is admissible exactly when both conditional margins are the law's arm risks.
The treatment probability is strictly interior by cell normalization. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
An interior Bernoulli parameter defines a probability measure. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Conditional treatment kernel is measurable. the documented result
Formal statement
Proof (Lean source)
Treatment is drawn independently of the potential outcomes given X.
Definition (Lean source)
The conditional factorization defining exchangeability.
The conditional product is the fibre of the sequential kernel composition. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The full conditional laws of an admissible coupling form a measurable kernel. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
X uniform, the supplied potential-outcome coupling, then independent Bernoulli treatment.
Definition (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Defs.CalibrationRegularity 9 declarations Fully substituted local cells and the closed parameter regions used for smoothness and bounds of all fixed derivative orders.
Calibration regularity specifications
Fully substituted local cells and the closed parameter regions used for smoothness and bounds of all fixed derivative orders.
Actual local four-cell formulas, with the root fully substituted.
Definition (Lean source)
Actual local fair-cell formulas, including spatial centering and comparator effect.
Definition (Lean source)
Closed mixed-amplitude neighbourhood, including the full spatial coordinate range.
Closed fair-amplitude neighbourhood, including zero effect and zero amplitude.
Both roots and all fully substituted local cell formulas are smooth.
Definition (Lean source)
Every fixed derivative order is uniformly bounded; the order is not truncated at two.
Definition (Lean source)
The literal mixed selector is the unique zero in its prescribed open bracket.
Definition (Lean source)
The literal fair selector lies in one fixed narrow bracket and is its unique zero; it also lies in the existing selector bracket.
Definition (Lean source)
Absolute signed branch radii larger than the derivative-bound radius, one fixed fair bracket, and open neighborhoods of the full closed parameter regions. The ambient open sets include signed effects across zero and neighborhoods of both spatial endpoints; all cells have their selectors fully substituted. The fair equation itself is smooth on an ambient open set containing the entire fair core and centered margin bracket, and agrees with the normalized numerator off the axes throughout that core, for every margin in the bracket.
Definition (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Defs.Engine 27 declarations Primitive image and excess contracts are distinct from statistical budget conclusions.
Rational engines and Borel dyadic naming policies
Primitive image and excess contracts are distinct from statistical budget conclusions. Bounded stateful rational register programs certify the recurrence requirement; arbitrary operation-count metadata alone does not certify a computation.
Instructions of a finite rational register machine. Registers carry state between steps; comparisons may branch or jump back to an earlier instruction. Integer operations act on the nonnegative part of the floor, except floor and ceil, which retain the sign.
Definition (Lean source)
A fixed finite instruction list, with no access to real inputs or external oracles.
Definition (Lean source)
Program counter, rational registers, and halt flag.
Definition (Lean source)
Initialize registers from the supplied rational arguments, and all others to zero.
Definition (Lean source)
One stateful rational step. Falling off the finite code also halts.
Definition (Lean source)
General state-carrying iteration for a specified public number of steps. In particular, repeated natPow instructions can generate towers of input-dependent height.
Definition (Lean source)
Allowable public iteration-count functions are all total functions of rational arguments computed by a fixed finite rational register program. The computation of this bound must itself halt on every input; no elementary-growth restriction is imposed.
Definition (Lean source)
A general bounded stateful rational program with its specified public bound. Registers zero and one are the returned endpoints. The bound and program are fixed independently of exponents, samples, laws, naming policies, and evaluation radii.
Definition (Lean source)
Execute the certified finite state recurrence and read its rational endpoints.
Definition (Lean source)
Endpoint ordering is enforced without any real input.
Definition (Lean source)
Fixed primitive index.
Definition (Lean source)
Independently fixed deterministic maps over rational data only.
Definition (Lean source)
Precision error.
Definition (Lean source)
Image containment and outward endpoint excess for a monotone primitive.
Definition (Lean source)
Every primitive is a general bounded stateful rational program, with a public iteration bound computed solely from precision, rational range bounds, and the integer base when present. The finite register language permits unrestricted state-carrying loops within that bound, including non-elementary output growth.
Definition (Lean source)
Primitive contracts and finite rational computation, with no budget conclusion.
Definition (Lean source)
A name is a precision-indexed rational interval.
Definition (Lean source)
Dyadic rational endpoint.
Definition (Lean source)
Validity at every precision, with nesting and literal containment.
Definition (Lean source)
Public names are fixed without the sample; covariate names may depend on it.
Definition (Lean source)
Every selected name is valid, and every rational response is Borel.
Definition (Lean source)
Ordered endpoints of the dyadic-floor response. the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact prescribed dyadic-floor name, including dyadic inputs.
Definition (Lean source)
One concrete policy, with the literal dyadic-floor responses.
Definition (Lean source)
The literal floor boxes contain their input with the prescribed width. the stated conclusion holds.
Formal statement
Proof (Lean source)
At each fixed precision the two rational floor endpoints are Borel. the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit floor policy meets all validity and Borel contracts. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Defs.FrontierSpecifications 6 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
Defs/FrontierSpecifications
Paper-owned scaffold obligations; proofs are filled in Stage 3.
The two explicit radius-elbow identities, with positivity and shared-boundary agreement.
Definition (Lean source)
Compact-uniform bounds, expressed as the actual infimum/supremum conditions.
The all-radius expected-length comparison for one literal implementation.
Definition (Lean source)
The operational guarantees are properties of the actual supplied-engine output.
Definition (Lean source)
Concrete sequence uses precisely the certified concrete engine and the floor policy.
Definition (Lean source)
Parameter-independent universal generalization of the sharp comparison and output guarantees.
Definition (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Defs.Projection 8 declarations Cosine projections and original-record ordered-pair statistics
Cosine projections and original-record ordered-pair statistics
Cosine basis with the constant frequency separated.
Inner product against the public uniform design.
Definition (Lean source)
Rank-k cosine projection.
Definition (Lean source)
Projection kernel.
Borel marks valued in the unit interval.
Definition (Lean source)
Conditional mean computed from the actual four-cell kernel.
Definition (Lean source)
Ordered distinct pairs, with the asymmetric marked kernel.
Definition (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Defs.Upper 40 declarations One retained rank pair drives both exact coordinates and the literal rational expression tree.
Fixed-budget represented upper intervals
One retained rank pair drives both exact coordinates and the literal rational expression tree. Ideal real endpoints and their evaluated enclosures are separate.
[Exact interval intersection; an empty intersection is reported.
Definition (Lean source)
A successful intersection is contained in its second input interval. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Exact minimum range.
Definition (Lean source)
Exact maximum range.
Definition (Lean source)
Domain-checked division.
Definition (Lean source)
Full public effect box.
Definition (Lean source)
Public rank budget, computed with integer comparisons.
Definition (Lean source)
Public endpoint budget.
Literal engine rank-target enclosures.
Definition (Lean source)
Ceiling of each upper enclosure endpoint, fixed before sampling.
Definition (Lean source)
Exact covariance coordinate statistic at the retained rank.
Exact denominator statistic at the retained rank.
Both statistics use exactly the previously selected rank pair.
Definition (Lean source)
Public variance radius.
Definition (Lean source)
Clipping as literal maximum and minimum.
Joint odds inversion with the public effect clipping.
The ideal exact-real endpoint expressions.
Definition (Lean source)
Finite expression syntax with matching real and rational-box semantics.
Definition (Lean source)
Exact-real semantics.
Definition (Lean source)
Literal structural box evaluation with the supplied engine and one precision.
Definition (Lean source)
A literal finite expression sum.
Cosine basis expression at input covariate i.
Projection kernel expression.
Definition (Lean source)
The full original-record statistic as a finite expression.
Definition (Lean source)
Literal numerator and denominator expressions using exact binary labels.
Definition (Lean source)
Literal joint-inversion expression.
The displayed finite expression tree, retaining the rank-step integers.
Definition (Lean source)
Endpoint-step inputs are queried once at the public endpoint precision. The supplied boxes enter the expression tree directly, without domain narrowing.
Definition (Lean source)
Literal endpoint enclosures.
Definition (Lean source)
Outward rational endpoints, with full-box totalization on invalid inputs.
Definition (Lean source)
The final intersection or full-box fallback keeps both endpoints in the effect box. the stated conclusion holds.
Formal statement
Proof (Lean source)
The totalized rational output always defines a nonempty closed effect interval. the stated conclusion holds.
Formal statement
Proof (Lean source)
Closed interval carrier for the literal rational output.
Definition (Lean source)
A finite response code determines every subsequent rational computation. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
Any union of fibers of a measurable countable response code is measurable. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Borelness follows from finite rational computations and the Borel supplied policy. Under the stated assumptions.
Formal statement
Proof (Lean source)
The literal represented algorithm, with no radius or nuisance input.
Definition (Lean source)
Canonical upper handle for the literal fixed-budget represented procedure.
Definition (Lean source)
Sharp profile candidate, defined independently of the engine and policy.
Definition (Lean source)
The rate and the actual supplied-engine interval family.
Definition (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CalibratedDensityDerivatives 5 declarations Affine amplitude slices do not increase derivative norms.
Amplitude derivative envelopes for calibrated densities
Affine amplitude slices do not increase derivative norms. The compact local cell envelopes therefore control the fully substituted density formulas.
[Restricting a smooth local cell to a contractive affine amplitude slice cannot increase the norm of any fixed-order derivative. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The mixed amplitude plane is a contractive slice of the full local parameter space, with the spatial coordinate held fixed. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The fair amplitude line is a contractive slice, with effect and spatial coordinate held fixed. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Passing from a cell probability to its uniform-label relative density multiplies every amplitude derivative envelope by four. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Compact local calibration boxes give a common finite envelope for the first two derivatives of both relative-density amplitude slices. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CalibratedEffects 6 declarations Positive four-cell odds identify the native logit contrast.
Homogeneous effects of the calibrated laws
Positive four-cell odds identify the native logit contrast. The mixed covariance branch and the fair risk shift therefore give the effects of the actual laws, provided their continuous cell tables are valid.
Positive cells turn their odds ratio into the native conditional logit contrast. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A common conditional cell odds coefficient is the law's scalar effect and makes its native logistic regression homogeneous. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Valid totalized cells retain the literal supplied table. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Logistic risk shifting multiplies the risk odds by the exponential effect. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Every valid fair table has its prescribed scalar effect, including the comparator's effect, and is homogeneous at every covariate. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Every valid mixed table has the null or calibrated effect, and its logit coefficient is homogeneous throughout the covariate interval. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CalibratedHolderModulus 4 declarations The roadmap's two-scale modulus argument turns a global Lipschitz bound and an oscillation bound into the exact prescribed Hölder radius.
Global Hölder modulus for calibrated supports
The roadmap's two-scale modulus argument turns a global Lipschitz bound and an oscillation bound into the exact prescribed Hölder radius. It includes exponent one and requires no derivative matching at cell endpoints.
[Below unit scale, the linear modulus is bounded by every legal Hölder power; above unit scale, the constant modulus is bounded by that power. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
A Lipschitz modulus at cell scale and a uniform oscillation modulus give an exponent-uniform Hölder bound after cancelling the rate-scaled amplitude. the documented result Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Remaining construction obligations before applying the global modulus argument: the five non-Hölder model properties and the two scale bounds for each native logit. These are proof obligations, not additional model premises.
Definition (Lean source)
The two-scale native-logit bounds discharge both exact Hölder radii of the paper model, uniformly over the public exponent domain. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CalibratedModelProperties 13 declarations The explicit cells give uniform covariate design, homogeneous scalar effects, and the required effect envelopes.
Basic model properties of the calibrated constructions
The explicit cells give uniform covariate design, homogeneous scalar effects, and the required effect envelopes. Fair treatment is exactly balanced. Only native logit envelopes and spatial scale bounds remain in the reduced assembly.
[Totalization retains the public uniform design, even on fallback inputs. the stated conclusion holds.
Formal statement
Proof (Lean source)
Fair tables have exactly balanced treatment, including totalization fallback. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Exact fair treatment balance makes the native propensity logit zero. Under the stated assumptions.
Formal statement
Proof (Lean source)
Fair supports satisfy the propensity envelope and both spatial scale bounds at every exponent and rank, because their propensity logit vanishes. the documented result Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
[The mixed effect from cell odds stays in the model envelope on the signed calibration square; uniform design and homogeneity hold for every valid table. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Fair effects and comparator effects lie in the model envelope, as follows from exact cell odds and the calibrated comparator range. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Interior probabilities between one third and two thirds have native logit magnitude at most one, using the two elementary logarithm bounds. the documented result Under the stated assumptions.
Proof (Lean source)
Small covariance and centered margins keep the table's control risk between one third and two thirds. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Both mixed native logit envelopes follow from the centered margins and small calibrated covariance on the fixed signed support square. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The remaining mixed spatial scale bounds after design, homogeneous effects, and all three pointwise envelopes have been proved from explicit cells.
Definition (Lean source)
Native-logit spatial bounds combine with independently proved mixed cell-law properties and envelopes to feed the global Hölder assembly. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[For fair treatment, only the prognosis envelope and its two spatial scale bounds remain; the propensity logit is already identically zero.
Definition (Lean source)
The actual fair tables' balanced treatment supplies every propensity obligation, leaving just the native prognosis bounds for Hölder assembly. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CalibratedPriorTesting 2 declarations The mixed null prior belongs to every radius slice.
Testing bounds from the calibrated mixed and fair supports
The mixed null prior belongs to every radius slice. The random fair prior with input effect r/2 also belongs to the slice. Their original-record Hellinger budgets imply length lower bounds through the finite-prior reduction.
[The null mixed support and the homogeneous alternative yield a lower bound proportional to the actual mixed amplitude product. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The random fair prior is the evaluation prior, even though its effect exceeds the comparator's effect. The comparator is a constant finite prior. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ComponentPriorRestriction 10 declarations Averaging a likelihood over all endpoint signs equals averaging over the signs owned by its record block.
Restricting hidden sign priors to one component
Averaging a likelihood over all endpoint signs equals averaging over the signs owned by its record block. This bridge transfers exact singleton matching to component densities without revealing signs or assuming record independence.
[The uniform prior on all signs has the uniform marginal on any ownership fiber. A function depending only on that fiber has the same two averages. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
A block product depending only on its owned signs can use the full prior, which makes the existing whole-prior cancellation lemmas directly applicable. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Exact matching of single-record averages removes every block of at most one record, including the empty block used for unowned endpoint signs. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Endpoint ownership transfers the full sign prior to a selected component for literal mixed cells. Totalization is handled separately by cell validity. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The fair component uses the same hidden-prior restriction as the mixed component, uniformly in the effect and signed amplitude. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Validity on the support neighborhood transfers sign restriction to the actual mixed record density, including its law constructor. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Validity on the support neighborhood transfers sign restriction to the actual fair record density, with every root already substituted. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Empty and singleton components have identical actual mixed likelihoods, by the support theorem's exact singleton matching and hidden-prior restriction. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact singleton matching also removes every fair component of at most one original record; its comparator average is a constant-prior average. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The record fiber is empty for unowned signs and otherwise has exactly the support cardinality of its graph component. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CoordinateBias 7 declarations Cauchy–Schwarz for the uniform design converts the verified constant-five projection approximation into residual-product bounds.
Hölder approximation bounds for the coordinate biases
Cauchy–Schwarz for the uniform design converts the verified constant-five projection approximation into residual-product bounds. Native-logit regularity supplies the off-diagonal Hölder radii, giving the exact denominator constant.
For continuous functions, the extended norm has the ordinary integral representation. Under the stated assumptions.
Formal statement
Proof (Lean source)
The real inner product is bounded by the product of the two finite L2 norms. Under the stated assumptions.
Formal statement
Proof (Lean source)
The finite projection of any function is continuous. Under the stated assumptions.
Formal statement
Proof (Lean source)
A real Hölder radius bounds the real L2 approximation error. Under the stated assumptions.
Formal statement
Proof (Lean source)
Two real Hölder radii give the product approximation bound with constant twenty-five. Under the stated assumptions.
Formal statement
Proof (Lean source)
The off-diagonal residual has precisely the paper's constant twenty-five bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
The sharper marginal radius gives a numerator residual constant below eight. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CoordinateRegularity 10 declarations The quarter-Lipschitz logistic map transports the model's native Hölder radii to propensity and arm risks.
Native-logit Hölder control of the observable cells
The quarter-Lipschitz logistic map transports the model's native Hölder radii to propensity and arm risks. On the unit covariate interval, the smoother propensity exponent can be lowered to the prognosis exponent. Product bounds then give the unit Hölder radii of both off-diagonal cells used in the bias proof.
[The logistic derivative is globally bounded by one quarter. the stated conclusion holds.
Proof (Lean source)
A finite extended Hölder radius gives its pointwise real modulus. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
A pointwise modulus bounds the extended Hölder seminorm. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Hölder powers decrease with the exponent on the unit covariate interval. Under the stated assumptions.
Formal statement
Proof (Lean source)
Native propensity regularity is transported through the logistic map. Under the stated assumptions.
Formal statement
Proof (Lean source)
Both arm risks inherit the same prognosis Hölder modulus; the effect is constant. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Products of probability factors have the sum of their two moduli. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
Each off-diagonal cell has unit prognosis-exponent Hölder radius. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The homogeneous arm-risk gap is bounded by one quarter of the scalar effect. Under the stated assumptions.
Formal statement
Proof (Lean source)
The marginal outcome mean has the sharper nine-sixteenths Hölder radius. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CoordinateVariance 15 declarations The empirical mean uses independent original records.
Coordinate mean identities and variance bounds
The empirical mean uses independent original records. The projection statistic uses the sharp order-two Hoeffding bound; adding the independent seed preserves variance. Together these give the two public coordinate variance radii. Disintegration also identifies both biases with projection residual inner products.
[Both binary marks are continuous on the original record space. The stated conclusion follows.
Formal statement
Proof (Lean source)
The outcome mark is continuous on the original record space. The stated conclusion follows.
Formal statement
Proof (Lean source)
Finite cosine statistics are continuous functions of the original sample. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The two coordinate estimates have finite second moments, including the seed. the stated conclusion holds.
Formal statement
Proof (Lean source)
Continuous marks give a square-integrable finite projection statistic. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Tensoring the unused independent seed preserves the sharp projection variance. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Independence of the original records gives the unit-range empirical mean variance bound used for the numerator coordinate. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Nonnegativity of the sum variance bounds the variance of a difference, without requiring the two coordinates to be independent. the documented result Under the stated assumptions.
Proof (Lean source)
Both exact coordinate estimates obey the prescribed public variance radius. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Integrating a statistic that ignores the independent probability seed gives its original finite-sample expectation. the documented result
Formal statement
Proof (Lean source)
The seed-free empirical mean has the original one-record expectation. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Disintegration identifies the conditional treatment mean with propensity. Under the stated assumptions.
Formal statement
Proof (Lean source)
Disintegration identifies the conditional outcome mean with the marginal risk. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The two off-diagonal marks have exactly the model's off-diagonal cell means. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The coordinate biases are precisely the two projection residual inner products; no nuisance smoothness or approximation premise is used in these identities. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.CosProgram 13 declarations The fixed program computes the midpoint polynomial by the successive-term recurrence, sorts its scalar endpoints, and enlarges by the input half width.
Finite register certificate for the prescribed cosine routine
The fixed program computes the midpoint polynomial by the successive-term recurrence, sorts its scalar endpoints, and enlarges by the input half width.
[The next cosine term is obtained by the prescribed rational multiplier. the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite midpoint cosine program, including the exact prescribed truncation count.
Definition (Lean source)
Registers at the head of the cosine term loop.
Definition (Lean source)
Initialization on arbitrary rational inputs clamps the precision to a natural number. the stated conclusion holds.
Formal statement
Proof (Lean source)
Each nine-instruction loop block adds one term and advances its multiplier. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
At zero count the exit block returns the literal scalar sorting and width enlargement. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Iteration exhausts the prescribed term counter before executing the exit block. Under the stated assumptions.
Formal statement
Proof (Lean source)
The total public step count includes initialization, each term, and clipping.
A fixed straight-line program computes the public fuel from the same input bounds.
Definition (Lean source)
The cosine fuel is itself a total finite rational register computation. the stated conclusion holds.
Formal statement
Proof (Lean source)
The publicly bounded cosine computation halts on every rational input list. the stated conclusion holds.
Formal statement
Proof (Lean source)
Certified register implementation of the midpoint cosine routine.
Definition (Lean source)
The finite recurrence returns exactly the concrete engine's cosine interval. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.EndpointCoordinates 9 declarations The original-record ordered-pair expression propagates kernel widths through exact binary marks and exact normalization.
Literal coordinate enclosures
The original-record ordered-pair expression propagates kernel widths through exact binary marks and exact normalization. The empirical mean is rational and exact, so both coordinate expressions inherit the kernel width bound without a sample size loss. These are bounds on the actual expression tree.
Finite expression sums preserve containment and add width bounds for any index type. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Multiplication by an exact nonnegative rational scales the width exactly. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The filtered list in the literal statistic enumerates precisely the ordered distinct pairs. the stated conclusion holds.
Formal statement
Proof (Lean source)
There are exactly n(n-1) ordered distinct pairs, including the small sample cases. the stated conclusion holds.
Formal statement
Proof (Lean source)
Normalizing the actual ordered-pair sum cancels the pair count in the width bound. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The binary-label coordinate trees terminate, contain the exact sample coordinates, and inherit the kernel width bounds since the empirical mean is evaluated exactly. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
A finite list of successful input queries evaluates to the list of their selected boxes. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[All literal endpoint inputs are available at the prescribed precision, with the supplied raw covariate boxes at their exact input positions. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[At the actual endpoint budget and with the actual naming policy, both literal coordinate evaluations succeed with the roadmap's width bounds. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.EndpointQuotients 18 declarations The denominator floor controls both reciprocal magnitudes and reciprocal widths.
Literal quotient widths
The denominator floor controls both reciprocal magnitudes and reciprocal widths. The four-corner product estimate then bounds the actual quotient evaluation, including numerator boxes that straddle zero.
A denominator above the public floor has bounded reciprocal endpoints and width. Under the stated assumptions.
Formal statement
Proof (Lean source)
Exact rational quotient evaluation preserves containment and has the roadmap width bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Width contraction for logarithms on the public positive argument range. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The two clipping exponentials stay strictly inside the public argument range. the stated conclusion holds.
Proof (Lean source)
The literal exponential boundary boxes have two-error widths and positive public bounds. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
A successful positive argument produces a logarithm box with twice its input width plus two errors. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The literal clipping and logarithm tree terminates and propagates the quotient width. Under the stated assumptions.
Formal statement
Proof (Lean source)
The exact cosine kernel has the roadmap magnitude envelope. Under the stated assumptions.
Formal statement
Proof (Lean source)
Normalization by the number of distinct pairs preserves the kernel magnitude bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
The covariance coordinate is bounded by one plus twice its retained rank. Under the stated assumptions.
Formal statement
Proof (Lean source)
The variance radius and its square root have elementary rank-dependent envelopes. Under the stated assumptions.
Formal statement
Proof (Lean source)
The exact numerator radius obeys the roadmap magnitude bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
Containment and width turn an exact magnitude bound into endpoint magnitude bounds. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The public endpoint budget controls the full quartic precision product. the stated conclusion holds.
Formal statement
Proof (Lean source)
Every coefficient below the quartic budget has a precision product at most one. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The endpoint budget pays for coordinate widths, positive log arguments, and final widths. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Both actual numerator corners have bounded magnitudes and the roadmap widths. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
At the endpoint budget every inversion corner has width at most one over sample size. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.EndpointRadii 15 declarations Negative powers on the public exponent rectangle have derivative bounded by the integer base.
Literal endpoint radius enclosures
Negative powers on the public exponent rectangle have derivative bounded by the integer base. Primitive endpoint excess and exact scaling then give the two bias-and-noise radius widths in the fixed-budget roadmap.
Negative exponent ranges have variation at most the base times their width. Under the stated assumptions.
Formal statement
Proof (Lean source)
The power primitive adds at most two endpoint errors on a negative exponent box. Under the stated assumptions.
Formal statement
Proof (Lean source)
The variance quantity in the literal radius tree is an exact nonnegative rational. Under the stated assumptions.
Formal statement
Proof (Lean source)
An exact nonnegative input has a square-root enclosure of width at most two errors. Under the stated assumptions.
Formal statement
Proof (Lean source)
A successful power expression and its exact noise term assemble a scaled radius. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The endpoint precision bounds the positive exponent overhang even after multiplication by either retained rank. the documented result
Formal statement
Proof (Lean source)
A precision-sized positive overhang leaves the integer-base derivative bound unchanged when the rank times the precision error is at most one sixteenth. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The primitive endpoint errors add twice the precision to the raw power range. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The raw power expression and exact noise term assemble the same scaled radius. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Successful endpoint queries retain the raw public exponent boxes with their containment, widths, and precision-sized overhang beyond the public rectangle. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The raw exponent trees remain in the primitive domain, with a two-error positive overhang. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The two bias-and-noise subtrees used verbatim by the literal endpoint expressions.
Definition (Lean source)
At the actual endpoint inputs both radius subtrees terminate and have the roadmap widths. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The literal denominator clipping is safe for division and preserves the incoming width. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Both literal denominator corners stay positive and have the roadmap's joint width. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.EndpointRanges 18 declarations Exact minimum and maximum ranges preserve containment and the larger input width.
Range operations for the fixed endpoint budget
Exact minimum and maximum ranges preserve containment and the larger input width. Product ranges obey the cross-product variation inequality used in the endpoint roadmap. These estimates concern literal rational operations, not ideal ranges.
[Ordered input endpoints remain ordered after taking either minimum or maximum. the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact minimum and maximum ranges contain the corresponding real operations. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Minimum and maximum ranges have width at most the larger input width. the stated conclusion holds.
Formal statement
Proof (Lean source)
Inserting the cross product bounds product variation by two coordinate variations. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Two points of a rational range differ by at most its width. Under the stated assumptions.
Formal statement
Proof (Lean source)
A uniform magnitude bound on both endpoints bounds every point of the range. Under the stated assumptions.
Formal statement
Proof (Lean source)
The literal four-corner product has the cross-product width bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
Uniform endpoint magnitudes multiply under the literal four-corner product. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Every admissible engine supplies a two-error-width pi box in [3,4]. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The cosine primitive encloses its exact image, stays in [-1,1], and adds only two precision errors to the argument width. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The square-root-of-two primitive has width at most two precision errors; when the error is at most one quarter its entire range has magnitude at most two. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Multiplication on the right by a nonnegative point scales both endpoints exactly. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The literal cosine basis tree terminates, contains its exact value, has magnitude at most two, and has width at most twenty times the index plus one precision errors, uniformly over engines and covariate enclosures. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A finite expression sum terminates and contains the exact sum whenever each summand does; its width is bounded by the sum of the summand width bounds. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual finite cosine-kernel expression terminates, encloses the exact projection kernel, and has width at most 160 k squared precision errors. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The prescribed endpoint precision is small enough for the square-root basis range bound, for every sample size and every selected pair of ranks. the documented result
Formal statement
Proof (Lean source)
Containment and width bound the overhang of an unchanged input box. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Intersecting a valid covariate name with the public unit interval succeeds, retains its exact covariate, and does not enlarge the name width. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.EngineRoutines 20 declarations The specified truncation counts, remainder brackets, binary integer-square-root recurrence and Machin formula define the witness; its contracts remain proof obligations.
The paper's explicit finite rational arithmetic routines
The specified truncation counts, remainder brackets, binary integer-square-root recurrence and Machin formula define the witness; its contracts remain proof obligations.
Exact dyadic rational error.
Definition (Lean source)
Bound for the exponential and cosine routines.
The specified polynomial length.
Definition (Lean source)
Exact exponential polynomial.
Definition (Lean source)
Scalar exponential enclosure with the prescribed positive floor.
Definition (Lean source)
Exact cosine polynomial.
Definition (Lean source)
Scalar cosine bracket, clipped to its range.
Definition (Lean source)
Rational range bound for the logarithm.
Exact atanh logarithm polynomial, with the specified count.
Definition (Lean source)
Positive-domain logarithm enclosure, totalized by a point outside the domain.
Definition (Lean source)
One binary integer-square-root step.
Definition (Lean source)
Exactly the public number of binary steps, by structural recursion.
Definition (Lean source)
The literal prescribed fixed-count integer-square-root algorithm.
Definition (Lean source)
Scalar dyadic square-root bracket.
Definition (Lean source)
The alternating arctangent polynomial.
Definition (Lean source)
Machin's fixed-count rational pi enclosure.
Definition (Lean source)
Monotone endpoint extension of a scalar routine.
Definition (Lean source)
Midpoint cosine, enlarged by half the argument width then intersected with [-1,1].
Definition (Lean source)
Scalar positive-integer-base power with the paper's internal precision.
Definition (Lean source)
The concrete independently fixed rational engine.
Definition (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ExpProgram 15 declarations Two copies of the successive-term loop evaluate the scalar endpoint brackets.
Register certificate for the prescribed exponential recurrence
Two copies of the successive-term loop evaluate the scalar endpoint brackets. The instruction count is a fixed rational computation of the public truncation counts.
[Successive terms multiply by the argument and divide by the next index. the stated conclusion holds.
Formal statement
Proof (Lean source)
The two scalar loops retain the original precision and right endpoint in spare registers.
Definition (Lean source)
The loop head records the partial sum, current term, counter, and untouched frame.
Definition (Lean source)
Initialization computes the prescribed count from any rational argument and precision. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Seven instructions add a term and advance the exponential recurrence. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
At zero count the scalar exit sorts its prescribed positive-floor bracket. Under the stated assumptions.
Formal statement
Proof (Lean source)
The fixed loop count exhausts all terms before the scalar exit. Under the stated assumptions.
Formal statement
Proof (Lean source)
The initial frame saves the right endpoint before the left scalar loop. the stated conclusion holds.
Formal statement
Proof (Lean source)
The two scalar loops have a public count determined by the input precision and endpoints.
Definition (Lean source)
Both endpoint loops return the literal endpoint extension, on every rational input list. the stated conclusion holds.
Formal statement
Proof (Lean source)
A straight-line register program computes the complete two-endpoint instruction count.
Definition (Lean source)
The step bound is itself computed by a total finite rational program. the stated conclusion holds.
Formal statement
Proof (Lean source)
The publicly bounded two-endpoint exponential program halts on every rational list. the stated conclusion holds.
Formal statement
Proof (Lean source)
Certified finite register implementation of exponential endpoint extension.
Definition (Lean source)
The register output agrees with the prescribed concrete exponential interval. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairAmbientSmoothness 3 declarations Compactness of the two integration coordinates preserves joint smoothness on one ambient neighborhood.
Ambient smoothness of the fair Taylor equation
Compactness of the two integration coordinates preserves joint smoothness on one ambient neighborhood. The scalar implicit theorem then gives one smooth branch on an open set, rather than order-dependent point neighborhoods.
[The analytic Taylor integrand remains smooth above a common ambient neighborhood of every point of the closed parameter box. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A single open domain of smoothness gives a single smooth implicit branch for every finite derivative order. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Smooth selected roots near a zero-amplitude point yield smooth actual fair cells nearby; the outer risk formulas have analytic ambient neighborhoods. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairAmplitudeSymmetry 6 declarations Sign symmetry transports through the numerator, its Taylor extension, and the literal selected root, including both amplitude axes.
Signed fair-calibration symmetry
Sign symmetry transports through the numerator, its Taylor extension, and the literal selected root, including both amplitude axes.
Symmetry of the two independent signs makes every transformed sign average even. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The deterministic fair comparator is even in the signed amplitude. the stated conclusion holds.
Formal statement
Proof (Lean source)
Reversing the amplitude reindexes the symmetric sign law in the fair numerator. the stated conclusion holds.
Formal statement
Proof (Lean source)
Two derivatives preserve evenness, including where the totalized derivative is zero. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The literal integral Taylor extension retains amplitude evenness on both axes. the stated conclusion holds.
Formal statement
Proof (Lean source)
Equal normalized equations give equal literal fair-root selectors. the stated conclusion holds.
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairCellSmoothness 9 declarations The literal fair selector stays in its interior bracket.
Smooth actual fair cells
The literal fair selector stays in its interior bracket. The comparator's positive logarithm arguments and the shifted-risk denominator therefore make the actual cell formulas smooth wherever the selected root is smooth. Compactness then bounds all fixed-order derivatives of these fully substituted formulas.
[The local sign interpolation is bounded on its entire real carrier. the stated conclusion holds.
Formal statement
Proof (Lean source)
Any nonnegative logistic shift has a positive denominator at a positive risk. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[A nonzero shifted-risk denominator makes the two-parameter risk map smooth. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual logarithmic comparator is smooth through both zero axes and on full neighborhoods of the endpoints of the prescribed effect interval. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual selected fair control risk remains interior before any smoothness of the selector is used. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Composing the smooth actual root with the interior risk maps proves smoothness of every actual fair cell, including the comparator cells. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The closed effect-amplitude-coordinate parameter region is compact. the stated conclusion holds.
Formal statement
Proof (Lean source)
Smoothness to every finite order uniformly bounds each fixed derivative on a compact parameter set; analyticity is not needed. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Root smoothness on neighborhoods of the closed region supplies both cell smoothness and all fixed-order bounds for the fully substituted roots and cells. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairCenterSlope 8 declarations Differentiating the cleared endpoint identity at the asymmetric center proves strict positivity of the actual normalized equation's center derivative.
Nonzero fair center slope over the full effect range
Differentiating the cleared endpoint identity at the asymmetric center proves strict positivity of the actual normalized equation's center derivative. The zero-effect extension handles the removable boundary without division.
[Differentiating the endpoint factorization at its center root gives a cleared derivative identity throughout the full effect range. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The fair equation's center derivative is strictly positive, including zero effect, at every point of the closed effect and position ranges. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Compactness in effect and position preserves the positive center slope on one absolute signed amplitude and center neighborhood. the documented result
Formal statement
Proof (Lean source)
The normalized fair equation is strictly increasing on a fixed center bracket for every allowed effect and all sufficiently small signed amplitudes. the documented result
Formal statement
Proof (Lean source)
Uniform continuity excludes every zero-amplitude noncenter root, even at the bracket endpoints, on a compact set away from the center. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A fixed center derivative neighborhood and compact exclusion of all other roots yield uniqueness on the original full selector bracket. the documented result
Formal statement
Proof (Lean source)
A positive center slope and exclusion of roots elsewhere remain valid on full parameter neighborhoods, including effect and position endpoints. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual fair selector is jointly smooth on full neighborhoods of the closed parameter region, uniformly over the complete prescribed effect range. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairComponentSupport 2 declarations The support theorem's smoothness and derivative envelope discharge the actual record inputs to the quadratic Taylor bound.
Fair component bounds from calibrated record support
The support theorem's smoothness and derivative envelope discharge the actual record inputs to the quadratic Taylor bound. Restricting the hidden sign prior then transfers that bound to each original-record component.
[Actual fair block likelihoods satisfy the quadratic Hellinger estimate using the jointly selected support radius and derivative envelope. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The uniform sign marginal on one component preserves the Taylor bound, with the exact number of original records in that component. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairDensityRanges 6 declarations The literal root bracket and the explicit effect bounds control every fair cell on a fixed signed amplitude neighborhood, without a smoothness assumption.
Fair four-cell density bounds
The literal root bracket and the explicit effect bounds control every fair cell on a fixed signed amplitude neighborhood, without a smoothness assumption.
[Endpoint signs have unit magnitude. the stated conclusion holds.
Formal statement
Proof (Lean source)
The shared endpoint sign field is bounded on every covariate. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
[A small nonnegative shift preserves a fixed interior risk interval. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The root bracket and small signed perturbation keep the fair control risk interior. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
All four literal fair cells have the required common density floor and ceiling. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Totalizing a bounded table preserves its density bounds, including the fallback table. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairEffectBounds 4 declarations The explicit comparator logarithms give a quadratic effect gap, uniformly through zero effect and zero amplitude, on the paper's fixed amplitude neighbourhood.
Quantitative separation of the fair comparator effect
The explicit comparator logarithms give a quadratic effect gap, uniformly through zero effect and zero amplitude, on the paper's fixed amplitude neighbourhood.
Reciprocal bounds for the two logarithms in the fair effect gap. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The exponential increment has the bounds used by the fair calibration roadmap. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The explicit fair comparator loses between three and six times the quadratic amplitude. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The fair comparator stays between half the input effect and the input effect. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairEndpointUniqueness 12 declarations Clearing the positive risk denominators factors the endpoint matching equation.
Uniqueness of the fair endpoint center
Clearing the positive risk denominators factors the endpoint matching equation. Its second factor is strictly negative throughout the prescribed bracket, so nonzero effect and amplitude force the literal selected root to be the center.
[The residual factor in endpoint matching is strictly negative throughout the fair bracket for every nonnegative exponential increment. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Clearing the endpoint risk denominators factors the exact matching residual, retaining the amplitude square needed for the removable extension. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The explicit log correction supplies the rational comparator odds after clearing its positive logarithm denominators. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The rational comparator odds and endpoint risk matching have only the asymmetric center as a bracket solution off the two removable axes. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact endpoint singleton matching identifies any bracket root with the fixed center whenever effect and amplitude are both nonzero. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The literal endpoint selector equals the center throughout the full effect range away from the removable axes. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The endpoint factorization survives Taylor normalization off the axes; the amplitude square cancels without changing the risk residual. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Continuity of the actual Taylor extension preserves the factored endpoint equation at zero amplitude, throughout the closed effect range. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The zero-amplitude normalized equation has a unique bracket root for the entire effect range; its position independence comes from unit sign variance. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual zero-amplitude selector is the fixed asymmetric center on the whole prescribed effect and spatial ranges. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Both spatial endpoint selectors equal the center, including effect and amplitude zero, uniformly on the complete prescribed effect range. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
At zero amplitude the normalized fair equation has strictly separated signs on the whole selector bracket, uniformly over the closed effect range. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairEquationContinuity 10 declarations Compact domination justifies continuity of both Taylor integrations.
Continuity of the normalized fair equation through its axes
Compact domination justifies continuity of both Taylor integrations. The exact endpoint numerator identity then extends to the actual normalized equation on both zero axes, providing genuine bracket roots for the literal selector.
A continuous family on a compact parameter set has a continuous unit-interval integral. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The compact box on which the fair Taylor equation is used.
Coordinate characterization of the closed Taylor box. the stated conclusion holds.
Formal statement
Proof (Lean source)
Compactness includes both removable axes and all spatial endpoints. the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual weighted Taylor integrand is smooth jointly in the parameters and its two integration coordinates on full neighborhoods of the closed box. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The double Taylor integral is jointly continuous through both axes. Compact bounds on the actual integrand justify both integrations. The stated conclusion follows.
Formal statement
Proof (Lean source)
Endpoint roots persist through zero effect for every nonzero signed amplitude. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The endpoint center solves the actual Taylor-normalized equation also on both removable axes, by joint continuity and the exact off-axis identity. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Every endpoint has an actual bracket root, with no off-axis restriction. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[At either spatial endpoint the literal selected fair root is a genuine bracket zero, including zero effect and zero amplitude. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairEquationRegularity 6 declarations The Taylor identity gives joint smoothness away from the removable axes, including relative smoothness on the closed parameter box.
Regularity and endpoint roots of the fair equation
The Taylor identity gives joint smoothness away from the removable axes, including relative smoothness on the closed parameter box. At the cell endpoints it supplies actual bracket roots off the axes. Matching itself follows from the undivided Taylor identity, including both axes.
[The closed effect, signed amplitude, and centering box; position is unrestricted.
Off the axes the Taylor extension has the joint smoothness of its quotient, relative to the full closed calibration box. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
At interior box points, off-axis smoothness holds on a full neighborhood. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Endpoint matching supplies a root of the actual normalized equation off the axes. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The endpoint root belongs to the prescribed open centering bracket. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Multiplying the normalized root equation gives matching without any division or exception for the effect and amplitude axes. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairEquationSmoothness 7 declarations Compactness of the integration interval supplies uniform derivative bounds for parameter differentiation.
Smoothness of the fair Taylor equation through its axes
Compactness of the integration interval supplies uniform derivative bounds for parameter differentiation. Iterating this argument preserves every finite order of smoothness in the two Taylor integrations.
The scalar integration coordinate is fixed when taking the parameter derivative. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Local joint differentiability on a compact interval justifies differentiation under the parameter integral, with a bound uniform in the integration coordinate. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Every finite derivative order passes through integration on the fixed compact interval. The induction differentiates the actual parameter family. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Smoothness at all points above a compact integration interval gives smoothness of the parameter integral on a full neighborhood of the base parameter. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Both Taylor integrations preserve joint smoothness of the actual fair normalized equation, including both axes and every boundary of the closed box. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The center partial derivative is jointly smooth also on the removable axes. Under the stated assumptions.
Formal statement
Proof (Lean source)
Every fixed derivative order of the actual normalized equation is uniformly bounded on the same closed parameter box, with no excluded amplitude axis. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairMixtureParity 16 declarations Simultaneous reversal of endpoint signs proves evenness of the actual fair component likelihoods, including all substituted roots and totalization.
Fair component cancellation through zero amplitude
Simultaneous reversal of endpoint signs proves evenness of the actual fair component likelihoods, including all substituted roots and totalization. Their difference from the comparator vanishes to first order at zero, as required by the quadratic Taylor step in the original-record mixture proof.
[Negating the fair amplitude reverses every endpoint sign in the random table. the stated conclusion holds.
Formal statement
Proof (Lean source)
The comparator table is even in the amplitude, with its actual root substituted. the stated conclusion holds.
Formal statement
Proof (Lean source)
Sign reversal identifies actual observed laws, including the fallback law. the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual observed comparator law is even in its amplitude. the stated conclusion holds.
Formal statement
Proof (Lean source)
The entire finite-prior sample measure is even, without revealing any signs. the stated conclusion holds.
Formal statement
Proof (Lean source)
Actual likelihood difference on any selected block of original records. The sign prior remains hidden and all records in the block share its draw.
Definition (Lean source)
Every block mixture difference is even by reversal of the shared sign prior. the stated conclusion holds.
Formal statement
Proof (Lean source)
At zero amplitude every block mixture equals its product comparator. the stated conclusion holds.
Formal statement
Proof (Lean source)
An even real function has zero totalized derivative at zero. This also covers nondifferentiable inputs, where Lean's derivative is defined as zero. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The linear term of every actual fair block difference vanishes. the stated conclusion holds.
Formal statement
Proof (Lean source)
The signed second-order Taylor bound when the constant and linear terms vanish. Evenness permits the same positive-interval argument for both signs. the documented result Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Applying Taylor to the actual block difference needs only its smoothness and second-derivative estimate; the two zero terms are already proved. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual fair component Taylor estimate has the roadmap's coefficient. The product differentiation bound is kept as an explicit remaining input. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Exact singleton matching removes any one-record block, throughout the support neighborhood and including the original observed cells. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Averaging products of densities with the common half-unit floor preserves the component floor, despite dependence among records through the hidden signs. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual fair component square-root discrepancy follows from its Taylor bound and one-record density floors, with the precise exponential coefficient. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairNumeratorSmoothness 6 declarations The numerator is smooth on full neighborhoods of the closed effect range, small signed amplitudes, and the entire centering bracket.
Smooth fair numerator and Taylor-axis cancellations
The numerator is smooth on full neighborhoods of the closed effect range, small signed amplitudes, and the entire centering bracket. Sign symmetry kills its first amplitude derivative at zero; the zero-effect identity kills every amplitude derivative there. These are inputs to the two Taylor divisions.
The shifted centering risk remains positive uniformly over the sign law. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Smoothness concerns the actual numerator, jointly in all four variables. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Evenness gives the missing linear Taylor coefficient without excluding the axes. the stated conclusion holds.
Formal statement
Proof (Lean source)
At zero effect the whole second amplitude-derivative function vanishes. the stated conclusion holds.
Formal statement
Proof (Lean source)
The zero linear coefficient is an actual derivative at every allowed effect and center, rather than only the value of a totalized derivative. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Every fixed-order derivative of the actual numerator has one absolute bound on the full closed effect, signed amplitude, center, and coordinate box. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairOpenNeighbourhood 2 declarations The implicit equation supplies genuine roots on ambient neighborhoods of the zero-amplitude effect and spatial rectangle.
Common open fair-calibration neighborhood
The implicit equation supplies genuine roots on ambient neighborhoods of the zero-amplitude effect and spatial rectangle. Persistent bracket uniqueness identifies the actual selector there. Compactness then puts a closed signed amplitude box inside one open set for the root and every substituted cell.
At zero amplitude the fair selector remains a genuine, unique narrow-bracket root on a full ambient parameter neighborhood. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
One open set contains a positive closed signed amplitude box over the entire fair effect and spatial ranges, with unique roots and smooth actual cells. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairProductDerivatives 2 declarations The actual hidden-sign mixture and comparator inherit the component derivative bound from their one-record smoothness and derivative envelopes.
Fair component product differentiation
The actual hidden-sign mixture and comparator inherit the component derivative bound from their one-record smoothness and derivative envelopes.
[Product differentiation and finite averaging establish the fair component's second-derivative estimate from one-record bounds, including the comparator's substituted root and effect. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The fair component Hellinger estimate now needs only the one-record analytic envelopes. Product smoothness, its second derivative, and both Taylor cancellations are assembled here rather than assumed at component level. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairPrognosisEnvelope 5 declarations The calibrated root's quadratic displacement and the bounded sign field keep both fair control risks near the asymmetric center.
Fair native prognosis envelope
The calibrated root's quadratic displacement and the bounded sign field keep both fair control risks near the asymmetric center. This proves the native prognosis envelope on one absolute signed neighborhood, including fallback laws.
[Quadratic centering and a small sign perturbation keep both fair control risks in the interval where the native logit has magnitude at most one. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The exact fair arm normalization identifies its native control risk. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Centered fair roots give the native prognosis envelope even if cell continuity has not yet been established, because the fallback has zero logit. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The calibration lemma's quadratic root bound yields one positive signed radius on which both fair constructions satisfy the model's prognosis envelope. the documented result
Formal statement
Proof (Lean source)
The two remaining spatial prognosis obligations, separated from the pointwise envelope already proved from quadratic root centering.
Definition (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairRootExistence 2 declarations The strictly separated zero-amplitude bracket signs persist on one signed amplitude neighborhood by compactness in effect and spatial coordinate.
Uniform fair-root existence over the full effect range
The strictly separated zero-amplitude bracket signs persist on one signed amplitude neighborhood by compactness in effect and spatial coordinate. Continuity in the centering argument then supplies an interior root.
One absolute signed amplitude neighborhood preserves the fair bracket signs for all effects and spatial coordinates in their closed prescribed ranges. the documented result
Formal statement
Proof (Lean source)
The intermediate value theorem yields a genuine fair root in the full selector bracket on one absolute signed amplitude neighborhood. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairRootNearZero 9 declarations The explicit zero-effect equation supplies a nonzero center slope.
Local fair-root regularity at zero effect
The explicit zero-effect equation supplies a nonzero center slope. Compactness preserves its signs and local monotonicity, identifying the literal selector with a smooth implicit branch on full neighborhoods of the zero-effect axis.
The normalized equation has the Bernoulli-variance slope on the zero-effect axis. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[On a full parameter neighborhood, every bracket value remains close to its explicit zero-effect value and remains jointly smooth. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The center derivative stays uniformly positive on a smaller bracket in full neighborhoods of zero effect and amplitude, including spatial endpoints. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Uniform approximation to the limiting variance equation excludes roots outside a smaller bracket, rather than presupposing the selected root's value. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Opposite signs give an interior root, and the derivative floor makes it unique throughout the original selector bracket on a full parameter neighborhood. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
One absolute signed neighborhood supplies unique fair bracket roots for all spatial coordinates, including both endpoints, when the effect is near zero. the documented result
Formal statement
Proof (Lean source)
A C∞ equation and nearby uniqueness give C∞ regularity of the actual bracket selector. A C1 implicit branch first supplies continuity; the pointwise implicit theorem then upgrades it without an analyticity assumption. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The literal fair root is jointly C∞ at zero effect and zero amplitude, on full neighborhoods of every spatial point in the closed interval. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual selected fair root solves its normalized equation and is the only root in the prescribed bracket on one absolute neighborhood of the origin. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairRootSelection 6 declarations The endpoint sign laws give identical Taylor-normalized equations and identical literal root selectors.
Fair calibration root selection
The endpoint sign laws give identical Taylor-normalized equations and identical literal root selectors. Existence and uniqueness in the prescribed bracket transport to the actual selected root, without assumptions on its value.
[Endpoint sign averages agree for all amplitudes and centering values. the stated conclusion holds.
Formal statement
Proof (Lean source)
Equality of the full numerator functions transports all derivatives in the integral Taylor extension, including its zero axes. the documented result
Formal statement
Proof (Lean source)
Equal endpoint equations give equal literal fair selectors, even on fallback inputs where no bracket root exists. the documented result Under the stated assumptions. The stated conclusion follows.
Proof (Lean source)
An existing bracket root makes the totalized fair selector a genuine root. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The totalized selector stays in its prescribed open bracket on every input; the fallback center also lies strictly inside that bracket. the documented result
Proof (Lean source)
A uniquely characterized bracket root is the actual selected center. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairRootTaylorBounds 7 declarations The integral Taylor estimate derives the quadratic amplitude bound for the actual root and its spatial derivative from smoothness and the axis value.
Quadratic fair-root bounds
The integral Taylor estimate derives the quadratic amplitude bound for the actual root and its spatial derivative from smoothness and the axis value.
An even scalar function has zero totalized derivative at the origin. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The second integral Taylor formula bounds a smooth even function for signed increments. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Scalar coordinate partial derivative of a joint parameter function.
Coordinate differentiation preserves joint smoothness at the actual parameter point. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Smoothness on the closed calibration region uniformly bounds the actual second amplitude derivatives of the root and its spatial derivative. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Constancy on the closed spatial interval forces the actual derivative to vanish even at the endpoints, where two-sided smoothness is available. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Smoothness and the zero-amplitude center derive one uniform quadratic bound for the actual fair root and its spatial derivative. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairSingletonMatching 11 declarations The explicit comparator effect matches the two-point risk average at both cell endpoints.
Exact fair singleton matching
The explicit comparator effect matches the two-point risk average at both cell endpoints. The zero-effect and zero-amplitude identities also cover the axes when assembling matching from the normalized root equation.
[The fair comparator preserves effect on the zero-amplitude axis. the stated conclusion holds.
Formal statement
Proof (Lean source)
The fair comparator vanishes on the zero-effect axis. the stated conclusion holds.
Formal statement
Proof (Lean source)
Zero effect makes the risk shift the identity. the stated conclusion holds.
Formal statement
Proof (Lean source)
The fair numerator vanishes for zero amplitude, at every centering value. the stated conclusion holds.
Formal statement
Proof (Lean source)
The mean-zero sign field gives exact matching at zero effect. the stated conclusion holds.
Formal statement
Proof (Lean source)
Positivity of the logarithm arguments and shifted-risk denominators in the fair construction. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The comparator exponential is exactly the rational odds correction in the roadmap. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
At the fixed centering value, the fair comparator matches the average of the two shifted risks. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
At either cell endpoint, the sign field has the law of one fair sign. Under the stated assumptions.
Formal statement
Proof (Lean source)
The explicit fair comparator has exactly zero endpoint numerator at the prescribed center. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
A normalized root gives singleton matching; the zero axes use their exact identities. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairSpatialOscillation 5 declarations The logit is Lipschitz on the fixed interior risk interval.
Fair prognosis oscillation at the calibrated amplitude scale
The logit is Lipschitz on the fixed interior risk interval. Quadratic root centering and the bounded sign field give an exponent-uniform oscillation bound for the actual random law and deterministic comparator.
[The logarithm has Lipschitz constant three on the interior interval used for a risk and its complement. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Positive floors for a risk and its complement bound logit differences by six times the risk difference. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual fair native control logit stays near the fixed center with linear sign-field displacement and quadratic root displacement. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Two displacements from the same fixed center give the actual fair prognosis oscillation; fallback laws have constant zero prognosis. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
One absolute positive amplitude radius gives the prescribed fair prognosis oscillation at every nonnegative exponent and every rank. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairTaylorDerivatives 10 declarations The two amplitude derivatives and subsequent effect derivative are jointly smooth on full neighborhoods of the calibration box.
Actual derivatives in the fair Taylor extension
The two amplitude derivatives and subsequent effect derivative are jointly smooth on full neighborhoods of the calibration box. These are derivatives of the actual numerator, with all four parameters allowed to vary.
Taking a scalar partial derivative preserves joint smoothness of a smooth family. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The first amplitude derivative is smooth jointly in effect, amplitude, center and position. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Both amplitude derivatives remain jointly smooth, including at zero amplitude. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual third derivative appearing inside the double Taylor integral is jointly smooth. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
A segment from zero to a signed amplitude stays inside its absolute-value bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Multiplication by a unit-interval coordinate lies on the signed amplitude segment. the stated conclusion holds. Under the stated assumptions.
Proof (Lean source)
Rescaling the fundamental theorem works for signed increments and at zero. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The second integral Taylor identity uses the actual zero value and slope; it remains valid for both signs of the amplitude. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Two integral Taylor identities recover the actual numerator on both axes, without division by either parameter. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Away from the axes, the double-integral extension is exactly the normalized numerator. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairZeroAmplitude 9 declarations The second amplitude derivative of the finite sign average depends only on the unit second moment of the sign field.
Fair calibration on the zero - amplitude axis
The second amplitude derivative of the finite sign average depends only on the unit second moment of the sign field. Thus the Taylor - normalized equation is independent of position at zero amplitude, and the exact endpoint identity supplies a center root throughout that axis.
The derivative of the risk under an affine amplitude perturbation is the explicit squared - denominator expression. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The second amplitude derivative of the risk at zero amplitude contains exactly the squared perturbation mark. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The second derivative of the sign - averaged risk is independent of the within - cell coordinate because every sign field has unit second moment. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The comparator term has no position argument, while the averaged risk's second derivative depends only on the unit sign variance. Hence the actual numerator's second derivative agrees with its endpoint value. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Both integral Taylor divisions preserve the position - independent second amplitude coefficient, including the effect - range boundary points. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The exact endpoint equation supplies the asymmetric center as a root on the entire zero - amplitude axis, uniformly in effect and position. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The center root lies strictly in the selector bracket at every point of the zero - amplitude axis. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
An actual root exists on the zero - amplitude axis, so the literal selector satisfies the normalized equation there without invoking a fallback case. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The near - zero uniqueness neighborhood identifies the literal selector with the fixed center at the cell endpoints and on the amplitude axis. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FairZeroEffect 8 declarations The effect derivatives of the literal risk and comparator formulas identify the limiting normalized equation and its unique bracket root.
Fair calibration on the zero-effect axis
The effect derivatives of the literal risk and comparator formulas identify the limiting normalized equation and its unique bracket root.
[At zero effect the logistic risk slope is its Bernoulli variance. the stated conclusion holds.
Formal statement
Proof (Lean source)
The comparator's zero-effect slope accounts for the amplitude variance. the stated conclusion holds.
Formal statement
Proof (Lean source)
Differentiating the actual finite sign average at zero effect gives exactly its variance cancellation against the deterministic comparator. the documented result
Formal statement
Proof (Lean source)
The undivided Taylor identity identifies the normalized zero-effect value whenever the signed amplitude is nonzero. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Continuity in the signed amplitude extends the explicit zero-effect formula through the intersection of both removable axes. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The prescribed asymmetric center is a root on the entire zero-effect axis. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The other quadratic root is outside the selector bracket, so the zero-effect center is uniquely characterized within that bracket. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The literal root selector equals the paper's center for zero effect, including zero amplitude and both spatial endpoints. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FinitePriorHellinger 4 declarations The original-sample mixture densities are normalized probability densities.
Hellinger testing reduction for the actual finite priors
The original-sample mixture densities are normalized probability densities. The library's affinity comparison therefore converts a squared Hellinger budget of one hundredth into the total variation budget of one tenth, unchanged by the optional independent seed.
[The actual finite-prior density integrates to one under the sample reference. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The RN formulation of the distance equals the discrepancy of the literal finite averages of original-record likelihoods. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The Cauchy–Schwarz affinity estimate controls the full sample-and-seed experiment by the square root of its original-record squared Hellinger distance. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The paper's Hellinger budget yields its seven-tenths testing coefficient. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FinitePriorTesting 12 declarations Uniform sign averaging preserves honesty and averages expected interval length.
Finite-prior testing with the original records and independent seed
Uniform sign averaging preserves honesty and averages expected interval length. Transferring coverage by total variation then gives the two-effect length lower bound for every Borel honest procedure, including randomized procedures.
[The prior draws its sign once, then supplies the original sample and seed.
Definition (Lean source)
Averaging the original-record laws and then tensoring the seed gives exactly the finite prior of full experiments. the documented result
Formal statement
Proof (Lean source)
A prior concentrated on one law gives its literal full experiment. the stated conclusion holds.
Formal statement
Proof (Lean source)
The sign prior has exactly unit mass. the stated conclusion holds.
Definition (Lean source)
The original-record mixture is itself a probability measure. the stated conclusion holds.
Formal statement
Proof (Lean source)
Adding the same independent seed preserves total variation exactly. the stated conclusion holds.
Formal statement
Proof (Lean source)
Event probabilities are the finite average of the constituent experiments. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrals of an integrable observable are finite prior averages. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Bounded measurable procedure length is integrable under the finite prior. the stated conclusion holds.
Formal statement
Proof (Lean source)
If all prior draws lie in the evaluation slice, its average length is bounded by the worst expected length on that slice. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Global honesty transfers to a prior with a single common scalar effect. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Two common-effect finite priors give the roadmap's length bound. The second prior needs ambient membership; only the first needs slice membership. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FrontierAssembly 7 declarations The proved upper construction supplies the operational guarantees and both upper comparisons.
Assembling the honest frontier
The proved upper construction supplies the operational guarantees and both upper comparisons. The parametric floor supplies the numerator branch above the elbow. Separate numerator and radius lower estimates combine into the full profile against every honest, possibly randomized procedure.
[A pointwise bound on expected length bounds the radius-slice supremum; the concrete parametric null certifies that this slice is nonempty. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The finite honest upper theorem certifies the literal implementation's operational guarantees and the two upper comparisons with one absolute constant. the documented result Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
[Above and at the numerator elbow, the parametric null comparison supplies the numerator lower rate for every honest procedure and every radius. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A lower estimate in the rough numerator regime extends to the whole domain by taking the smaller of its constant and the proved parametric constant. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The positive-radius lower estimate extends to radius zero by the nonnegativity of expected interval length, without a new comparison prior. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Simultaneous numerator and radius lower estimates give half the smaller constant times their sum, as in the testing-to-length roadmap. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The proved operational and upper guarantees and a universal procedure lower bound give all three frontier comparisons, transferring the lower bound to the infimum over honest procedures. the documented result Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FrontierElbows 5 declarations The explicit rate exponents give both radius-transition formulas, with positive gap and agreement at the numerator elbow.
Algebraic transitions and compact bounds for the frontier
The explicit rate exponents give both radius-transition formulas, with positive gap and agreement at the numerator elbow. Absolute positive finite constants also satisfy the compact-uniform conditions. These certificates do not use the unfinished statistical comparison theorems.
Below the numerator elbow, the projection exponent is the active branch. Under the stated assumptions.
Formal statement
Proof (Lean source)
At and above the numerator elbow, the parametric exponent is the active branch. Under the stated assumptions.
Formal statement
Proof (Lean source)
The two radius-transition expressions are exact, positive, and agree on the elbow. Under the stated assumptions.
Formal statement
Proof (Lean source)
Saturation at the parametric exponent occurs precisely on and above the elbow. Under the stated assumptions.
Formal statement
Proof (Lean source)
Absolute positive finite constants meet all the compact-uniform requirements. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.FrontierMixtureRates 3 declarations A single absolute ceiling multiplier controls occupancy and the two mixture Hellinger budgets.
Uniform mixture lower rates
A single absolute ceiling multiplier controls occupancy and the two mixture Hellinger budgets. The mixed and fair testing bounds then give the numerator and radius rates with the roadmap's uniform square-root ceiling factor.
The amplitude product is the power at the sum of the native exponents. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The squared amplitude product and the pair-count factor combine into the balanced Hellinger power budget. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Both lower rates use one absolute multiplier and the same original record mixture lemma, with no restrictions beyond the paper's domain. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.LengthSensitivity 10 declarations The clipped logarithm is globally Lipschitz in its quotient argument.
Sensitivity of the clipped odds interval
The clipped logarithm is globally Lipschitz in its quotient argument. A positive denominator floor then controls the width of the confidence rectangle on every sample, including samples outside the coverage event.
Clipping contracts absolute differences. Under the stated assumptions.
Formal statement
Proof (Lean source)
On a positive half-line the logarithm has the reciprocal-floor Lipschitz bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Effect clipping gives the exact global exponential Lipschitz constant in the roadmap. the stated conclusion holds.
Formal statement
Proof (Lean source)
Inserting a cross quotient controls the two-coordinate perturbation. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Any two corners of a confidence rectangle obey the same length envelope. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Clipping the denominator preserves its floor and bounds the width by the input width. Under the stated assumptions.
Formal statement
Proof (Lean source)
The four-corner inversion width obeys an unconditional rectangle bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact ideal endpoints satisfy the unconditional bound on every original sample. the stated conclusion holds.
Formal statement
Proof (Lean source)
Outward rounding adds only the prescribed two-over-n excess to the samplewise bound. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
A square-integrable coordinate is controlled in absolute mean by its bias and variance. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.LogEnclosure 7 declarations The finite geometric remainder, public rational range bound and exponential comparison certify the literal atanh sum at its fixed truncation count.
Certificates for the prescribed logarithm truncation
The finite geometric remainder, public rational range bound and exponential comparison certify the literal atanh sum at its fixed truncation count. Monotonicity then gives the primitive interval contract.
[The public logarithm range bounds both the argument and its reciprocal. the stated conclusion holds.
Formal statement
Proof (Lean source)
The atanh coordinate has the range and denominator bounds used by the roadmap. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The exponential comparison makes a full public block decay by a dyadic factor. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The prescribed integer count absorbs the range factor in the geometric tail. the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite geometric remainder certifies the literal logarithm polynomial. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The symmetric scalar bracket contains the logarithm with the requested endpoint excess. Under the stated assumptions.
Formal statement
Proof (Lean source)
Monotonicity extends the certified logarithm brackets to positive rational intervals. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.LogProgram 15 declarations Two endpoint loops compute the odd-power sum using the exact public count.
Register certificate for the prescribed logarithm recurrence
Two endpoint loops compute the odd-power sum using the exact public count. Nonpositive scalar arguments return the prescribed zero point.
[The integer range bound is computed by clamping the two signed ceilings. the stated conclusion holds.
Formal statement
Proof (Lean source)
The two-endpoint logarithm register code.
Definition (Lean source)
The loop head records the odd index, power, partial sum and untouched frame.
Definition (Lean source)
Initialization computes the literal logarithm truncation count. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
One seven-instruction block adds the next odd-power term. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
At zero count both branches return the prescribed sorted scalar endpoints. Under the stated assumptions.
Formal statement
Proof (Lean source)
The fixed term loop exhausts its counter before the scalar exit. Under the stated assumptions.
Formal statement
Proof (Lean source)
The initial frame saves the right endpoint before the left scalar loop. the stated conclusion holds.
Formal statement
Proof (Lean source)
The instruction bound includes two endpoint initializations, loops and exits.
Definition (Lean source)
Both endpoint loops return the literal endpoint extension on every rational list. the stated conclusion holds.
Formal statement
Proof (Lean source)
A straight-line program computes the public count of both endpoint loops.
Definition (Lean source)
The instruction count is itself a finite rational register computation. the stated conclusion holds.
Formal statement
Proof (Lean source)
The fixed public count halts the logarithm computation on every rational list. the stated conclusion holds.
Formal statement
Proof (Lean source)
Certified finite rational register implementation of both logarithm endpoints.
Definition (Lean source)
The finite register result equals the prescribed logarithm endpoint extension. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.LowerRankRates 3 declarations One rank estimate applies with s = α + β to the mixed priors and s = 2β to the fair priors.
Ceiling ranks for the mixed and fair lower rates
One rank estimate applies with s = α + β to the mixed priors and s = 2β to the fair priors. It controls occupancy and the Hellinger budget and retains a uniform lower bound on the amplitude separation.
Ceiling selection has the roadmap's two-sided rank bounds. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A rank above L times the target controls both occupancy and the balanced power budget. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The ceiling costs a fixed square-root factor, uniformly over the entire rough numerator regime and over the fair exponent s = 2β. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MachinEnclosure 6 declarations Integration of the finite geometric identity bounds the two arctangent remainders.
The prescribed finite Machin enclosure
Integration of the finite geometric identity bounds the two arctangent remainders. Machin's identity and the public truncation count certify the rational pi box.
Finite geometric cancellation leaves precisely the omitted arctangent term. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Integrating the finite geometric polynomial gives the literal rational polynomial. the stated conclusion holds.
Formal statement
Proof (Lean source)
The integrated geometric remainder is bounded uniformly on a positive argument interval. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The fixed public term count controls the sum of both weighted remainders. the stated conclusion holds.
Formal statement
Proof (Lean source)
Machin's identity bounds the literal rational approximation at every precision. the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping the certified Machin approximation preserves containment and both excess bounds. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedAlternativePrognosisLinear 5 declarations The smooth control-logit map is locally Lipschitz on a fixed interior box.
Alternative mixed prognosis spatial bounds
The smooth control-logit map is locally Lipschitz on a fixed interior box. The spatial moduli of the calibrated margins then preserve the prognosis amplitude.
[The control logit is smooth at the independent central table. the stated conclusion holds.
Formal statement
Proof (Lean source)
A fixed signed interior box has one finite control-logit Lipschitz constant. the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual alternative control risk uses the smooth calibrated margin map. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Fixed local Lipschitz and root derivative bounds yield the alternative prognosis spatial modulus with its amplitude factor intact. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
One positive radius fits the alternative prognosis modulus to the public rate for every legal exponent pair, including the Lipschitz endpoint. the documented result Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedCellSmoothness 5 declarations The literal selected root is substituted before differentiating the cells.
Smooth actual mixed cells
The literal selected root is substituted before differentiating the cells. Positive radicands at zero amplitudes, smooth composition, and compactness give one signed neighborhood and bounds for every fixed derivative order.
The covariance formula is smooth at zero effect and central margins. the stated conclusion holds.
Formal statement
Proof (Lean source)
With the actual root substituted, every mixed cell is smooth on a full neighborhood of every zero-amplitude spatial point. the documented result
Formal statement
Proof (Lean source)
A single signed square makes all actual mixed cells smooth, including full neighborhoods of both spatial endpoints. the documented result
Formal statement
Proof (Lean source)
The closed mixed parameter square is compact. the stated conclusion holds.
Formal statement
Proof (Lean source)
Compactness bounds full derivatives of all finitely many actual mixed cells simultaneously, at every fixed order. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedComponentSupport 3 declarations The full derivative envelope supplies scalar amplitude partials.
Mixed component bounds from calibrated record support
The full derivative envelope supplies scalar amplitude partials. Product differentiation and two-axis cancellation bound each actual block likelihood; restriction of the uniform hidden sign prior transfers the bound to components.
[Every scalar partial needed by the rectangular Taylor estimate follows from the actual mixed record's full derivative and smoothness envelopes. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual mixed block satisfies the two-axis component Hellinger estimate with the jointly selected support constants and no independent-record premise. the documented result Under the stated assumptions. Under the stated assumptions.
Proof (Lean source)
[Restricting the uniform sign prior preserves the actual mixed block bound, with the exact number of original records in the selected graph component. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedCoordinateDerivatives 3 declarations Coordinate lines have unit tangent vectors.
Scalar mixed partials from full derivative bounds
Coordinate lines have unit tangent vectors. The chain rule transfers the full first and second Fréchet derivative envelopes to the scalar amplitude partials.
The first amplitude derivative is the full derivative on a unit coordinate direction. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The second amplitude derivative uses the other unit coordinate direction. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Two-variable smoothness supplies the scalar mixed derivative and its literal second-order operator-norm bound. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedDensityRanges 5 declarations The literal root bracket bounds both perturbed margins.
Mixed four-cell density bounds
The literal root bracket bounds both perturbed margins. The covariance branch bound then gives a common density floor and ceiling for the actual mixed cells, including signed amplitudes and the law constructor's fallback inputs.
[The mixed selector always lies in its bracket, including its fallback value. the stated conclusion holds.
Proof (Lean source)
Small signed amplitudes keep both mixed margins near one half. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Products of the centered margins have uniform lower and upper bounds. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
All four mixed cells retain a fixed density floor and ceiling. Under the stated assumptions.
Formal statement
Proof (Lean source)
The complete substituted mixed cells satisfy the support density bounds. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedEquationSmoothness 12 declarations The exponential divided difference is smooth through zero by its analytic slope extension.
Smooth mixed calibration equation
The exponential divided difference is smooth through zero by its analytic slope extension. The positive - radicand table formula is consequently smooth jointly in the signed amplitudes, spatial coordinate, and root variable.
[The integral divided difference recovers the exponential increment, also at zero. the stated conclusion holds.
Formal statement
Proof (Lean source)
The integral divided difference is the derivative - completed exponential slope. the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual integral formula is smooth to every order, including at zero. The stated conclusion follows.
Formal statement
Proof (Lean source)
The normalized table is jointly smooth at every positive radicand and nonzero denominator. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
Radicand of a mixed normalized table, with all signed parameters substituted.
Definition (Lean source)
Smoothness of the actual mixed equation follows from its finitely many positive radicands. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[At every point of the zero-amplitude rectangle, the full mixed equation is smooth. the stated conclusion holds.
Formal statement
Proof (Lean source)
The root-variable derivative at zero amplitudes is exactly minus one. the stated conclusion holds.
Formal statement
Proof (Lean source)
The root-variable derivative varies continuously jointly near each zero-amplitude point. the stated conclusion holds.
Formal statement
Proof (Lean source)
Compactness supplies one signed amplitude square with a uniform negative derivative floor. the stated conclusion holds.
Formal statement
Proof (Lean source)
A negative derivative floor gives uniqueness throughout the entire prescribed root bracket. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Existence and the uniform derivative floor give a unique mixed root on one absolute signed square. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedMixtureTaylor 7 declarations Both amplitude axes cancel for any block of original records under the hidden sign prior.
Mixed component cancellation and the rectangular Taylor estimate
Both amplitude axes cancel for any block of original records under the hidden sign prior. Two applications of the mean value theorem turn a bound on the actual mixed derivative into the product-amplitude component estimate. The smoothness and product derivative bounds remain explicit inputs, rather than being assumed by the paper's mixture theorem.
[Difference of the two actual block likelihoods, averaged over the same hidden endpoint-sign prior without assuming independence inside the block.
Definition (Lean source)
On the zero propensity axis the actual block likelihoods agree draw by draw. the stated conclusion holds.
Formal statement
Proof (Lean source)
On the zero prognosis axis global sign reversal reindexes the block prior. the stated conclusion holds.
Formal statement
Proof (Lean source)
Two mean value estimates on the signed rectangle give a product-amplitude bound when both axes vanish. The derivatives are of the fully substituted function. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Applying the rectangular estimate to actual mixed blocks uses the two proved axis identities. Product differentiation is the remaining analytic input. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Each singleton block cancels throughout the signed support neighborhood, using exact matching of the actual observed cell tables. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual mixed component square-root discrepancy follows from its rectangular Taylor estimate and one-record floors. No record independence inside the block is used. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedNullPrognosisLinear 6 declarations The null covariance vanishes, so its control risk is exactly the prognosis margin.
Null mixed prognosis spatial bounds
The null covariance vanishes, so its control risk is exactly the prognosis margin. The shared-sign Lipschitz estimate and interior logit bound preserve the prognosis amplitude, including the endpoint exponent one.
[A positive treatment complement identifies the table's control risk with the prognosis margin minus its covariance correction. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[On the fixed interior margin interval, changes in the covariance correction split into a covariance change and a treatment-margin change. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The control-risk formula transfers covariance and margin moduli to an explicit risk modulus on the fixed interior box. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The valid null mixed law has control risk equal to its prognosis margin. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The null native prognosis logit has a global Lipschitz constant linear in the prognosis amplitude, independently of the propensity amplitude. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The null prognosis Lipschitz estimate fits the prescribed scale for all nonnegative public exponents and every calibrated rank. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedOpenNeighbourhood 2 declarations The implicit branch supplies actual bracket zeros near each zero-amplitude spatial point.
Common open mixed-calibration neighborhood
The implicit branch supplies actual bracket zeros near each zero-amplitude spatial point. The derivative floor identifies the selector uniquely there. Compactness of the spatial interval then gives a closed amplitude square inside one open set on which both the selector and every substituted cell are smooth.
Bracket existence and uniqueness persist on ambient neighborhoods, including beyond the endpoints of the spatial interval. the documented result
Formal statement
Proof (Lean source)
One common open set contains a positive closed signed amplitude square and preserves the genuine mixed branch and all fully substituted cell formulas. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedProductDerivatives 4 declarations Leibniz differentiation bounds the mixed amplitude derivative of a finite product using only derivatives of its individual records.
Mixed partial derivatives of record products
Leibniz differentiation bounds the mixed amplitude derivative of a finite product using only derivatives of its individual records.
[The mixed Leibniz estimate counts both diagonal and off-diagonal terms. First-coordinate differentiability is needed only near the second coordinate, so this applies inside a signed calibration neighborhood. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Finite hidden-sign averages commute with the two amplitude derivatives; the difference of two averages costs a factor of two in the envelope. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual mixed block inherits its mixed derivative envelope from one-record partial derivatives, with all calibration roots substituted. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Product differentiation, sign averaging, axis cancellation, and rectangular Taylor control assemble the mixed component Hellinger bound directly from one-record analytic inputs. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedPrognosisOscillation 5 declarations The rationalized covariance retains its effect factor.
Mixed prognosis oscillation
The rationalized covariance retains its effect factor. Control-risk displacement and the interior logit estimate give oscillation at the prognosis amplitude.
The covariance is bounded linearly by the effect on the fixed interior box. Under the stated assumptions.
Formal statement
Proof (Lean source)
Subtracting the covariance correction bounds the control risk's displacement. Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual native prognosis retains the prognosis amplitude in its envelope. Under the stated assumptions.
Formal statement
Proof (Lean source)
Two centered bounds control mixed prognosis oscillation. Under the stated assumptions.
Formal statement
Proof (Lean source)
The oscillation estimate fits the prescribed scale at every calibrated rank. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedPropensityLinear 5 declarations Bounded root derivatives and shared endpoint gluing preserve the propensity amplitude in the global Lipschitz constant.
Mixed propensity spatial bounds
Bounded root derivatives and shared endpoint gluing preserve the propensity amplitude in the global Lipschitz constant.
[Restricting the smooth root to its spatial coordinate preserves the first Fréchet derivative bound, since the coordinate tangent has norm one. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Equal endpoint roots and the derivative bound give a global spatial Lipschitz estimate without requiring matching endpoint derivatives. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The bounded root times the sign field has Lipschitz constant at most five plus twice the root derivative bound, multiplied by rank. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Interior logits transfer the margin's amplitude-preserving spatial bound to the actual mixed law; the totalization fallback is constant. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
A fixed positive radius makes the mixed propensity Lipschitz constant fit the prescribed scale for every nonnegative exponent pair and every rank. the documented result Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedPropensityOscillation 5 declarations The root bracket and bounded sign field give linear displacement from one half.
Mixed propensity oscillation
The root bracket and bounded sign field give linear displacement from one half. The interior logit bound transfers it to the native propensity and its oscillation.
The literal treatment margin is the propensity whenever the cells are valid. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Root and sign bounds retain the amplitude factor in the margin displacement. Under the stated assumptions.
Formal statement
Proof (Lean source)
The native propensity logit has linear displacement, including fallback laws. Under the stated assumptions.
Formal statement
Proof (Lean source)
Two centered displacements bound the oscillation at the propensity amplitude. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Every sufficiently small calibration radius gives the prescribed oscillation uniformly over ranks and nonnegative exponents, for both mixed constructions. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedRootExistence 7 declarations Positive table denominators and uniform sign separation follow from continuity on the compact zero-amplitude parameter rectangle.
Uniform existence of the mixed calibration root
Positive table denominators and uniform sign separation follow from continuity on the compact zero-amplitude parameter rectangle. The intermediate value theorem then supplies a root in the prescribed open bracket for small signed amplitudes.
The exponential divided difference is continuous also at zero. The stated conclusion follows.
Formal statement
Proof (Lean source)
Denominator of one normalized mixed table, before selecting a root.
Definition (Lean source)
Each mixed-table denominator varies continuously with all parameters. The stated conclusion follows.
Formal statement
Proof (Lean source)
The mixed equation is continuous wherever its finitely many denominators are nonzero. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
At zero amplitudes the equation is the affine function with root one. the stated conclusion holds.
Formal statement
Proof (Lean source)
Compactness gives one signed amplitude square with positive denominators and separated signs. the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform sign separation and continuity provide a genuine interior mixed root. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedRootSmoothness 6 declarations Local implicit branches agree with the literal bracket selector by the uniform negative derivative floor.
Smoothness of the actual mixed root
Local implicit branches agree with the literal bracket selector by the uniform negative derivative floor. Compactness extends their smoothness to a single signed amplitude neighborhood, including the spatial endpoints.
The literal mixed selector chooses a bracket zero whenever one exists. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
At zero amplitudes the selector is exactly the affine-equation root one. the stated conclusion holds.
Formal statement
Proof (Lean source)
The derivative floor holds on the whole bracket for parameters in a full neighborhood of every zero-amplitude spatial point, even at the endpoints. the documented result
Formal statement
Proof (Lean source)
The actual selected mixed root is smooth through both signed amplitude axes at every spatial point. Local uniqueness identifies it with the implicit branch. the documented result
Formal statement
Proof (Lean source)
Smoothness of the literal selector holds on one absolute closed signed amplitude square, on full neighborhoods even at its spatial endpoints. the documented result
Formal statement
Proof (Lean source)
On the same signed neighborhood, every fixed derivative order of the actual mixed selector has a finite absolute bound. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixedSingletonMatching 10 declarations The normalized covariance equation cancels the mixed-margin second moment in all four cells.
Exact calibrated singleton cancellation
The normalized covariance equation cancels the mixed-margin second moment in all four cells. The fair risk equation matches the comparator. Uniform finite priors reproduce both local two-sign averages, with the roots substituted.
[The two local mixed tables have identical averages whenever the normalized root equation holds. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Two distinct coordinates of the uniform Boolean prior are independent fair signs; the other coordinates contribute exactly their multiplicity. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
A positive cell count gives two distinct endpoint indices. Under the stated assumptions.
Proof (Lean source)
[Even at the rightmost endpoint, the selected within-cell coordinate lies in the closed unit interval. the documented result Under the stated assumptions.
Proof (Lean source)
The full finite prior reproduces the exact local cancellation at each covariate. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Validity transfers the cancellation to the actual ambient laws, so the fallback of the totalized construction is never used. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact calibrated risk matching implies matching of each fair singleton cell; the control arm uses the mean-zero sign field. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The full fair sign prior has exactly the deterministic comparator's singleton cells whenever the calibrated risk equation holds. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Validity transfers fair singleton matching to the actual law and comparator. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Rate scaling by a nonnegative exponent stays inside the fixed amplitude neighborhood for every positive cell count. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureAxes 10 declarations On the propensity axis the two mixed laws coincide draw by draw.
Exact zero-amplitude identities for the original-record experiments
On the propensity axis the two mixed laws coincide draw by draw. On the prognosis axis reversal of all endpoint signs reindexes the complete finite prior. At zero fair amplitude every draw is the deterministic comparator. These are identities of the actual sample measures, including totalization.
Reversing every endpoint sign negates the entire shared-endpoint field. Under the stated assumptions.
Formal statement
Proof (Lean source)
The covariance is exactly zero at zero effect, for any margins. the stated conclusion holds.
Formal statement
Proof (Lean source)
Zero propensity amplitude makes the two mixed tables identical. the stated conclusion holds.
Formal statement
Proof (Lean source)
Zero prognosis amplitude turns sign reversal into a draw-wise table identity. the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual mixed sample measures agree on the zero propensity axis. the stated conclusion holds.
Formal statement
Proof (Lean source)
The uniform finite sign prior is invariant under simultaneous reversal. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual mixed sample measures agree on the zero prognosis axis after reindexing the prior, without revealing any latent signs. the documented result
Formal statement
Proof (Lean source)
Every zero-amplitude fair draw equals the comparator's table, regardless of which value the common root selector returns. the documented result
Formal statement
Proof (Lean source)
A uniform sign mixture of one common law is exactly that law's iid experiment. the stated conclusion holds.
Formal statement
Proof (Lean source)
At zero fair amplitude the entire original-record experiment equals its comparator, including the normalization of the finite prior. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureConditionalIntegration 11 declarations The uniform record reference separates into the public covariate law and the uniform four-label law.
Integrating conditional original-record experiments
The uniform record reference separates into the public covariate law and the uniform four-label law. Regrouping its finite product and applying Fubini retains all original records and integrates their conditional label discrepancy.
[The four-label reference assigns probability one quarter to each label.
The fair label reference has total mass one. the stated conclusion holds.
Definition (Lean source)
Every label array has exactly the uniform mass four to the minus n. the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional integration over labels is a finite uniform average. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The actual one-record reference is the product of covariates and fair labels. the stated conclusion holds.
Formal statement
Proof (Lean source)
Regrouping a sample into its covariates and labels preserves the full reference measure. This is a bijection and discards no sample coordinates. the documented result
Formal statement
Proof (Lean source)
Fubini identifies the original-sample integral with the covariate integral of the conditional label integral whenever the sample integrand is integrable. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Product likelihoods of the actual observed laws are integrable under the sample reference. the documented result
Formal statement
Proof (Lean source)
The shared-sign finite-prior likelihood is integrable under the same sample reference, with no independence assumption on its mixture components. the documented result
Formal statement
Proof (Lean source)
Nonnegative integrable densities have an integrable squared square-root discrepancy: its pointwise value is bounded by their sum. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The unconditional discrepancy is exactly the covariate integral of the conditional label discrepancy, since the two experiments share their covariate marginal. Fubini applies to the integrable actual likelihood discrepancy. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureCovariateOccupancy 20 declarations Cell adjacency has child-section mass at most 3/k.
Original-covariate component occupancy
Cell adjacency has child-section mass at most 3/k. A single root for each selected vertex set avoids an extra factor of the component size in the spanning-tree union bound.
The half-open cell convention, including its endpoint totalization, is measurable. The stated conclusion follows.
Formal statement
Proof (Lean source)
A cell graph edge is a measurable event of its two original covariates.
Definition (Lean source)
The coordinate-local graph is exactly the original-record sign graph. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
A child's admissible cells fit inside a real interval of length 3/k. Under the stated assumptions.
Formal statement
Proof (Lean source)
Integrating one leaf costs at most 3/k, including boundary cells. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A specified nonempty component has one selected rooted-parent cover. The root is fixed before sampling, so no extra factor of its size is charged. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[With all roots eligible, the library event is exactly the actual component event. the stated conclusion holds.
Formal statement
Proof (Lean source)
The event that a selected vertex set is an actual component is measurable. the stated conclusion holds.
Formal statement
Proof (Lean source)
The indicator of a component event is bounded and integrable. the stated conclusion holds.
Formal statement
Proof (Lean source)
The expected indicator of each actual component has the finite-parent tree bound. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The number of actual size-m components, each counted once by its vertex set.
Definition (Lean source)
The literal component count equals the sum of the actual component indicators. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Expected size-m components obey the precise unrooted subset coefficient. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The finite weighted count of all non-singleton components. Sizes above n contribute zero.
Definition (Lean source)
The weighted component count is an integrable statistic of the original covariates. the stated conclusion holds.
Formal statement
Proof (Lean source)
The weighted spanning-tree envelope applies to the actual original-covariate graph. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
At the prescribed occupancy threshold, actual components have quadratic expected weight. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Counting component supports by size agrees with counting the graph quotient. The finite powerset representation supplies a measurable statistic despite the sample-dependent type of connected components. the documented result
Formal statement
Proof (Lean source)
The finite size sum is exactly the non-singleton weighted component sum. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The complete component Taylor coefficient integrates to the paper's explicit mixture constant, for either amplitude product. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureDensities 17 declarations Finite cell integration identifies the one-record density relative to the uniform four-label reference, with the actual law's cells substituted.
Densities of the actual original-record laws
Finite cell integration identifies the one-record density relative to the uniform four-label reference, with the actual law's cells substituted.
[The relative density uses the actual continuous cells of the observed law.
Definition (Lean source)
Discrete label selection preserves measurability of continuous cell functions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Cell positivity makes the explicit likelihood ratio nonnegative. the stated conclusion holds.
Formal statement
Proof (Lean source)
A law with public uniform design is its explicit cell density times the reference. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The reference is the probability law of uniform covariates and fair labels. the stated conclusion holds.
Definition (Lean source)
Continuous interior cells give a bounded integrable relative density. the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual iid likelihood retains every original covariate and label.
Definition (Lean source)
Finite products of the cell densities are measurable. The stated conclusion follows.
Formal statement
Proof (Lean source)
The iid likelihood is nonnegative, including for an empty sample. the stated conclusion holds.
Formal statement
Proof (Lean source)
Rectangle integration proves the explicit product density for the actual iid law. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The product reference sees the explicit iid likelihood as its actual RN derivative. Under the stated assumptions.
Formal statement
Proof (Lean source)
The sign is averaged once over the entire original sample likelihood.
Definition (Lean source)
A finite prior of measurable likelihoods is measurable. The stated conclusion follows.
Formal statement
Proof (Lean source)
Every finite-prior likelihood is nonnegative. the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite averaging identifies the density of the actual shared-sign experiment. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The RN derivative is the finite average of actual original-sample likelihoods. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The sign-prior weight equals the inverse number of sign vectors used in component factorization. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureHellinger 8 declarations The density floor converts a component likelihood difference into the roadmap's exponential component bound.
Component Hellinger bounds for the original-record mixtures
The density floor converts a component likelihood difference into the roadmap's exponential component bound. Affinity tensorization then adds component bounds, with exactly matching singleton components removed from the sum.
A positive common density floor controls squared square-root discrepancy. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The component density floor and mixed Taylor difference give the exact M⁴ m⁴ 8ᵐ coefficient used by the mixture roadmap. The fair difference bound is smaller and can use this same result. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Integrating the component pointwise estimate against its probability reference preserves its coefficient. No independence inside a component is used. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Affinities of normalized integrable nonnegative densities lie in [0,1]. The upper bound follows from the nonnegative Hellinger discrepancy identity. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[For conditionally independent components, the full Hellinger discrepancy is at most the sum of the component discrepancies. This combines the library's exact tensorized affinity with its finite product defect inequality. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact singleton matching removes those components from the conditional Hellinger bound, leaving precisely the weighted sum over components of size at least two. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A polynomial tail majorant proves the finite cubic geometric sum bound in the occupancy roadmap. It avoids differentiating an infinite power series. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[At occupancy parameter at most one quarter, the finite non-singleton cubic series is bounded by 32 times that parameter, as in the paper. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureLabelTensorization 12 declarations Finite sums over labels implement the conditional experiment at fixed original covariates.
Conditional label tensorization on the original record components
Finite sums over labels implement the conditional experiment at fixed original covariates. Regrouping record labels into ownership fibers preserves Hellinger distance; affinity tensorization then bounds it by the sum over components. The factors may themselves be finite sign mixtures, so independence is needed only between components, never between records in one component.
[Normalized finite label masses have Hellinger discrepancy equal to twice their affinity defect. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The affinity of normalized nonnegative finite label masses lies in [0,1]. Under the stated assumptions.
Formal statement
Proof (Lean source)
The conditional Hellinger discrepancy of finite independent label blocks is bounded by their summed discrepancies, by exact affinity factorization. the documented result Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Regrouping all original labels into record-component fibers loses no information and transports the tensorized bound back to the original sample. the documented result Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Conditional four-cell masses at any fixed covariate form a normalized finite label distribution. the documented result
Formal statement
Proof (Lean source)
Averaging conditional product label masses over finitely many latent signs preserves normalization, including empty record components. the documented result Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
[Every conditional component mixture is nonnegative as a finite average of products of the actual interior four-cell probabilities. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual conditional label mass in one record block, averaged over its owned endpoint signs. Labels outside that block are absent from the argument.
Definition (Lean source)
Conditional component masses normalize even when their block is empty. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional component masses inherit nonnegativity from the actual laws. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Local dependence on owned signs factors the actual conditional label mass on the full original record array into masses on disjoint record blocks. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
At fixed original covariates the full finite-prior label Hellinger discrepancy is at most the sum over sign components. The proof uses the actual local-sign factorization and normalized component laws, without revealing signs or imposing independence between records inside a component. the documented result Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureMassNormalization 6 declarations The uniform four-label reference cancels the number of label arrays exactly.
From component densities to conditional label masses
The uniform four-label reference cancels the number of label arrays exactly. Pointwise bounds for component likelihood densities therefore give the same bound for the summed Hellinger discrepancy of component probability masses.
[Scaling two nonnegative likelihoods scales their squared square-root discrepancy by the same factor. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A product of actual record densities is four to the block size times its conditional label probability, before any hidden-sign averaging. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The owned-sign component density has exactly the same normalization factor as its component label mass, including an empty block. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Summing a pointwise density bound over the four-label arrays costs no factor: the component reference is a probability measure. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Integration of the full conditional likelihood discrepancy equals the sum of discrepancies of its conditional probability masses. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A pointwise bound for the two owned-sign component densities controls the component Hellinger distance after summing its conditional label masses. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureOccupancySeries 5 declarations The factorial and binomial envelopes reduce the non-singleton tree sum to the finite cubic geometric series.
The numerical spanning-tree occupancy sum
The factorial and binomial envelopes reduce the non-singleton tree sum to the finite cubic geometric series. The resulting bound retains the paper's explicit 96 exp(2) B² coefficient and its occupancy threshold.
[The exponential-series bound supplies the factorial envelope needed for rooted parent arrays of a positive number of vertices. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Each non-singleton tree-count term is controlled by a cubic geometric term with occupancy parameter 3 exp(1) B n/k. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The complete finite spanning-tree envelope has the paper's quadratic occupancy bound, with no singleton term. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The prescribed occupancy threshold controls the tree sum with B = 8, exactly the base of the component Hellinger envelope. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Multiplying the tree envelope by the component Taylor coefficient gives the explicit constant for either choice of the amplitude product. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.MixtureProductDerivatives 2 declarations Leibniz differentiation controls a product of bounded record densities by its record count, rather than by an amplitude-dependent exponential constant.
Finite-product derivative bounds for original-record components
Leibniz differentiation controls a product of bounded record densities by its record count, rather than by an amplitude-dependent exponential constant.
[Simultaneous bounds for the value and the first two derivatives of a finite product. The second-order bound counts the diagonal and off-diagonal Leibniz terms, as required by the component-mixture roadmap. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Finite uniform averaging preserves the common second-derivative envelope; subtracting a comparator costs exactly a factor of two. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ParametricExperiment 25 declarations The null has four equiprobable labels; the alternative changes only the treated outcome risk.
Constant-logit Bernoulli comparison experiment
The null has four equiprobable labels; the alternative changes only the treated outcome risk. Both retain the public uniform covariate design and zero nuisance logits, as in the parametric-floor proof roadmap.
[Constant conditional cells with fair treatment and control outcome.
All four cells are continuous, interior, and normalized for every effect. the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual observed-law carrier of the constant-nuisance subexperiment.
Definition (Lean source)
The comparison laws retain the uniform design. the stated conclusion holds.
Formal statement
Proof (Lean source)
The conditional treatment probability is exactly one half. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional outcome risks are the prescribed Bernoulli probabilities. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Both native nuisance logits vanish, and the homogeneous effect is t. the stated conclusion holds.
Formal statement
Proof (Lean source)
Constant zero nuisance logits satisfy every Hölder radius. the stated conclusion holds.
Formal statement
Proof (Lean source)
Legal model membership follows from the effect envelope alone. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The null is legal in every nonnegative radius slice, including radius zero. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The one-record likelihood ratio relative to the four-label fair null.
Definition (Lean source)
The likelihood ratio is continuous, since it depends only on discrete labels. the stated conclusion holds.
Formal statement
Proof (Lean source)
The density is nonnegative at every record. the stated conclusion holds.
Formal statement
Proof (Lean source)
Direct finite cell summation identifies the likelihood ratio, without an abstract model gate. the stated conclusion holds.
Formal statement
Proof (Lean source)
The real Radon--Nikodym derivative is the explicit bounded label density. the stated conclusion holds.
Formal statement
Proof (Lean source)
The squared likelihood deviation is integrable on the actual null law. the stated conclusion holds.
Formal statement
Proof (Lean source)
Direct summation gives the exact one-record chi-square value. the stated conclusion holds.
Formal statement
Proof (Lean source)
The sigmoid derivative is bounded by a quarter on the whole real line. the stated conclusion holds.
Formal statement
Proof (Lean source)
The roadmap's one-record information bound follows from the derivative estimate. the stated conclusion holds.
Formal statement
Proof (Lean source)
The public root-n scalar effect used in the two-point comparison.
Definition (Lean source)
The comparison effect lies in the model envelope at every positive sample size. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The effect and sample-size factors cancel in the information budget. Under the stated assumptions.
Formal statement
Proof (Lean source)
The iid original-record laws have total variation at most one twentieth. Under the stated assumptions.
Formal statement
Proof (Lean source)
Tensoring the same independent uniform seed preserves the testing comparison. Under the stated assumptions.
Formal statement
Proof (Lean source)
Two concrete legal laws discharge the full parametric comparison obligation. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PiProgram 12 declarations A fixed loop advances the two alternating arctangent sums together.
Finite register certificate for the prescribed Machin enclosure
A fixed loop advances the two alternating arctangent sums together. Its public fuel is linear in the prescribed term count, including initialization and clipping.
[Iteration can be divided into consecutive blocks of instructions. the stated conclusion holds.
Formal statement
Proof (Lean source)
The fixed Machin program uses the two term recurrences and clips its final endpoints.
Definition (Lean source)
Loop-head register meanings after a specified number of arctangent terms.
Definition (Lean source)
Initialization clamps arbitrary rational precisions and prepares the prescribed count. the stated conclusion holds.
Formal statement
Proof (Lean source)
One loop block adds precisely the next term of both finite sums. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The exit block returns the literal clipped Machin endpoints and halts. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Iterating the loop exhausts its counter and returns both completed sums. Under the stated assumptions.
Formal statement
Proof (Lean source)
Public fuel for the fixed Machin program, on every rational input list.
The public fuel is computed by a fixed straight-line register program. the stated conclusion holds.
Formal statement
Proof (Lean source)
The fixed public fuel halts the Machin computation for every input list. the stated conclusion holds.
Formal statement
Proof (Lean source)
Certified finite rational program for the Machin primitive.
Definition (Lean source)
The Machin primitive is exactly the interval returned by its finite register program. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerClipProgram 13 declarations The last stage takes the internal precision, integer base, and exponential endpoints.
Register certificate for the final power bracket
The last stage takes the internal precision, integer base, and exponential endpoints. It widens by the prescribed rational error, clips to the exact cubic range, and implements the base-one exception. Its fixed bound is itself a finite rational program. The staged scalar computation uses the certified logarithm and exponential programs. Fusing these stages into a single bounded register program remains a separate obligation.
[The final power bracket, applied to already computed exponential endpoints.
Definition (Lean source)
The literal scalar power is its exponential bracket followed by final clipping. the stated conclusion holds.
Formal statement
Proof (Lean source)
Registers zero and one initially hold precision and base; two and three hold the exponential bracket. The output is sorted by the external rational box.
Definition (Lean source)
On any active starting frame, the clipping stage computes precisely the paper's rational formula; natural-number inputs are interpreted by floor-clamping. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The fixed instruction bound is computed without inspecting any input. the stated conclusion holds.
Formal statement
Proof (Lean source)
Certified total finite register program for the final power bracket.
Definition (Lean source)
The certified program returns the exact clipped scalar formula. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Given the two exponential endpoints, the register stage returns the literal power scalar, including its exceptional constant base. the documented result
Formal statement
Proof (Lean source)
A point-input exponential call returns both endpoints of the scalar bracket. the stated conclusion holds.
Formal statement
Proof (Lean source)
Execute the three certified register stages for one rational exponent. The logarithm stage supplies both the precision and its midpoint; the exponential stage is called on their product with the exponent, then the final stage clips.
Definition (Lean source)
The staged finite register evaluation agrees with the full scalar power formula, on all natural precisions and bases and all rational exponents. the documented result
Formal statement
Proof (Lean source)
Two staged scalar calls supply the monotone endpoint extension. This is a composition of bounded programs, rather than a certificate for a fused code list.
Definition (Lean source)
Every endpoint of the concrete power engine is computed by the certified stages. The remaining recurrence obligation is to fuse these calls and their fuel. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerEnclosure 6 declarations The logarithm midpoint and exponential bracket compose at the prescribed internal precision; clipping preserves containment and endpoint excess.
Certified integer-base power enclosures
The logarithm midpoint and exponential bracket compose at the prescribed internal precision; clipping preserves containment and endpoint excess.
[The prescribed internal precision pays for the cubic base amplification. the stated conclusion holds.
Formal statement
Proof (Lean source)
A positive integer base raised to an exponent in the primitive domain stays in its clip range. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The certified logarithm midpoint approximates the true logarithm. Under the stated assumptions.
Formal statement
Proof (Lean source)
The logarithm argument error gives a uniform cubic bound on the power value error. Under the stated assumptions.
Formal statement
Proof (Lean source)
Clipped scalar power brackets contain the value and satisfy the requested excess bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
Monotone endpoint evaluation gives the complete integer-base power primitive contract. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerEndpointProgram 62 declarations This module joins two certified scalar power calls.
A fused two-endpoint power register program
This module joins two certified scalar power calls. A small bridge retains the lower endpoint of the left call in spare registers while the right call runs.
[Away from the base-one shortcut, the clipping routine reaches its final halt instruction after exactly twenty-six active steps. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact active fuel for the relocated clipping tail outside the base-one shortcut.
Definition (Lean source)
The clipping tail reaches its final active frame with the raw clipped endpoints. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Exact active fuel of the exponential-and-clipping continuation.
Definition (Lean source)
Outside base one, the fused exponential/clipping code reaches its final active halt frame and already contains the scalar power bracket. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact fuel to the scalar program's active final halt frame outside base one.
Definition (Lean source)
Outside base one, the scalar code reaches its active final frame with the prescribed rational bracket. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The exact active scalar run plus its final halt fits inside the published fuel. the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar routine leaves registers forty and above untouched. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Finalize the right scalar call while restoring the saved left lower endpoint.
Definition (Lean source)
A scalar call whose halt continues into endpoint restoration.
Definition (Lean source)
Save the left lower endpoint and restore the original inputs for the right call.
Definition (Lean source)
The bridge and relocated right scalar call.
Definition (Lean source)
Two scalar calls joined at their active final halt frames.
Definition (Lean source)
Dispatch base one directly; otherwise save inputs before entering the fused calls.
Definition (Lean source)
The complete two-endpoint power program.
Definition (Lean source)
Active prelude length outside base one.
The outer prelude saves the common inputs and right exponent. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The four-instruction bridge prepares the second scalar call. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The restoration tail reaches its active halt frame with the requested pair. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Every register mentioned by an instruction lies below a fixed cutoff.
Definition (Lean source)
The anonymous instance result states the corresponding mathematical identity, bound, or structural property.
Definition (Lean source)
Agreement of the control frame and all registers below a cutoff.
Definition (Lean source)
The rational Program step agree below result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The rational Program run agree below result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The scalar code depends only on registers below forty. the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar active-frame certificate is stable under arbitrary spare-register data. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The initial endpoint prelude changes only spare registers before the first call. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The first scalar final halt jumps into the endpoint bridge. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The second scalar final halt jumps into endpoint restoration. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Exact active fuel of the fused core for a pair of scalar inputs.
Definition (Lean source)
The fused core returns the left lower and right upper scalar endpoints. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Arguments for the left scalar endpoint.
Arguments for the right scalar endpoint.
Exact fuel through the final halt of the two-endpoint program.
Definition (Lean source)
The exact fused run halts and returns the desired endpoint extension. the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar public-fuel program reaches its active final halt frame after 55 steps. the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar fuel code also depends only on registers below forty. the stated conclusion holds.
Formal statement
Proof (Lean source)
The active fuel certificate is stable under spare-register data. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
A common magnitude dominating both endpoint exponents.
One scalar-fuel query at the common endpoint magnitude.
Definition (Lean source)
A forty-register initialization matching the transformed frame, including irrelevant registers inherited from an arbitrary input list.
Definition (Lean source)
The power Endpoint Fuel Frame Args fuel result states the corresponding mathematical identity, bound, or structural property.
Formal statement
Proof (Lean source)
Conservative public fuel for both scalar calls and their bridges.
Definition (Lean source)
The power Scalar Series Bound mono abs result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions.
Formal statement
Proof (Lean source)
The power Scalar Public Fuel mono abs raw result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions.
Formal statement
Proof (Lean source)
[Each endpoint's published scalar fuel is covered by the common-magnitude fuel. the stated conclusion holds.
Formal statement
Proof (Lean source)
Compute the common magnitude in register two without disturbing low inputs.
Double the common scalar fuel and add all fixed bridge steps.
Definition (Lean source)
Continue the scalar fuel computation into the fixed arithmetic tail.
Definition (Lean source)
A finite rational program computing the public two-endpoint fuel.
Definition (Lean source)
The power Endpoint Fuel Prelude prepare result states the corresponding mathematical identity, bound, or structural property.
Formal statement
Proof (Lean source)
The power Endpoint Fuel Core connect result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The power Endpoint Fuel Core before halt frame result states the corresponding mathematical identity, bound, or structural property. Under the stated assumptions.
Formal statement
Proof (Lean source)
The power Endpoint Fuel Core result result states the corresponding mathematical identity, bound, or structural property. Under the stated assumptions.
Formal statement
Proof (Lean source)
The power Endpoint Fuel Code result result states the corresponding mathematical identity, bound, or structural property.
Formal statement
Proof (Lean source)
The combined fuel is itself a public rational iteration bound. the stated conclusion holds.
Formal statement
Proof (Lean source)
The conservative public fuel covers the exact fused run. the stated conclusion holds.
Formal statement
Proof (Lean source)
Sufficient public fuel leaves the already halted endpoint output unchanged. the stated conclusion holds.
Formal statement
Proof (Lean source)
Certified bounded program for both power endpoints.
Definition (Lean source)
The endpoint program returns the left lower and right upper scalar endpoints. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
The fused endpoint program implements the concrete power engine. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerExpFrames 21 declarations The existing exponential recurrence can start with arbitrary spare registers.
Exponential register calls on active power frames
The existing exponential recurrence can start with arbitrary spare registers. Its exact output certificate and untouched-register law allow the power computation to retain its precision, base, and second exponent across an exponential call.
Initialization of the exponential loop from an arbitrary active frame. Under the stated assumptions.
Formal statement
Proof (Lean source)
Both endpoint loops are certified without zeroing the spare registers. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The destination register of a writing instruction, if any.
Definition (Lean source)
A register not written by the code survives one step, including halting. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
An untouched register survives any finite recurrence. Under the stated assumptions.
Formal statement
Proof (Lean source)
The exponential routine never writes registers at or above twenty-one. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Relocate only control-flow targets; arithmetic registers retain their meaning.
Definition (Lean source)
Shift a frame into a code block appended after a fixed prelude.
Definition (Lean source)
Instruction lookup in a relocated appended block agrees with the original code. the stated conclusion holds.
Formal statement
Proof (Lean source)
Relocation preserves one step for every frame, including arbitrary branches and halt. the stated conclusion holds.
Formal statement
Proof (Lean source)
Every finite run of an appended relocated block is the relocated original run. the stated conclusion holds.
Formal statement
Proof (Lean source)
Save the power frame, then prepare a point-input exponential call for the left exponent.
Definition (Lean source)
The continuation is one literal code list with every exponential branch relocated.
Definition (Lean source)
Its exact finite instruction count includes preparation and both scalar loops.
Definition (Lean source)
The preparation block preserves all data needed for the later clipping and right call. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The relocated exponential computation certifies the left power argument while retaining the internal precision, base, right exponent, and logarithm midpoint. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A straight-line recurrence computes the continuation's exact step bound.
Definition (Lean source)
The continuation fuel is a total public rational computation on its input frame. the stated conclusion holds.
Formal statement
Proof (Lean source)
The exponential continuation is a certified bounded program on every input list.
Definition (Lean source)
The bounded continuation returns the exact point exponential bracket. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
The certified continuation replaces the standalone exponential call in the power scalar assembly, returning exactly the prescribed clipped formula. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerFusion 22 declarations The exponential stage reaches an active final frame before its halt instruction.
Control-flow certificates for fusion of the power recurrence
The exponential stage reaches an active final frame before its halt instruction. Replacing that halt with a relocated jump joins the prescribed clipping recurrence into one bounded register program. Its public fuel is computed by a separate finite rational recurrence. The logarithm and two endpoint calls remain to be joined.
A halted frame is fixed by any number of further steps. Under the stated assumptions.
Formal statement
Proof (Lean source)
[An active final frame certifies that the initial frame was active. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
Replace an explicit halt with a jump into an appended continuation.
Definition (Lean source)
Join two literal code lists, relocating all branches of the continuation.
Definition (Lean source)
Before the original computation halts, joining a continuation changes no step. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
Any active finite prefix of the original run is identical in the joined program. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The appended block uses the same register frame as the unrelocated continuation. the stated conclusion holds.
Formal statement
Proof (Lean source)
Both endpoint loops reach their active final frame without zeroing spare registers. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The relocated exponential computation certifies the left power argument while retaining the internal precision, base, right exponent, and logarithm midpoint. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Move the exponential bracket and saved power parameters into the clipping frame.
Definition (Lean source)
The clipping continuation with all branch addresses relocated past the bridge.
Definition (Lean source)
The bridge preserves the two exponential endpoints while restoring precision and base. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The appended clipping tail halts and returns the exact raw clipping endpoints. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A single literal register program performs the exponential and clipping stages.
Definition (Lean source)
Replace the last exponential halt by the actual jump into the clipping tail. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Exact instruction bound for the joined continuation.
Definition (Lean source)
The fused code computes the prescribed power bracket from a logarithm frame. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[A straight-line recurrence computes the continuation's exact step bound.
Definition (Lean source)
The continuation fuel is a total public rational computation on its input frame. the stated conclusion holds.
Formal statement
Proof (Lean source)
Certified single register program for the exponential-to-clipping continuation.
Definition (Lean source)
The fused continuation agrees with the literal scalar formula on prepared power data. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
The two-stage logarithm/fused-continuation computation is the prescribed scalar power. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerLogProgram 20 declarations This stage computes the prescribed internal precision and the midpoint of its logarithm bracket.
The logarithm stage of the integer-base power register computation
This stage computes the prescribed internal precision and the midpoint of its logarithm bracket. Its output retains the integer base and both exponent endpoints for the exponential continuation. The complete power certificate remains separate.
[Internal precision used by the literal power algorithm.
The sorted logarithm bracket has the same midpoint as its unsorted endpoints. the stated conclusion holds.
Formal statement
Proof (Lean source)
Single logarithm loop, retaining the original base and exponent endpoints. Register zero returns the internal precision and register one the logarithm midpoint.
Definition (Lean source)
The loop frame keeps the power data while generating the odd logarithm terms.
Definition (Lean source)
Signed rational inputs are clamped to their prescribed natural-number interpretations. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
[The short preparation block clamps the two integers and computes internal precision. the stated conclusion holds.
Formal statement
Proof (Lean source)
The initialization suffix prepares the literal logarithm loop. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Initialization computes exactly the internal precision and the logarithm count. the stated conclusion holds.
Formal statement
Proof (Lean source)
A seven-instruction block adds precisely one logarithm term. Under the stated assumptions. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Both domain branches return the midpoint and retain the continuation inputs. Under the stated assumptions.
Formal statement
Proof (Lean source)
Exhaustion of the exact term count proves termination and the completed sum. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Public fuel of the logarithm preparation stage.
Definition (Lean source)
The stage computes the literal logarithm midpoint, including the totalized zero base. the stated conclusion holds.
Formal statement
Proof (Lean source)
Straight-line computation of the public stage bound.
Definition (Lean source)
The two codes have identical straight-line instructions before the loop head. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The straight-line prefixes agree at each of their bounded instruction positions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The shared initialization prefix is the same computation. the stated conclusion holds.
Formal statement
Proof (Lean source)
The prescribed fuel itself is a finite rational register computation. the stated conclusion holds.
Formal statement
Proof (Lean source)
The preparation stage halts at the proved public count on every rational input.
Definition (Lean source)
The certified program supplies the literal midpoint needed by both scalar exponentials. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerScalarBudget 13 declarations A conservative rational count bounds the literal logarithm and exponential loops on all rational inputs, including inputs outside the primitive's analytic domain.
Public fuel for the full scalar power register program
A conservative rational count bounds the literal logarithm and exponential loops on all rational inputs, including inputs outside the primitive's analytic domain. The scalar code and its argument-specific truncation counts are unchanged.
[The number of odd terms evaluated in the power logarithm.
Definition (Lean source)
Each atanh term has magnitude at most one for a nonnegative integer base. the stated conclusion holds.
Formal statement
Proof (Lean source)
Original-input bound for the exponential argument's integer range.
The bound depends only on the original precision, base, and rational exponent.
Definition (Lean source)
The logarithm midpoint gives no larger range bound than the original-input count. the stated conclusion holds.
Formal statement
Proof (Lean source)
The fixed original-input fuel covers the exact fused scalar run. the stated conclusion holds.
Formal statement
Proof (Lean source)
A literal straight-line program computes the conservative scalar fuel.
Definition (Lean source)
The fuel program uses the same logarithm initialization instructions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Every initialization step is identical in the fuel and scalar programs. Under the stated assumptions.
Formal statement
Proof (Lean source)
The complete original-input bound is computed by finite rational instructions. the stated conclusion holds.
Formal statement
Proof (Lean source)
Sufficient extra steps leave the already halted scalar output unchanged. the stated conclusion holds.
Formal statement
Proof (Lean source)
A certified single register program implements the entire scalar power routine.
Definition (Lean source)
The bounded scalar register evaluation returns the prescribed paper bracket. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.PowerScalarFusion 9 declarations The logarithm reaches an active final frame with its midpoint and power inputs.
Joining logarithm evaluation with the scalar power continuation
The logarithm reaches an active final frame with its midpoint and power inputs. Replacing its halt by a jump executes the exponential and clipping instructions in the same register machine and yields the prescribed scalar power bracket.
The logarithm exit reaches the active halt instruction with the complete power frame. Under the stated assumptions.
Formal statement
Proof (Lean source)
Every logarithm term is evaluated before reaching the active final frame. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The logarithm midpoint and both exponents are ready before the final halt. the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact active-prefix length, including the shorter totalized zero-base branch.
Definition (Lean source)
The logarithm and exponential-to-clipping code form one literal instruction list.
Definition (Lean source)
The active logarithm halt jumps directly to the relocated power continuation. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Exact step count of the joined scalar computation on arbitrary rational inputs.
Definition (Lean source)
The fused literal program halts and returns the specified clipped scalar bracket. The logarithm and exponential contracts here are evaluation identities, not assumptions. the documented result
Formal statement
Proof (Lean source)
Natural precision and base inputs recover the exact paper scalar formula. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ProjectionApproximation 10 declarations Adapter for the public cosine-projection approximation theorem
Adapter for the public cosine-projection approximation theorem
Extend a function on the covariate subtype to the real line. Only its values on [0,1] are used by the study definitions.
The covariate Extension apply result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The covariate Extension continuous On result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The cosine Basis study result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions.
Formal statement
Proof (Lean source)
The uniform Inner basis eq study result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions.
Formal statement
Proof (Lean source)
The cosine Projection study result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The holder Seminorm study result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions.
Formal statement
Proof (Lean source)
The uniform L2 Norm study result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions.
Formal statement
Proof (Lean source)
The study extended L2 Norm congr Icc result states the corresponding mathematical identity, bound, or structural property Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The public constant-five theorem, transported to the run's subtype and uniform-design definitions without assuming a finite Hölder seminorm. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ProjectionCrossMoments 12 declarations Integrating out a residual coordinate makes its product with any square-integrable one-record function vanish.
Cross moments of the projection residual
Integrating out a residual coordinate makes its product with any square-integrable one-record function vanish. These identities cover either shared record, and an independent third record, in the first-order/residual covariance expansion.
Square integrability of the degenerate residual as a function of two records. Under the stated assumptions.
Formal statement
Proof (Lean source)
A square-integrable function of the first record is orthogonal to the residual. Under the stated assumptions.
Formal statement
Proof (Lean source)
A square-integrable function of the second record is orthogonal to the residual. Under the stated assumptions.
Formal statement
Proof (Lean source)
The residual has zero population mean. Under the stated assumptions.
Formal statement
Proof (Lean source)
A third independent record also gives zero cross moment with the residual. Under the stated assumptions.
Formal statement
Proof (Lean source)
Distinct sample coordinates have the product record law. Under the stated assumptions.
Formal statement
Proof (Lean source)
A residual pair is square integrable in the finite experiment. Under the stated assumptions.
Formal statement
Proof (Lean source)
Every one-record term has zero cross moment with a distinct residual pair. Under the stated assumptions.
Formal statement
Proof (Lean source)
The first-order finite sum is square integrable. Under the stated assumptions.
Formal statement
Proof (Lean source)
The residual average is square integrable in the finite experiment. Under the stated assumptions.
Formal statement
Proof (Lean source)
The two finite Hoeffding components are orthogonal. Under the stated assumptions.
Formal statement
Proof (Lean source)
Exact orthogonality assembles the sharp finite-sample variance bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ProjectionMoments 20 declarations Disintegration and iid coordinate transport give the exact mean and bias.
Projection statistic moments
Disintegration and iid coordinate transport give the exact mean and bias. The first uncentered projection has squared energy at most one, and the symmetric kernel has squared energy at most its rank.
Every subtype cosine mode is continuous. the documented result Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Borel tests integrate through the four-cell law whenever their weighted slices are integrable. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Disintegration identifies the design-weighted mean of every Borel bounded mark. Under the stated assumptions.
Formal statement
Proof (Lean source)
Products of a Borel bounded mark and a continuous record function are integrable. Under the stated assumptions.
Formal statement
Proof (Lean source)
Integrating one asymmetric kernel slice gives the projected conditional mark mean. Under the stated assumptions.
Formal statement
Proof (Lean source)
The first uncentered Hoeffding projection is the average of the two projected marks. Under the stated assumptions.
Formal statement
Proof (Lean source)
Independence and finite cosine orthogonality give the mean of the symmetric kernel. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The symmetric marked kernel is Borel measurable on the record pair space. the documented result
Formal statement
Proof (Lean source)
Bounded marks preserve integrability of the symmetric kernel under two independent records. the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging over all distinct ordered iid coordinates preserves the two-record mean. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The original finite-sample ordered statistic has the projected conditional-means inner product. Under the stated assumptions.
Formal statement
Proof (Lean source)
The finite-sample projection statistic has exactly the orthogonal residual bias. Under the stated assumptions.
Formal statement
Proof (Lean source)
Uniform design transports every continuous covariate integral to the record law. Under the stated assumptions.
Formal statement
Proof (Lean source)
The first uncentered projection is dominated by the average projected-mark energies. Under the stated assumptions.
Formal statement
Proof (Lean source)
The squared first projection is integrable under the record law. Under the stated assumptions.
Formal statement
Proof (Lean source)
Centering the first projection subtracts the squared kernel mean from its energy. Under the stated assumptions.
Formal statement
Proof (Lean source)
Its uncentered first projection has squared energy at most one. Under the stated assumptions.
Formal statement
Proof (Lean source)
The centered first Hoeffding projection has squared energy at most one. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The square of the symmetric marked kernel is integrable by its continuous kernel envelope. the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform-design transport and finite cosine orthogonality bound the marked kernel energy by k. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ProjectionOrthogonality 25 declarations Conditional mark means retain the unit-interval range.
Projection orthogonality
Conditional mark means retain the unit-interval range. Finite cosine orthogonality proves the residual bias and projected energy identities. Symmetrization preserves the ordered statistic and its squared envelope.
The conditional mean of a unit-interval mark is nonnegative. Under the stated assumptions.
Formal statement
Proof (Lean source)
Normalization of the conditional cells keeps the conditional mark mean below one. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A Borel mark and continuous conditional cells give a Borel conditional mean. the documented result
Formal statement
Proof (Lean source)
The squared conditional mean has the unit envelope used in the first-order variance bound. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
[The subtype cosine modes inherit the exact orthonormality of the public library. the stated conclusion holds.
Formal statement
Proof (Lean source)
Products of finitely many cosine modes are integrable under the public design. the stated conclusion holds.
Formal statement
Proof (Lean source)
The inner product of the two literal finite projections is the coefficient product sum. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
[Each cosine mode is integrable under the public design. the stated conclusion holds.
Formal statement
Proof (Lean source)
A bounded conditional mark mean can multiply any integrable design function. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Finite projection against a target is the sum of their coefficient products. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The public inner product is symmetric. Under the stated assumptions.
Formal statement
Proof (Lean source)
A target times a finite projection is integrable whenever its mode products are. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Orthogonality of the finite cosine modes gives the exact residual-product bias identity. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Conditional mark means are integrable without continuity of the mark. the stated conclusion holds.
Formal statement
Proof (Lean source)
The conditional means of Borel bounded marks satisfy the residual-bias identity. the stated conclusion holds.
Formal statement
Proof (Lean source)
A finite cosine projection cannot increase the squared energy of a conditional mark mean. the stated conclusion holds.
Formal statement
Proof (Lean source)
Under uniform design each projected conditional mark mean has squared energy at most one. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The finite cosine kernel is symmetric in its covariate arguments. Under the stated assumptions.
Formal statement
Proof (Lean source)
Integrating one squared kernel slice gives the diagonal sum of squared cosine modes. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The squared cosine kernel has exactly rank-k energy under two uniform covariates. the stated conclusion holds.
Formal statement
Proof (Lean source)
The symmetric two-record kernel of the ordered marked statistic.
Definition (Lean source)
Symmetrizing the marks gives an exactly symmetric record kernel. the stated conclusion holds.
Formal statement
Proof (Lean source)
Swapping the two distinct indices preserves the complete ordered-pair sum. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Averaging an ordered kernel with its transpose leaves the statistic unchanged. the stated conclusion holds.
Formal statement
Proof (Lean source)
The symmetrized unit-interval marks never enlarge the squared cosine kernel. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ProjectionResidual 22 declarations The order-two Hoeffding residual has zero conditional mean in both coordinates.
The degenerate projection-kernel residual
The order-two Hoeffding residual has zero conditional mean in both coordinates. Its energy is the kernel energy minus the constant and first-order energies.
[The uncentered first projection of the symmetric marked kernel.
Definition (Lean source)
The constant term of the Hoeffding decomposition.
Definition (Lean source)
The completely degenerate second-order residual.
Definition (Lean source)
Each kernel section is integrable, including at records in null sets. the stated conclusion holds.
Formal statement
Proof (Lean source)
The first projection is measurable by its explicit conditional-mean formula. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Fubini gives integrability of the first projection. the stated conclusion holds.
Formal statement
Proof (Lean source)
The mean of the first projection is the kernel mean. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Symmetry is preserved when removing the two first projections. the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating out the second coordinate kills the residual exactly. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Symmetry gives the other coordinate's degeneracy. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The residual is Borel measurable on the product record space. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Removing square-integrable projections preserves square integrability. Under the stated assumptions.
Formal statement
Proof (Lean source)
Orthogonality removes twice the first-projection energy from the kernel energy. Under the stated assumptions.
Formal statement
Proof (Lean source)
The residual energy is bounded by k, with the exact Hoeffding constant preserved. Under the stated assumptions.
Formal statement
Proof (Lean source)
The run's residual satisfies the library's exact order-two variance interface. Under the stated assumptions.
Formal statement
Proof (Lean source)
The first Hoeffding component is centered under the record law. Under the stated assumptions.
Formal statement
Proof (Lean source)
Exact fixed-order variance specializes to the run's degenerate residual. Under the stated assumptions.
Formal statement
Proof (Lean source)
Removing the square-root rescaling gives the sharp residual second moment. Under the stated assumptions.
Formal statement
Proof (Lean source)
The residual contributes exactly the required 2k/(n(n-1)) upper bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
Each record occurs n-1 times as the first coordinate of the ordered pair sum. Under the stated assumptions.
Formal statement
Proof (Lean source)
Each record occurs n-1 times as the second coordinate of the ordered pair sum. Under the stated assumptions.
Formal statement
Proof (Lean source)
The original statistic has the exact finite-sample Hoeffding decomposition. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.ProjectionSampling 8 declarations The finite product experiment is the pushforward of a canonical infinite IID sample.
Finite sampling transport for projection variance
The finite product experiment is the pushforward of a canonical infinite IID sample. Reindexing ordered pairs transports the exact residual second moment.
Ordered distinct finite indices and natural indices below n have identical sums. Under the stated assumptions.
Formal statement
Proof (Lean source)
The residual ordered average is the library U-statistic along the finite IID observable. Under the stated assumptions.
Formal statement
Proof (Lean source)
Finite product expectations equal expectations along the finite observable of an IID sample. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The sharp residual second moment holds under the original finite product law. Under the stated assumptions.
Formal statement
Proof (Lean source)
The finite experiment's residual contributes at most the sharp rank term. Under the stated assumptions.
Formal statement
Proof (Lean source)
The centered first projection is square integrable. Under the stated assumptions.
Formal statement
Proof (Lean source)
Independence gives the exact first-order contribution in the finite experiment. Under the stated assumptions.
Formal statement
Proof (Lean source)
The first-order term contributes at most 4/n under the finite product law. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.RankEnclosures 7 declarations Valid exponent names intersect the public rectangle.
Domain safety and containment for the represented rank computation
Valid exponent names intersect the public rectangle. Positive affine denominators produce exponent boxes in [0,2]. A derivative bound for integer-base powers and the cubic precision budget then give unit-width enclosures for both exact rank targets.
A shared real point certifies that the literal rational intersection succeeds. Under the stated assumptions.
Formal statement
Proof (Lean source)
Multiplication by a nonnegative point is the exact monotone endpoint operation. Under the stated assumptions.
Formal statement
Proof (Lean source)
A positive denominator above one gives a safe exponent box in [0,2]. Under the stated assumptions.
Formal statement
Proof (Lean source)
The derivative bound on [0,2] controls the exact power range before primitive excess. Under the stated assumptions.
Formal statement
Proof (Lean source)
Power endpoint excess adds at most two precision errors to the exact range width. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The prescribed rank precision satisfies the cubic sample-size error budget. the stated conclusion holds.
Formal statement
Proof (Lean source)
Both rank computations succeed, contain their exact targets, and have width at most one at the prescribed budget, uniformly over admissible engines and naming policies. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.RankRates 9 declarations The represented rank bounds imply uniform bias and noise rates.
Deterministic rank and radius rates
The represented rank bounds imply uniform bias and noise rates. These estimates use only the rank-budget contract, independently of endpoint realization.
Rank selection obeys the exact target and its threefold upper bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
The ordered-pair denominator is at least half the squared sample size. Under the stated assumptions.
Formal statement
Proof (Lean source)
Bias at a rank above its target has exactly the balanced power rate. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
A selected rank at most three times its target gives a uniform noise rate. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Both bias and noise are bounded by the slower of the balanced and parametric rates. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The two prescribed coordinate radii have absolute uniform power bounds. Under the stated assumptions.
Formal statement
Proof (Lean source)
The diagnostic powers are at most one, and the numerator absorbs inverse sample size. Under the stated assumptions.
Formal statement
Proof (Lean source)
The sensitivity formula assembles into the diagnostic profile without a remainder. Under the stated assumptions.
Formal statement
Proof (Lean source)
A single absolute constant bounds the full rank-dependent sensitivity expression. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.SeriesEnclosures 16 declarations The last half of the factorial dominates the public range bound.
Factorial tails for the prescribed scalar series
The last half of the factorial dominates the public range bound. The resulting geometric remainder certifies both literal polynomials. Monotonicity extends the exponential enclosure, and cosine Lipschitz continuity extends its midpoint bracket.
[The last half of the factorial supplies the roadmap's power lower bound. the stated conclusion holds.
Formal statement
Proof (Lean source)
The rational range bound dominates the absolute scalar argument. the stated conclusion holds.
Formal statement
Proof (Lean source)
A factorial term at the prescribed quadratic cutoff is at most a dyadic power. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The public cutoff makes twice the first omitted term smaller than the scalar error. the stated conclusion holds.
Formal statement
Proof (Lean source)
The geometric tail estimate for the real exponential series, including negative inputs. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Successive tail terms have ratio at most one half at the public cutoff. the stated conclusion holds.
Formal statement
Proof (Lean source)
The specified exponential polynomial approximates its scalar value at the internal precision. the stated conclusion holds.
Formal statement
Proof (Lean source)
The positive floor in the scalar exponential bracket lies below its true value. the stated conclusion holds.
Formal statement
Proof (Lean source)
The internal two-sided error is smaller than the primitive tolerance. the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar bracket contains the exponential, has positive floor, and bounded endpoint excess. the stated conclusion holds.
Formal statement
Proof (Lean source)
Monotonicity extends scalar containment and excess to the two endpoint evaluations. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The literal concrete exponential routine meets the primitive image and excess contract. the stated conclusion holds.
Formal statement
Proof (Lean source)
The real part of the even-length imaginary exponential polynomial is the cosine polynomial. the stated conclusion holds.
Formal statement
Proof (Lean source)
The cosine remainder is the real part of an exponential remainder at an imaginary argument. the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping the scalar cosine bracket preserves containment and bounds both endpoint excesses. the stated conclusion holds.
Formal statement
Proof (Lean source)
The midpoint bracket, enlarged by the half width and clipped, satisfies the cosine primitive. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.SignComponents 18 declarations Original records sharing an endpoint sign are adjacent in the cell graph.
Factorization of the finite endpoint-sign prior
Original records sharing an endpoint sign are adjacent in the cell graph. Distinct connected components therefore use disjoint signs. Regrouping the uniform prior by sign ownership factors arbitrary component likelihoods.
[The two endpoint indices on which a record depends.
Equal and adjacent cells join distinct original records.
Definition (Lean source)
Distinct latent-sign components have disjoint endpoint sets. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Regrouping independent uniform signs into arbitrary ownership fibers factors all component averages, including empty fibers for unused signs. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Extend one component's signs arbitrarily outside its ownership fiber.
Definition (Lean source)
Likelihood products factor under the finite prior when each record uses only signs assigned to its block. This allows dependence between records in a block. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
A record's sign field depends only on its two endpoint signs. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Both mixed hypotheses use precisely the same local endpoint support. Under the stated assumptions.
Formal statement
Proof (Lean source)
The random fair family and the comparator use no signs outside these endpoints. Under the stated assumptions.
Formal statement
Proof (Lean source)
Local cell likelihoods factor whenever each endpoint is owned by its record's block. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The conditional likelihood of the actual mixed formula factors without replacing original records or asserting independence inside a block. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The same exact finite-prior factorization holds for the actual fair cells, including the deterministic comparator and both amplitude axes. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Components plus one empty record block accommodate unused endpoint signs.
Definition (Lean source)
The finite component quotient supports literal finite sign averages.](goal) Under the stated assumptions.
Definition (Lean source)
[Assign a used endpoint sign to any incident record's component; unused signs are assigned to the empty block. Reachability makes this choice harmless.
Definition (Lean source)
Each record's two signs are owned by its actual graph component. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Conditional finite-prior likelihoods factor over the actual connected components. The unused-sign block contributes an empty record product equal to one. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.SpatialGluing 6 declarations Closed cells cover the covariate interval.
Shared-endpoint spatial gluing
Closed cells cover the covariate interval. Matching endpoint values allow continuous local formulas to pass through the discontinuous cell selector.
On a closed cell the selector is its index, except possibly at its right endpoint. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
A finite chain of continuous local profiles glues when adjacent endpoint values agree. No matching derivatives at endpoints are required. the documented result Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The shared endpoint sign field is continuous for every realization. Under the stated assumptions.
Formal statement
Proof (Lean source)
A periodic endpoint profile remains continuous after the cell-coordinate selector, despite that selector jumping from one to zero. the documented result Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Mixed local tables glue because their root has equal endpoint values and the two adjacent sign profiles share the same sign there. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Both fair local tables glue: their centers agree at the two endpoints, and the random risks use the same shared sign. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.SpatialLipschitz 8 declarations Local Lipschitz bounds telescope across the finite chain of cells.
Shared-endpoint Lipschitz gluing
Local Lipschitz bounds telescope across the finite chain of cells. This is the roadmap's subdivision argument and does not require matching endpoint derivatives.
Given a finite number of cells, a profile on each cell, and a common local constant, local bounds and matching endpoint values telescope for cell indices satisfying their order and range condition, and for cell coordinates satisfying the first unit-interval condition, the second unit-interval condition, and global coordinate order, to exactly the distance between the two cell coordinates.
Formal statement
Proof (Lean source)
The cell selector is monotone in the covariate. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A common local Lipschitz constant becomes a global constant multiplied by rank after gluing the shared endpoints, including points in different cells. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A profile whose endpoint values agree inherits the global rank-scaled Lipschitz bound through the discontinuous within-cell coordinate selector. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The shared sign field has a global Lipschitz constant at most four times rank, obtained from the two trigonometric profiles and endpoint gluing. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The fair root's quadratic spatial derivative bound becomes a global quadratic Lipschitz bound; its two endpoint values agree. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Global fair root and sign bounds give a linear spatial bound for the native prognosis logit of either construction, with zero on fallback laws. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
One absolute positive radius proves the fair prognosis linear scale bound for every nonnegative exponent and every rank, for both calibrated laws. the documented result Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.SqrtProgram 13 declarations The binary-loop invariant identifies its result with the integer-square-root instruction.
Finite register certificate for the prescribed square-root routine
The binary-loop invariant identifies its result with the integer-square-root instruction. A fixed straight-line program computes both dyadic endpoints, with a constant, independently certified public fuel bound.
A binary step preserves the integer square-root bracket. Under the stated assumptions.
Formal statement
Proof (Lean source)
A nonterminal binary step halves a power-of-two width budget. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The structurally recursive fixed-count loop preserves the bracket and exhausts its width. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The prescribed number of binary steps returns the unique integer square-root bracket. the stated conclusion holds.
Formal statement
Proof (Lean source)
The paper's binary recurrence agrees with the integer-square-root instruction. the stated conclusion holds.
Formal statement
Proof (Lean source)
Straight-line dyadic square-root endpoint program; inputs are precision, lower, upper.
Definition (Lean source)
Every rational input halts after the fixed instruction count. the stated conclusion holds.
Formal statement
Proof (Lean source)
The public fuel bound is itself computed by a two-step rational program. the stated conclusion holds.
Formal statement
Proof (Lean source)
The certified square-root register program.
Definition (Lean source)
Executing the program on valid precision inputs returns the two raw dyadic endpoints. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
The scalar dyadic bracket endpoints are in their literal monotone order for all inputs. the stated conclusion holds.
Formal statement
Proof (Lean source)
The concrete square-root map has a bounded finite rational register implementation. the stated conclusion holds.
Formal statement
Proof (Lean source)
Assemble the remaining five certificates with the independently proved square-root program. the stated conclusion holds. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.Helpers.TwoPointLength 9 declarations Coverage is transferred between the full sample-and-seed experiments by total variation.
Two-law testing bounds for honest interval length
Coverage is transferred between the full sample-and-seed experiments by total variation. Intervals covering two effects have length at least their separation, which yields a lower bound on expected, worst-case, and minimax length.
[Encoded intervals have length at most the width of the public effect region. the stated conclusion holds.
Formal statement
Proof (Lean source)
Membership implies the usual weak endpoint inequalities, including open endpoints. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Any connected encoded interval containing two points spans their separation. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The independent uniform seed and finite iid records form a probability experiment. the stated conclusion holds.
Formal statement
Proof (Lean source)
Length is integrable because procedures are measurable and length lies in [0,1]. the stated conclusion holds.
Formal statement
Proof (Lean source)
Expected length stays within the public unit width. the stated conclusion holds.
Formal statement
Proof (Lean source)
Every law in the radius slice gives a lower bound on its supremum risk. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Two coverage events under nearby full experiments give a length lower bound. The seed is already included in the two laws; independent randomization is allowed. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Honest coverage at two model laws turns a testing comparison into a minimax floor. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_CalibratedSupport 27 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
T CalibratedSupport
Paper-owned scaffold obligations; proofs are filled in Stage 3.
[The one-record reference is uniform covariate and uniform four-label measure.
Definition (Lean source)
Actual mixed-law density, with roots and construction fully substituted.
Actual fair-law density, including the comparator.
Substantive membership, effect, and singleton-matching claims at the rate-scaled amplitudes.
Definition (Lean source)
The model and homogeneous-effect obligations, separated from singleton matching, which follows from the exact calibration equations.
Definition (Lean source)
On one fixed signed neighbourhood the actual cell laws are valid, and their relative densities and first two amplitude derivatives have one universal envelope.
Definition (Lean source)
Actual fair record densities are twice continuously differentiable on the closed support neighborhood, inside the smooth signed calibration domain.
Definition (Lean source)
Actual mixed record densities are twice continuously differentiable on the signed support square, including full neighborhoods of its boundary.
Definition (Lean source)
The actual one-record densities are infinitely differentiable on open amplitude neighborhoods containing the very same closed signed support box. The fair clause includes both the random law and the deterministic comparator.
Definition (Lean source)
Exact singleton cancellation throughout the signed support neighborhood.
Definition (Lean source)
The actual fair laws inherit the literal four-cell bounds, even on totalization fallback inputs. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The actual mixed laws inherit the literal four-cell bounds, including fallback inputs. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The established mixed density bounds and exact table normalization reduce validity to spatial continuity. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The established fair density bounds and exact arm normalization reduce validity, for the random law and comparator alike, to spatial continuity. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A valid mixed construction on a neighborhood has the smooth amplitude slice of its fully substituted local cell formula. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Both fair constructions inherit amplitude smoothness from the local calibration formula wherever their cell-law constructor is valid nearby. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A smaller closed amplitude region lies strictly inside the validity region. Smooth local calibration formulas therefore give smooth actual record densities even at the boundary of the closed region. the documented result
Formal statement
Proof (Lean source)
Nearby validity identifies the derivatives of an actual mixed density with the derivatives of its local formula, with the spatial coordinate fixed. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Nearby validity identifies an actual fair or comparator density with its local amplitude slice to every derivative order. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Validity on the larger signed box transfers the compact local density envelopes to both actual density families on every smaller closed box. the documented result
Formal statement
Proof (Lean source)
One absolute calibration radius and derivative envelope support every legal exponent pair and certify infinitely differentiable densities on open neighborhoods containing that same closed signed amplitude box. the documented result
Formal statement
Proof (Lean source)
The support radius chosen from the actual support theorem.
Definition (Lean source)
The derivative envelope chosen together with that same radius.
Definition (Lean source)
Export the jointly selected constants, rather than mismatching separate existential witnesses. the stated conclusion holds.
Proof (Lean source)
The same chosen support radius supplies exact singleton matching, with no rate scaling restriction on the signed amplitudes. the documented result
Formal statement
Proof (Lean source)
The jointly chosen radius is inside the explicit cell-bound square, its common derivative envelope is at least one, and fair densities are smooth. the documented result
Proof (Lean source)
The same selected support square supplies mixed-density smoothness. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_ConcreteArithmeticEngine 5 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
T ConcreteArithmeticEngine
Paper-owned scaffold obligations; proofs are filled in Stage 3.
The scalar square-root algorithm contains the true root and has the exact dyadic width. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The rational and real precision errors represent the same dyadic number. the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar dyadic width is below the requested primitive tolerance. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Monotone endpoint extension of the certified scalar brackets satisfies the square-root contract. Under the stated assumptions.
Formal statement
Proof (Lean source)
The literal fixed-count rational routines satisfy every primitive engine contract. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_ExactCalibrations 35 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
T ExactCalibrations
Paper-owned scaffold obligations; proofs are filled in Stage 3.
[The normalized branch has the prescribed value on the zero-effect axis. the stated conclusion holds.
Formal statement
Proof (Lean source)
Multiplication by the effect removes the divided difference without excluding zero. the stated conclusion holds.
Formal statement
Proof (Lean source)
Off zero the normalization is exactly division by the effect. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The table retains its first margin for every covariance. the stated conclusion holds.
Proof (Lean source)
The table retains its second margin for every covariance. the stated conclusion holds.
Proof (Lean source)
The four cells sum to one for every covariance. the stated conclusion holds.
Proof (Lean source)
A root of the normalized mixed equation gives exact singleton covariance matching. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[The two independent fair signs have zero averaged field. the stated conclusion holds.
Formal statement
Proof (Lean source)
The cosine-sine sign interpolation has unit second moment. the stated conclusion holds.
Formal statement
Proof (Lean source)
On the zero-propensity-amplitude axis, the equation is affine in the root. the stated conclusion holds.
Formal statement
Proof (Lean source)
The prescribed local selector has the exact zero-axis value for small signed amplitudes. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[At either cell endpoint the finite sign average gives the same root equation. the stated conclusion holds.
Formal statement
Proof (Lean source)
The literal selectors agree at cell endpoints because their equations agree. the stated conclusion holds.
Proof (Lean source)
An existing bracket root makes the totalized selector a genuine bracket root. the stated conclusion holds. Under the stated assumptions.
Formal statement
Proof (Lean source)
On the other zero-amplitude axis the mixed equation reduces to the stated quadratic. the stated conclusion holds.
Formal statement
Proof (Lean source)
The zero-prognosis-amplitude quadratic has a bracket root by the intermediate value theorem. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The actual selected root satisfies the zero-axis quadratic, including signed amplitudes. Under the stated assumptions.
Formal statement
Proof (Lean source)
Small effects have a uniformly small exponential increment. Under the stated assumptions.
Formal statement
Proof (Lean source)
The rationalized branch has a positive denominator and small covariance. Under the stated assumptions.
Formal statement
Proof (Lean source)
Every centered product is separated from zero on the chosen margin neighbourhood. Under the stated assumptions.
Formal statement
Proof (Lean source)
All four actual cells are positive throughout a fixed absolute neighbourhood. Under the stated assumptions.
Formal statement
Proof (Lean source)
Rationalizing the small quadratic root preserves its defining polynomial at zero. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
The covariance branch solves the odds-ratio quadratic on the absolute neighbourhood. Under the stated assumptions.
Formal statement
Proof (Lean source)
The determinant identity turns the solved quadratic into the exact odds ratio. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Reversing the effect scales its smooth exponential divided difference. the stated conclusion holds.
Formal statement
Proof (Lean source)
Scaling the quadratic coefficients by a positive factor preserves the normalized branch. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
Complementing the first binary margin reverses the effect in the normalized branch. the stated conclusion holds.
Formal statement
Proof (Lean source)
Exchanging the two margins preserves the normalized covariance branch. the stated conclusion holds.
Formal statement
Proof (Lean source)
Complementing the second binary margin also reverses the effect. the stated conclusion holds.
Formal statement
Proof (Lean source)
The mixed root equation is even in its propensity amplitude. the stated conclusion holds.
Formal statement
Proof (Lean source)
The mixed root equation is even in its prognosis amplitude. the stated conclusion holds.
Formal statement
Proof (Lean source)
Identical equations give identical literal mixed-root selectors. the stated conclusion holds.
Proof (Lean source)
The literal mixed-root selector is even in the prognosis amplitude. the stated conclusion holds.
Proof (Lean source)
Existing uniform uniqueness, confinement, and pointwise smoothness supply one common signed branch certificate with explicit ambient open neighborhoods, including the fair equation's removable extension on the full centered bracket. the documented result
Formal statement
Proof (Lean source)
Exact signed singleton matching, unique selected branches on fixed brackets, open smooth neighborhoods, smooth zero-axis extensions, and the effect separation. the documented result
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_FiniteHonestUpper 20 declarations Confidence-rectangle inversion covers the observable causal effect.
T FiniteHonestUpper
Confidence-rectangle inversion covers the observable causal effect. Finite second moments and Chebyshev concentration give ninety-percent coverage once the coordinate bias bounds are supplied. The literal single-record branch is honest with unit length. Native-logit Hölder bounds and projection approximation prove both coordinate biases. Unconditional rectangle sensitivity and absolute numerator moments give a radius-sensitive expected-length inequality; proved rank-budget estimates give an absolute uniform diagnostic rate bound. Endpoint realization remains an imported open dependency.
Clipped logarithmic inversion preserves the ordering of its quotient argument. Under the stated assumptions.
Formal statement
Proof (Lean source)
[On a positive denominator interval the extrema occur at its two endpoints, with the direction determined by the sign of the numerator. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The two selected corners cover the inversion of every point of a positive confidence rectangle. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The clipped inversion identifies the causal effect on the model, since the observable odds already lie inside the public exponential effect envelope. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Denominator clipping retains any true coordinate in the public interval that was contained in the original error interval. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A coordinate confidence event covers the inverted target at the exact minimum and maximum corners used by the upper construction. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The integrated off-diagonal product is at most one under the public design. the stated conclusion holds.
Formal statement
Proof (Lean source)
The paper's two coordinate error bounds imply coverage of the causal effect by the exact ideal interval, prior to outward rational rounding. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The literal single-record output is the full public effect interval. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The single-record procedure has coverage one because it returns the full effect envelope on every input. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The literal single-record interval has length one. Under the stated assumptions.
Formal statement
Proof (Lean source)
[At one record the expected length obeys the diagnostic bound for any constant at least one and any nonnegative radius. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A bias bound and the sharp variance radius give the one-twentieth coordinate failure probability used in the paper's Chebyshev step. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The public variance radius is strictly positive for every multi-record sample. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The union of the two coordinate failure events has probability at most one tenth. Endpoint realization then transfers rectangle coverage to the literal output. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
The ranks selected before sampling are positive, using only the rank contract. Under the stated assumptions.
Formal statement
Proof (Lean source)
The effect envelope controls the observable numerator linearly, with the roadmap's constant. Under the stated assumptions.
Formal statement
Proof (Lean source)
Bias and sharp variance control the unconditional absolute numerator mean. Under the stated assumptions.
Formal statement
Proof (Lean source)
Integrating the samplewise rectangle bound gives the unconditional radius-sensitive length bound. Under the stated assumptions.
Formal statement
Proof (Lean source)
An absolute expected-length bound and global honesty for every supplied implementation. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_FixedBudgetRealization 9 declarations Unit-width enclosure rounding controls the selected ranks.
T FixedBudgetRealization
Unit-width enclosure rounding controls the selected ranks. Ideal endpoint ordering, rational output shape, and outward clipping assemble realization from the proved rank-budget contract and the proved literal endpoint box-evaluation estimates.
[The literal output has rational closed ordered endpoints in the public effect region.
Definition (Lean source)
The rational output has the prescribed shape even on totalized inputs. the stated conclusion holds.
Formal statement
Proof (Lean source)
Ceiling the upper endpoint of a unit-width enclosure gives the strict two-unit rank excess in the roadmap; the target's unit lower bound controls the multiplicative excess. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Both exact rank targets are at least one on the public exponent domain. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Clipped odds inversion stays inside the public effect interval. the stated conclusion holds.
Formal statement
Proof (Lean source)
For a positive denominator, clipped odds inversion is nondecreasing in its numerator. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Proof (Lean source)
[The ideal interval is ordered on every sample and lies in the public effect region. the stated conclusion holds.
Formal statement
Proof (Lean source)
Outward endpoint enclosures survive intersection with the effect region, and their widths bound the extra length. This step uses no arithmetic approximation estimate. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
Primitive contracts alone suffice at both prescribed budgets, and the floor policy is valid. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_FullHonestFrontierAnswer 1 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
T FullHonestFrontierAnswer
Paper-owned scaffold obligations; proofs are filled in Stage 3.
The explicit power profile and one concrete data-only sequence answer the full honest-frontier question. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_FullHonestFrontierSolution 1 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
T FullHonestFrontierSolution
Paper-owned scaffold obligations; proofs are filled in Stage 3.
The full solution includes the concrete sequence and the same absolute guarantees for every implementation. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_ObservableOdds 26 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
T ObservableOdds
Paper-owned scaffold obligations; proofs are filled in Stage 3.
Both conditional arm risks are strictly interior. Under the stated assumptions.
Formal statement
Proof (Lean source)
The Bernoulli factorization recovers each of the original four cells. Under the stated assumptions.
Formal statement
Proof (Lean source)
The conditional outcome mean is the sum of the two outcome-one cells. Under the stated assumptions.
Formal statement
Proof (Lean source)
Expanding the two margins yields the determinant of the binary table. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Log odds invert the logistic map on every real argument. the stated conclusion holds.
Proof (Lean source)
Homogeneity gives the same log-odds contrast at every covariate. Under the stated assumptions. The stated conclusion follows.
Formal statement
Proof (Lean source)
Homogeneous log odds give the four-cell odds-ratio identity pointwise. Under the stated assumptions.
Formal statement
Proof (Lean source)
Division by the positive denominator recovers the scalar effect. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The observed outcome obeys literal potential-outcome consistency. the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional treatment is independent of the potential-outcome pair. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
A Bernoulli law has its parameter as the binary expectation. Under the stated assumptions.
Formal statement
Proof (Lean source)
Admissible coupling margins give the two potential-outcome means. Under the stated assumptions.
Formal statement
Proof (Lean source)
Continuous marks integrate against the explicit conditional cell disintegration. Under the stated assumptions.
Formal statement
Proof (Lean source)
The treatment-outcome product has conditional expectation equal to the (1,1) cell. Under the stated assumptions.
Formal statement
Proof (Lean source)
Integrating the homogeneous determinant identity gives the observable covariance coordinate. Under the stated assumptions.
Formal statement
Proof (Lean source)
Logistic and log odds are inverse at interior probabilities. Under the stated assumptions.
Proof (Lean source)
[Numerical exponential bounds certify the two envelope endpoint values. the stated conclusion holds.
Formal statement
Proof (Lean source)
The native logit envelopes bound all four Bernoulli factors away from zero. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
The off-diagonal product exceeds the public numerical denominator floor pointwise. Under the stated assumptions.
Formal statement
Proof (Lean source)
Integration of the pointwise floor under the known uniform probability design. Under the stated assumptions.
Formal statement
Proof (Lean source)
Integrating a binary test function against the explicit Bernoulli law. Under the stated assumptions.
Formal statement
Proof (Lean source)
Coupling margins determine every nonnegative test of either potential outcome. Under the stated assumptions.
Formal statement
Proof (Lean source)
The conditional observation test recovers the four original cells. Under the stated assumptions.
Formal statement
Proof (Lean source)
The conditional cell construction integrates any nonnegative measurable test. Under the stated assumptions.
Formal statement
Proof (Lean source)
The full-data extension has precisely the original observed marginal. Under the stated assumptions.
Formal statement
Proof (Lean source)
On the public exponent domain 0 < β < 1/4 and β < α ≤ 1, each model law has the observable odds identity, denominator floor, and causal interpretation. The full conditional laws disintegrate the causal extension by the canonical reassociation from X × ((Y⁰, Y¹) × A) to (X × (Y⁰, Y¹)) × A. the documented result Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_OriginalRecordMixtures 22 declarations Paper-owned scaffold obligations; proofs are filled in Stage 3.
T OriginalRecordMixtures
Paper-owned scaffold obligations; proofs are filled in Stage 3.
[Non-singleton occupancy weight of a sign block; the unused-sign block has no records and contributes zero.
Definition (Lean source)
The occupancy weight vanishes exactly on the empty and singleton record fibers. Their Hellinger contribution must be canceled rather than bounded crudely. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Adding the empty unused-sign block leaves the exact component occupancy sum unchanged, so singleton cancellation is retained. the documented result
Formal statement
Proof (Lean source)
[The actual mixed conditional likelihood factors over the original-record sign graph, with every root and cell formula substituted. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[The actual fair mixture and comparator conditional likelihoods factor over that same graph, uniformly through zero amplitudes and effects. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Tensorization applies to the actual mixed laws conditional on every original covariate, with labels regrouped only along latent-sign components. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[The fair mixture is tensorized against its deterministic comparator on exactly the same original covariate-dependent components. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Common dominating reference for exactly n records.
Definition (Lean source)
Unhalved squared Hellinger distance, through the actual Radon--Nikodym densities.
Definition (Lean source)
Identical original-record measures have zero squared Hellinger distance. the stated conclusion holds.
Formal statement
Proof (Lean source)
The mixed distance is exactly the integral of the actual finite-prior likelihoods. the stated conclusion holds.
Formal statement
Proof (Lean source)
The fair distance uses the averaged random likelihood and the actual iid comparator likelihood. the stated conclusion holds.
Formal statement
Proof (Lean source)
The mixed full-sample distance integrates the conditional label distance against the common original covariate law, with no loss of observations. the documented result
Formal statement
Proof (Lean source)
The fair mixture and comparator also share exactly the original covariate marginal, so their distance is the integral of their conditional label distance. the documented result
Formal statement
Proof (Lean source)
A one-record likelihood is just the original record's four-cell density. the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact mixed singleton matching identifies the actual one-record mixture densities. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
[Exact fair singleton matching identifies the actual one-record mixture with the comparator density, uniformly in the effect. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
With one original record the mixed Hellinger discrepancy vanishes exactly. Under the stated assumptions.
Formal statement
Proof (Lean source)
With one original record the fair Hellinger discrepancy vanishes exactly. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
Public occupancy threshold.
Definition (Lean source)
The explicit envelope constant uses the support theorem's same M.
Both original-record mixture bounds, uniformly in effect, with no singleton remainder. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_ParametricNullFloor 1 declarations The constant-logit Bernoulli comparison and total-variation transfer give the finite-sample root-n minimax length floor, including the radius-zero slice.
T ParametricNullFloor
The constant-logit Bernoulli comparison and total-variation transfer give the finite-sample root-n minimax length floor, including the radius-zero slice.
A root-n length floor, including the radius-zero evaluation slice. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_ProjectionControl 1 declarations The cosine approximation, mean and bias identities, and sharp variance bound follow from projection orthogonality and the exact finite-sample Hoeffding decomposition.
Projection control
The cosine approximation, mean and bias identities, and sharp variance bound follow from projection orthogonality and the exact finite-sample Hoeffding decomposition. Both variance components have zero cross moment.
Jackson approximation and all three moment identities for the original ordered-pair statistic. Under the stated assumptions. Under the stated assumptions. The stated hypotheses hold, and the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_ScalarImplicitFunction 5 declarations The scalar product-domain implicit-function theorem, with open coordinate neighborhoods and local uniqueness of the zero graph.
T ScalarImplicitFunction
The scalar product-domain implicit-function theorem, with open coordinate neighborhoods and local uniqueness of the zero graph.
A scalar zero set is locally the graph of a unique C1 function. Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[A continuous zero-graph inherits every smoothness order of its scalar implicit equation. This identifies the actual selected root with Mathlib's local branch, rather than proving regularity of an unrelated witness. the documented result Under the stated assumptions. Under the stated assumptions.
Formal statement
Proof (Lean source)
[Smooth scalar equations have a single smooth local zero-graph on open coordinate neighborhoods. The C1 graph is upgraded pointwise by local implicit uniqueness, so all finite derivative orders concern the same root. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[A bracket selector inherits smoothness from the local implicit branch when nearby bracket roots are unique. No continuity assumption on the selector is needed: uniqueness identifies it with the smooth branch on a neighborhood. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
[Compactness bounds each fixed derivative order of the actual smooth map. Smoothness is required on neighborhoods of the compact set, so the derivatives are unrestricted derivatives even at boundary points. the documented result Under the stated assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LogoddsLowsmoothFrontier_Research.T_SharpHonestFrontier 1 declarations The upper comparisons, operational guarantees, parametric numerator branch, and combination of the lower rates use supporting lemmas.
T SharpHonestFrontier
The upper comparisons, operational guarantees, parametric numerator branch, and combination of the lower rates use supporting lemmas. The mixture lower rates follow from calibrated supports, original-record Hellinger bounds, finite-prior testing, and uniform ceiling-rank estimates.
Positive absolute constants certify the entire domain and every radius, including randomized competitors. the stated conclusion holds.