CARD separates mathematical proof from the transform a robot executes

A certificate needs a clearly defined job

In the CARD preprint, Yushan Li examines the boundary between certifiable geometric estimation and executable robotic service. The central proposal is not to discard mathematical certificates, but to prevent them from carrying meanings they do not establish.

A certificate concerns a particular mathematical object: here, a registration problem built from sixteen frozen correspondences and their support radii. Physical execution uses a separately computed relative transform from causal navigation. CARD records both, alongside the conditions under which a confirmed proof token can support a service.

That separation matters when the outputs disagree. A checker-confirmed optimizer point and a navigation-derived transform can represent different quantities even when they share the same image and event identities. Treating them as one accepted output would obscure what was actually verified.

Two channels, joined by explicit support

CARD splits each opportunity into a certificate channel and an execution channel. The first freezes the registration instance before optimization. A checker reconstructs the observations, bounds and objective, confirming the specified mathematical statement when its conditions hold.

The second channel computes the physical transform using navigation information available at the decision time. Before buying a certificate, the system tests that transform against the frozen correspondences. In this implementation, service eligibility requires at least three of the sixteen residuals to fall within their respective support radii.

A later checker confirmation joins this unchanged eligibility decision and transform to create a proof-backed service. The certificate still applies to the registration instance and objective; it does not become a separate certification that the navigation transform optimizes that objective. Reference measurements enter afterward for evaluation, rather than selecting requests retrospectively.

What the airborne comparison shows

The primary study reports 404 non-overlapping cases from twenty sorties of an AA15–X500 airborne survey system, covering mountainous, village and town scenes.

All 404 registration instances received checker confirmation. Nevertheless, the paper classifies every certificate-side optimizer point as discrepant from its processed navigation reference. Median rotational and translational discrepancies were about 1.9891 degrees and 21.6322 metres.

For the same image and event identities, all 404 causal-navigation transforms were classified as reference-consistent, with median discrepancies of about 0.0036566 degrees and 0.0104519 metres. Of these transforms, 370 became proof-backed services and 34 were withheld because they did not satisfy the service-support condition.

These results support the paper’s distinction between mathematical confirmation and physical reference consistency. They should not be read as evidence that certificates generally fail, or that CARD corrected the certified optimizer into a more accurate transform. The executed transform comes from the separate navigation channel.

Buy proofs that can support a service

The acquisition experiment makes the practical consequence especially clear. Among 170 policy candidates, 155 were service-eligible before certificate purchase. All 170 ultimately received checker confirmation and had reference-consistent navigation transforms, but fifteen could not instantiate the specified service.

Uniformly sampling without replacement from all 170 candidates therefore spends some requests on ineligible cases. Under the experiment’s live-confirmation condition, the useful-service count follows a hypergeometric distribution, with expected yield equal to the request budget multiplied by 155/170.

Sampling only from the eligible population instead gives one useful service per request, provided the budget does not exceed 155 and the required proofs complete, remain live and retain legal support. Across five budgets, the observed ordinary-random means differed from the theoretical predictions by at most 0.8412 services.

Crucially, random selection restricted to eligible candidates matched CARD’s useful-service yield. The paper therefore attributes this gain to eligibility screening, not to a demonstrated advantage of its chronological scheduling rule over eligible random selection.

Proof maintenance and graph computation

CARD also models an action together with its exact proof witness. An unchanged action can still incur maintenance cost when its witness expires or needs replacement. The theoretical decomposition adds semantic movement and witness-repair cost along the same action sequence. Ignoring witnesses gives the same optimum only when a semantic-optimal sequence admits a zero-cost witness path.

Separately, public downstream experiments compare recorded graph interventions across eleven KITTI, EuRoC and TUM cases. Comparisons match graph size, intervention counts, downweight levels and effective total weight. Ordinary-random interventions took 1.128–67.65 times CARD’s optimizer wall time, while the maximum absolute relative trajectory-error change was 0.0611%.

Solver instrumentation locates the separation in elimination fill, Cholesky factor size and numerical work. These are downstream optimizer measurements, not an end-to-end speedup for certificate acquisition and execution.

The evidence combines a proprietary airborne study with public downstream cases. Its one-request/one-service result depends on the stated proof-availability conditions. Within those boundaries, the preprint’s contribution is a precise accounting interface: what was certified, what was executed, which proof remained usable, and what the resulting graph cost to solve.