Exact Real Probe Costs
Abstract
Exact real probes have certificate cost two, deterministic cost three, weak random cost one, and strong random cost two.
Theorem 1.1 (Sharp certificate and discovery costs).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Decision/ExactRealProbeCosts.result (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Frederic Magniez, Ashwin Nayak, Miklos Santha, Jonah Sherman, Gabor Tardos, and David Xiao (2013). Improved bounds for the randomized decision tree complexity of recursive majority. URL: https://arxiv.org/abs/1309.7565v1.
Commentary.
The target is definition and theorem 22.3 of FIB_SCALE_READOUT_PERMISSION_GEOMETRY. Source is the closed unit interval times Bool. The coordinate and label of s are its first and second projections. Querying a returns the label except at the coordinate, where it flips the bit. History uses the dependent passive history carrier and retains each exact parameter and its response; queryCount counts different parameters. Consistent(h,s) checks every response, and Sound(h,b) requires label b on the entire compatibility fiber.
Controller is a local notation for a history-to-Sum policy: each action queries an exact parameter or returns a Boolean label. Finite Run(pi,s,prefix,h,b) means that some fuel makes the frozen PassivePolicyNormalization.execute return the additional history h and label b. Correct(pi) requires such a correct return on every source. There is no uniform fuel bound. Repetition is allowed and charged once; the local cost definition counts distinct exact parameters in the terminal history and is infinite when no fuel returns. worstCost(pi) is the supremum over sources. deterministicValue minimizes it over measurable correct policies.
Internal stalls can be represented by endless queries after the first stalled prefix. This preserves all finite returns, costs, and error events; conversely every Sum policy embeds as an Option controller using some. Thus certificates and all three optimal values agree. The attaining policies terminate at every declared seed and source. The executor is reused from the frozen normalization module; this module supplies the exact-probe response and distinct-parameter cost.
The midpoint is 1/2. threeProbe(a,c,d) queries a and c, returns the first response when they agree, and otherwise queries d and returns that response. Every sound certificate needs two distinct parameters. Two parameters avoiding the coordinate certify its label. For a correct controller with first parameter a, a terminal record at (a,true) using only a and c would also match (c,false). This forces a third parameter. The fixed controller at 0,1/2,1 attains the bound.
A random family pi uses one input-independent probability law mu. CorrectAE(mu,pi,s) means almost every seed has a finite correct run on s. Weak(mu,pi) requires this for every source separately; Strong(pi) requires Correct(pi(omega)) at every declared seed. expectedCost(mu,pi,s) is the nonnegative extended integral of the execution cost. The randomizedValue(false) and randomizedValue(true) infima range over all seed spaces, measurable control maps, probability laws, and respectively weak or strong contracts, after taking the supremum over sources.
volumeI is the Lebesgue probability law on the closed unit interval. oneProbe(u) queries u and returns its response. Its error seeds at source s are exactly the singleton coordinate(s), with measure zero. Every declared seed nevertheless has an erroneous source. Zero-query returns cannot lower a weak strategy’s expected cost: almost sure correctness at two opposite labels excludes them.
StrongSeed denotes the half-open unit interval subtype [0,1), with the standard subtype measure. shift(u) adds 1/2 below 1/2 and subtracts 1/2 above or at 1/2. strongFamily(u) is threeProbe(u,shift(u),1), and volumeJ is its Lebesgue probability law. Every seed is correct on every source. The cost is two except when the coordinate equals u or shift(u), when it is three. For a fixed source the exceptional seeds form a finite null set. Thus its expected cost is two, whereas every fixed seed has worst cost three.
ErrorSeeds(pi,s) is the set of seeds with a finite erroneous return. MeasurableStrategy requires measurable control on the product of the seed sigma algebra and each Borel finite record space, and measurable costs, termination events, and error events for each source. ControlsMeasurably is its control condition. constantFamily(pi) is the constant family on Unit. jointResponse(a,s) is response(a,s), on the product domain. Both attaining families and the joint response satisfy these measurability conditions. The fixed-input expectation convention is acknowledged from Magniez and coauthors; the exact probe sharp values are repository deductions.