FormalSLT

UCI Occupancy Detection · 8,224 chronological observations

Model selected after data. Bound still valid.

An all-sensor logistic classifier was selected from two predeclared candidates after the monitored prefix. The selection cost is included in the certificate.

Checkingfinal endpoint
Observed Brier loss
—
95% checked upper bound
—
Constant baseline
—

Published receipt decomposition

Where the margin comes from.

The gap above observed loss is driven mostly by observable path variation, not the cost of selecting between these models.

Observed —
Observable variation —
Model selection —
Confidence —
Checked endpoint —

Strict decimal rounding adds —.

Risk over the monitored prefix

The bound narrows as observations accumulate.

Observation
—
Observed
—
Boundary
—
Final checked point
Brier risk and upper boundary over time Replayed model Brier losses and boundary previews over 8,224 chronological observations. The published logistic final boundary is checked by Lean; other candidate boundaries are previews.
Final point checked
All-sensor logistic Constant baseline Logistic boundary Log scale · published logistic endpoint checked

Prediction timing

The outcome cannot arrive first.

The service accepts a monitored row only after its predictions have been committed for that time. The commitment is unsigned; it proves request order inside the service, not external data provenance.

  1. 01Prediction
  2. 02Commit
  3. 03Outcome
Choose an order.

Trust boundary

Fast computation. Independent replay. Final verification.

  1. 01
    Model computation

    Python trains the frozen classifier and emits quantized predictions.

  2. 02
    Independent replay

    Two implementations recompute losses, variation, hashes, and the selected posterior.

    Checking
  3. 03
    Lean kernel

    The compact checker verifies the KL charge, confidence term, variance ceiling, and final endpoint.

    Checking

Scope: posterior-averaged conditional Brier risk encountered on this monitored prefix. This retrospective application does not establish future occupancy, population risk, real-time label delay, or deployment performance.