Tensor-native 3D box camera certificates

This module is TorchLean's tensor-native camera-box certificate implementation.

Cube R-CNN, SAM 3D, and related systems can be treated as untrusted producers of tensors. This checker verifies the geometric contract of one exported artifact:

• a camera projection matrix P : Tensor α (shape![3,4]);
• eight 3D cuboid corners corners : Tensor α (shape![8,3]);
• image dimensions; and
• a claimed 2D enclosing box.

The checker recomputes the pinhole projection of every 3D corner and checks:

1. every projected corner has positive camera depth;
2. every projected pixel lies inside the image bounds; and
3. the claimed 2D box itself is inside the image;
4. the claimed 2D box encloses all projected corners, up to an explicit tolerance.

Why this shape?

Real 3D perception systems already speak tensors: Cube R-CNN / Omni3D predictions, PyTorch3D utilities, and SAM-3D-style post-hoc metadata all move around matrices, points, boxes, and camera parameters. So this module uses Spec.Tensor throughout instead of introducing a detached Vec3 island. The few abbrevs below are only names for tensor shapes.

Small interval arithmetic layer

structure NN.Verification.Geometry3D.Box3D.ScalarInterval (α : Type) : Type

A closed scalar interval [lo, hi].

This intentionally stays compact: it is just enough to state and prove camera-parameter uncertainty theorems without pulling the 3D demo into a much larger interval-analysis framework.

• lo : α

  Lower endpoint.

• hi : α

  Upper endpoint.

def NN.Verification.Geometry3D.Box3D.InInterval {α : Type} [LE α] (I : ScalarInterval α) (x : α) : Prop

Membership in a closed scalar interval.

def NN.Verification.Geometry3D.Box3D.NonnegativeInterval {α : Type} [OfNat α 0] [LE α] (I : ScalarInterval α) : Prop

The interval has nonnegative lower endpoint, hence all members are nonnegative.

def NN.Verification.Geometry3D.Box3D.addInterval {α : Type} [Add α] (I J : ScalarInterval α) : ScalarInterval α

Interval addition: [a,b] + [c,d] = [a+c, b+d].

def NN.Verification.Geometry3D.Box3D.mulNonnegInterval {α : Type} [Mul α] (I J : ScalarInterval α) : ScalarInterval α

Interval multiplication for nonnegative intervals: [a,b] * [c,d] = [a*c, b*d] when both intervals are nonnegative.

def NN.Verification.Geometry3D.Box3D.divNonnegByPosInterval {α : Type} [Div α] (num den : ScalarInterval α) : ScalarInterval α

Interval division for a nonnegative numerator interval and a strictly positive denominator interval:

[a,b] / [c,d] = [a/d, b/c] when 0 ≤ a and 0 < c.

This is the perspective-division primitive. A pinhole projection is not just affine camera arithmetic; it also divides homogeneous pixel numerators by positive depth. Keeping this operation separate makes the trust boundary explicit: an exporter may provide interval enclosures for u_num, v_num, and z, and Lean proves the quotient enclosure is sound.

theorem NN.Verification.Geometry3D.Box3D.addInterval_sound {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {I J : ScalarInterval α} {x y : α} (hx : InInterval I x) (hy : InInterval J y) : InInterval (addInterval I J) (x + y)

Soundness of interval addition.

If x ∈ I and y ∈ J, then x + y ∈ I + J.

theorem NN.Verification.Geometry3D.Box3D.mulNonnegInterval_sound {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {I J : ScalarInterval α} {x y : α} (hI : NonnegativeInterval I) (hJ : NonnegativeInterval J) (hx : InInterval I x) (hy : InInterval J y) : InInterval (mulNonnegInterval I J) (x * y)

Soundness of nonnegative interval multiplication.

If I and J have nonnegative lower endpoints, then multiplication is monotone over both intervals: x ∈ I, y ∈ J implies x*y ∈ [I.lo*J.lo, I.hi*J.hi].

theorem NN.Verification.Geometry3D.Box3D.divNonnegByPosInterval_sound {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {num den : ScalarInterval α} {x z : α} (hnum : NonnegativeInterval num) (hdenPos : 0 < den.lo) (hx : InInterval num x) (hz : InInterval den z) : InInterval (divNonnegByPosInterval num den) (x / z)

Soundness of perspective-style interval division.

If x ∈ num, z ∈ den, num is nonnegative, and the denominator interval is bounded away from zero, then x / z lies in [num.lo / den.hi, num.hi / den.lo].

This theorem is the mathematical core behind the "full uncertainty envelope" for 3D boxes: depth uncertainty is handled by a certified quotient, not by an informal post-processing check.

def NN.Verification.Geometry3D.Box3D.pinholePixelInterval {α : Type} [Add α] [Mul α] (fI coordI cI : ScalarInterval α) : ScalarInterval α

Pinhole x-coordinate interval from uncertain intrinsics and normalized coordinate.

For u = fx * xn + cx, with fx ≥ 0 and xn ≥ 0, interval arithmetic gives: u ∈ fxI*xnI + cxI.

theorem NN.Verification.Geometry3D.Box3D.pinholePixelInterval_sound {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {fI coordI cI : ScalarInterval α} {f coord c : α} (hfNonneg : NonnegativeInterval fI) (hcoordNonneg : NonnegativeInterval coordI) (hf : InInterval fI f) (hcoord : InInterval coordI coord) (hc : InInterval cI c) : InInterval (pinholePixelInterval fI coordI cI) (f * coord + c)

Soundness of the one-axis pinhole interval formula.

This is the camera-parameter uncertainty theorem used by the 3D geometry certificate workflow: if focal length, principal point, and normalized coordinate are each inside certified intervals, then the resulting pixel coordinate is inside the interval computed by pinholePixelInterval.

structure NN.Verification.Geometry3D.Box3D.PixelInterval2D (α : Type) : Type

A pair of x/y pixel intervals enclosing a projected point under camera uncertainty.

• x : ScalarInterval α

  Pixel-x interval.

• y : ScalarInterval α

  Pixel-y interval.

def NN.Verification.Geometry3D.Box3D.PixelInInterval2D {α : Type} [LE α] (pix : PixelInterval2D α) (px py : α) : Prop

A concrete pixel lies inside a 2D pixel interval.

def NN.Verification.Geometry3D.Box3D.homogeneousProjectionInterval {α : Type} [Div α] (uNumI vNumI zI : ScalarInterval α) : PixelInterval2D α

Pixel interval obtained from homogeneous camera-coordinate intervals.

Here uNumI and vNumI enclose the first two rows of P * [X,Y,Z,1], while zI encloses the positive depth row. The actual projected pixel is (u_num / z, v_num / z).

This formulation matches real exported tensors better than a detached Vec3 API: camera matrices, 3D corners, and interval bounds can all be produced by the same tensor pipeline, and Lean proves the final quotient/bbox claim.

theorem NN.Verification.Geometry3D.Box3D.list_all_true_of_mem {α : Type} {p : α → Bool} {xs : List α} (h : xs.all p = true) {x : α} (hx : x ∈ xs) : p x = true

If List.all p xs succeeds, then p succeeds on every member of xs.

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.Point3 (α : Type) : Type

A 3D point as a tensor of shape [3].

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.Point2 (α : Type) : Type

A 2D point as a tensor of shape [2].

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.BoxCorners (α : Type) : Type

Eight cuboid corners, stored as a tensor of shape [8, 3].

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.CameraP (α : Type) : Type

A 3×4 camera projection matrix.

For a homogeneous point [X,Y,Z,1], the raw camera coordinates are:

u_num = P₀·[X,Y,Z,1], v_num = P₁·[X,Y,Z,1], z = P₂·[X,Y,Z,1].

The projected pixel is (u_num / z, v_num / z), checked only when z > 0.

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.ProjectedCorners (α : Type) : Type

Projected eight-corner tensor of shape [8, 2].

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.Box2D (α : Type) : Type

A 2D box [xmin, ymin, xmax, ymax].

def NN.Verification.Geometry3D.Box3D.matGet {α : Type} {rows cols : ℕ} (x : Spec.Tensor α (Tensor.Shape.Mat rows cols)) (i : Fin rows) (j : Fin cols) : α

Matrix scalar accessor for tensor-shaped matrices.

def NN.Verification.Geometry3D.Box3D.vecGet {α : Type} {n : ℕ} (x : Spec.Tensor α (Tensor.Shape.Vec n)) (i : Fin n) : α

Vector scalar accessor for tensor-shaped vectors.

def NN.Verification.Geometry3D.Box3D.corner {α : Type} (corners : BoxCorners α) (i : Fin 8) : Point3 α

Extract the i-th cuboid corner as a [3] tensor.

def NN.Verification.Geometry3D.Box3D.matOfFn {α : Type} (rows cols : ℕ) (f : Fin rows → Fin cols → α) : Spec.Tensor α (Tensor.Shape.Mat rows cols)

Build a matrix tensor from a coordinate function. Useful for small fixtures.

def NN.Verification.Geometry3D.Box3D.vecOfFn {α : Type} (n : ℕ) (f : Fin n → α) : Spec.Tensor α (Tensor.Shape.Vec n)

Build a vector tensor from a coordinate function. Useful for small fixtures.

def NN.Verification.Geometry3D.Box3D.cameraCoord {α : Type} [OfNat α 1] [Add α] [Mul α] (P : CameraP α) (x : Point3 α) (row : Fin 3) : α

Raw homogeneous camera coordinate P[row] · [X,Y,Z,1].

def NN.Verification.Geometry3D.Box3D.projectZ {α : Type} [OfNat α 1] [Add α] [Mul α] (P : CameraP α) (x : Point3 α) : α

Positive-depth denominator used by pinhole projection.

def NN.Verification.Geometry3D.Box3D.projectX {α : Type} [OfNat α 1] [Add α] [Mul α] [Div α] (P : CameraP α) (x : Point3 α) : α

Projected x/pixel coordinate. Meaningful when projectZ P x ≠ 0.

def NN.Verification.Geometry3D.Box3D.projectY {α : Type} [OfNat α 1] [Add α] [Mul α] [Div α] (P : CameraP α) (x : Point3 α) : α

Projected y/pixel coordinate. Meaningful when projectZ P x ≠ 0.

def NN.Verification.Geometry3D.Box3D.projectPoint {α : Type} [OfNat α 1] [Add α] [Mul α] [Div α] (P : CameraP α) (x : Point3 α) : Point2 α

Project one 3D point to a 2D tensor.

def NN.Verification.Geometry3D.Box3D.projectBox {α : Type} [OfNat α 1] [Add α] [Mul α] [Div α] (P : CameraP α) (corners : BoxCorners α) : ProjectedCorners α

Project all eight cuboid corners.

structure NN.Verification.Geometry3D.Box3D.BoxCameraCert (α : Type) : Type

A compact exported 3D-box/camera certificate.

• width : α

  Image width in pixels.

• height : α

  Image height in pixels.

• tol : α

  Tolerance used when checking the claimed enclosing box.

• camera : CameraP α

  3×4 camera projection matrix.

• corners : BoxCorners α

  Eight exported 3D cuboid corners.

• bbox : Box2D α

  Claimed 2D box [xmin,ymin,xmax,ymax].

def NN.Verification.Geometry3D.Box3D.xmin {α : Type} (cert : BoxCameraCert α) : α

Claimed 2D box left edge.

def NN.Verification.Geometry3D.Box3D.ymin {α : Type} (cert : BoxCameraCert α) : α

Claimed 2D box top edge.

def NN.Verification.Geometry3D.Box3D.xmax {α : Type} (cert : BoxCameraCert α) : α

Claimed 2D box right edge.

def NN.Verification.Geometry3D.Box3D.ymax {α : Type} (cert : BoxCameraCert α) : α

Claimed 2D box bottom edge.

def NN.Verification.Geometry3D.Box3D.PixelIntervalInsideBBox {α : Type} [LE α] (cert : BoxCameraCert α) (pix : PixelInterval2D α) : Prop

The pixel interval is contained in the claimed 2D box.

theorem NN.Verification.Geometry3D.Box3D.pixel_inside_bbox_of_interval_inside {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {cert : BoxCameraCert α} {pix : PixelInterval2D α} {px py : α} (hinside : PixelIntervalInsideBBox cert pix) (hpix : PixelInInterval2D pix px py) : xmin cert ≤ px ∧ px ≤ xmax cert ∧ ymin cert ≤ py ∧ py ≤ ymax cert

If a pixel interval is contained in the claimed bbox, every concrete pixel inside that interval is also contained in the bbox.

theorem NN.Verification.Geometry3D.Box3D.pinhole_intrinsics_interval_inside_bbox_sound {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {cert : BoxCameraCert α} {fxI fyI xnI ynI cxI cyI : ScalarInterval α} {fx fy xn yn cx cy : α} (hfxNonneg : NonnegativeInterval fxI) (hfyNonneg : NonnegativeInterval fyI) (hxnNonneg : NonnegativeInterval xnI) (hynNonneg : NonnegativeInterval ynI) (hinside : PixelIntervalInsideBBox cert { x := pinholePixelInterval fxI xnI cxI, y := pinholePixelInterval fyI ynI cyI }) (hfx : InInterval fxI fx) (hfy : InInterval fyI fy) (hxn : InInterval xnI xn) (hyn : InInterval ynI yn) (hcx : InInterval cxI cx) (hcy : InInterval cyI cy) : xmin cert ≤ fx * xn + cx ∧ fx * xn + cx ≤ xmax cert ∧ ymin cert ≤ fy * yn + cy ∧ fy * yn + cy ≤ ymax cert

Full pinhole-intrinsics interval-to-bbox theorem.

Assume independent intervals for focal lengths (fx, fy), normalized coordinates (xn = X/Z, yn = Y/Z), and principal point (cx, cy). If the interval arithmetic result

u ∈ fxI*xnI + cxI, v ∈ fyI*ynI + cyI

is contained in the claimed bbox, then every concrete camera/pixel choice satisfying those input intervals projects inside the bbox.

This is the full uncertainty-envelope bridge for the camera-uncertainty workflow: uncertainty begins at camera intrinsics and normalized camera coordinates, propagates through the pinhole equations, and ends as a certified bbox-enclosure statement. The theorem is phrased over normalized coordinates so callers can plug in whichever depth-interval or model-uncertainty method they use to bound X/Z and Y/Z.

theorem NN.Verification.Geometry3D.Box3D.homogeneous_projection_interval_inside_bbox_sound {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {cert : BoxCameraCert α} {uNumI vNumI zI : ScalarInterval α} {uNum vNum z : α} (huNumNonneg : NonnegativeInterval uNumI) (hvNumNonneg : NonnegativeInterval vNumI) (hzPos : 0 < zI.lo) (hinside : PixelIntervalInsideBBox cert (homogeneousProjectionInterval uNumI vNumI zI)) (huNum : InInterval uNumI uNum) (hvNum : InInterval vNumI vNum) (hz : InInterval zI z) : xmin cert ≤ uNum / z ∧ uNum / z ≤ xmax cert ∧ ymin cert ≤ vNum / z ∧ vNum / z ≤ ymax cert

Full homogeneous projection interval-to-bbox theorem.

This is the stronger robustness theorem. Instead of assuming the projected pixel has already been bounded, it starts from intervals over the homogeneous camera outputs:

• uNumI encloses the x numerator P₀ · [X,Y,Z,1];
• vNumI encloses the y numerator P₁ · [X,Y,Z,1]; and
• zI encloses the positive depth denominator P₂ · [X,Y,Z,1].

If the quotient intervals [uNumI.lo / zI.hi, uNumI.hi / zI.lo] and [vNumI.lo / zI.hi, vNumI.hi / zI.lo] are inside the claimed 2D box, then every concrete camera projection represented by those intervals is inside the box. This is exactly the guard we want for uncertain camera intrinsics/extrinsics, bounded corner perturbations, or mixed numeric backends: they may produce ranges for homogeneous coordinates, but Lean checks the perspective divide and the final bbox containment.

def NN.Verification.Geometry3D.Box3D.certProjectX {α : Type} [OfNat α 1] [Add α] [Mul α] [Div α] (cert : BoxCameraCert α) (i : Fin 8) : α

Projected x-coordinate of corner i.

def NN.Verification.Geometry3D.Box3D.certProjectY {α : Type} [OfNat α 1] [Add α] [Mul α] [Div α] (cert : BoxCameraCert α) (i : Fin 8) : α

Projected y-coordinate of corner i.

def NN.Verification.Geometry3D.Box3D.certProjectZ {α : Type} [OfNat α 1] [Add α] [Mul α] (cert : BoxCameraCert α) (i : Fin 8) : α

Camera depth of corner i.

Mathematical certificate predicates

def NN.Verification.Geometry3D.Box3D.PositiveImageSize {α : Type} [OfNat α 0] [LT α] (cert : BoxCameraCert α) : Prop

Image dimensions must be positive.

def NN.Verification.Geometry3D.Box3D.BBoxOrdered {α : Type} [OfNat α 0] [LE α] (cert : BoxCameraCert α) : Prop

Basic sanity for the reported 2D box and tolerance.

def NN.Verification.Geometry3D.Box3D.BBoxInsideImage {α : Type} [OfNat α 0] [LE α] (cert : BoxCameraCert α) : Prop

The reported 2D box itself should lie inside the image frame.

def NN.Verification.Geometry3D.Box3D.PositiveDepths {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Mul α] [LT α] (cert : BoxCameraCert α) : Prop

Every 3D corner lies in front of the camera.

def NN.Verification.Geometry3D.Box3D.ProjectedInImage {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Mul α] [Div α] [LE α] (cert : BoxCameraCert α) : Prop

Every projected corner lies inside the image rectangle.

def NN.Verification.Geometry3D.Box3D.BBoxEnclosesProjection {α : Type} [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] (cert : BoxCameraCert α) : Prop

The reported 2D box encloses all projected 3D corners, up to tolerance.

Robust projection predicates

The single-artifact checker above says the exported projection is coherent at one numeric point. For real model outputs we also want robustness statements around that point.

There are two complementary robustness layers in this file:

• homogeneous_projection_interval_inside_bbox_sound starts from intervals over homogeneous camera outputs (u_num, v_num, z) and proves the perspective-divided pixels stay inside the claimed box.
• bbox_encloses_perturbed_of_margin starts from a nominal projected pixel and proves that any bounded pixel-space perturbation stays inside the claimed box if there is enough slack.

Together they cover the two most common exporter contracts: interval-enclosed camera arithmetic and bounded downstream pixel perturbation.

def NN.Verification.Geometry3D.Box3D.BBoxEnclosesProjectionWithMargin {α : Type} [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] (cert : BoxCameraCert α) (margin : α) : Prop

The projected corners are inside the claimed 2D box with an explicit positive slack margin.

Compared with BBoxEnclosesProjection, this predicate is stricter: corners must land inside [xmin + margin, xmax - margin] × [ymin + margin, ymax - margin]. The margin is what pays for future uncertainty.

def NN.Verification.Geometry3D.Box3D.ProjectionPerturbationWithin {α : Type} [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] (cert : BoxCameraCert α) (eps : α) (px py : Fin 8 → α) : Prop

px, py describe an interval-perturbed projection of every corner.

For each corner i, px i and py i are some possible projected coordinates after exporter, renderer, rounding, or uncertainty perturbation. This predicate says those coordinates are within eps pixels of the nominal projection recomputed from the certificate.

def NN.Verification.Geometry3D.Box3D.BBoxEnclosesPerturbedProjection {α : Type} [LE α] (cert : BoxCameraCert α) (px py : Fin 8 → α) : Prop

The claimed 2D box encloses every perturbed projected corner.

This is the robust postcondition downstream consumers want: even after a bounded perturbation, the candidate 3D artifact still projects inside the detector's claimed 2D box.

theorem NN.Verification.Geometry3D.Box3D.bbox_encloses_perturbed_of_margin {α : Type} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {cert : BoxCameraCert α} {eps margin : α} {px py : Fin 8 → α} (hle : eps ≤ margin) (hmargin : BBoxEnclosesProjectionWithMargin cert margin) (hperturb : ProjectionPerturbationWithin cert eps px py) : BBoxEnclosesPerturbedProjection cert px py

Projection-interval robustness theorem.

If every nominal projected corner has at least margin pixels of slack inside the box, and every perturbed projection is within eps ≤ margin pixels of that nominal projection, then all perturbed projections remain inside the original claimed 2D box.

This is deliberately independent of how the perturbation was produced: it can come from Float rounding, a renderer approximation, a model uncertainty interval, or an external exporter. The theorem is the certified geometry guard.

def NN.Verification.Geometry3D.Box3D.Verified3DBox {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] (cert : BoxCameraCert α) : Prop

The end-user theorem-facing statement.

This says the exported detector artifact is internally coherent under its stated camera model: positive image dimensions, ordered in-frame 2D box, positive camera depth, projected corners inside the image, and claimed 2D box enclosure.

Boolean checker and soundness theorems

def NN.Verification.Geometry3D.Box3D.checkPositiveImageSize {α : Type} [OfNat α 0] [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (cert : BoxCameraCert α) : Bool

Boolean check for positive image dimensions.

def NN.Verification.Geometry3D.Box3D.checkBBoxOrdered {α : Type} [OfNat α 0] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (cert : BoxCameraCert α) : Bool

Boolean check for BBoxOrdered.

def NN.Verification.Geometry3D.Box3D.checkBBoxInsideImage {α : Type} [OfNat α 0] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (cert : BoxCameraCert α) : Bool

Boolean check for BBoxInsideImage.

def NN.Verification.Geometry3D.Box3D.checkPositiveDepths {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Mul α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (cert : BoxCameraCert α) : Bool

Boolean check for PositiveDepths.

def NN.Verification.Geometry3D.Box3D.checkProjectedInImage {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Mul α] [Div α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (cert : BoxCameraCert α) : Bool

Boolean check for ProjectedInImage.

def NN.Verification.Geometry3D.Box3D.checkBBoxEnclosesProjection {α : Type} [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (cert : BoxCameraCert α) : Bool

Boolean check for BBoxEnclosesProjection.

def NN.Verification.Geometry3D.Box3D.checkCert {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] (cert : BoxCameraCert α) : Bool

Full Boolean checker for one exported 3D-box/camera artifact.

theorem NN.Verification.Geometry3D.Box3D.checkPositiveImageSize_sound {α : Type} [OfNat α 0] [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {cert : BoxCameraCert α} (h : checkPositiveImageSize cert = true) : PositiveImageSize cert

theorem NN.Verification.Geometry3D.Box3D.checkBBoxOrdered_sound {α : Type} [OfNat α 0] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {cert : BoxCameraCert α} (h : checkBBoxOrdered cert = true) : BBoxOrdered cert

theorem NN.Verification.Geometry3D.Box3D.checkBBoxInsideImage_sound {α : Type} [OfNat α 0] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {cert : BoxCameraCert α} (h : checkBBoxInsideImage cert = true) : BBoxInsideImage cert

theorem NN.Verification.Geometry3D.Box3D.checkPositiveDepths_sound {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Mul α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {cert : BoxCameraCert α} (h : checkPositiveDepths cert = true) : PositiveDepths cert

theorem NN.Verification.Geometry3D.Box3D.checkProjectedInImage_sound {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Mul α] [Div α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {cert : BoxCameraCert α} (h : checkProjectedInImage cert = true) : ProjectedInImage cert

theorem NN.Verification.Geometry3D.Box3D.checkBBoxEnclosesProjection_sound {α : Type} [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {cert : BoxCameraCert α} (h : checkBBoxEnclosesProjection cert = true) : BBoxEnclosesProjection cert

theorem NN.Verification.Geometry3D.Box3D.checkCert_sound {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] {cert : BoxCameraCert α} (h : checkCert cert = true) : Verified3DBox cert

Soundness of the executable checker.

This is the main theorem for the implementation: if the Boolean checker accepts an artifact, the artifact satisfies the mathematical Verified3DBox predicate.

Consequence theorems for verified artifacts

theorem NN.Verification.Geometry3D.Box3D.Verified3DBox.positive_image_size {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] {cert : BoxCameraCert α} (h : Verified3DBox cert) : 0 < cert.width ∧ 0 < cert.height

theorem NN.Verification.Geometry3D.Box3D.Verified3DBox.bbox_inside_image {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] {cert : BoxCameraCert α} (h : Verified3DBox cert) : 0 ≤ xmin cert ∧ xmax cert ≤ cert.width ∧ 0 ≤ ymin cert ∧ ymax cert ≤ cert.height

theorem NN.Verification.Geometry3D.Box3D.Verified3DBox.corner_positive_depth {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] {cert : BoxCameraCert α} (h : Verified3DBox cert) (i : Fin 8) : 0 < certProjectZ cert i

theorem NN.Verification.Geometry3D.Box3D.Verified3DBox.projected_corner_in_image {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] {cert : BoxCameraCert α} (h : Verified3DBox cert) (i : Fin 8) : 0 ≤ certProjectX cert i ∧ certProjectX cert i ≤ cert.width ∧ 0 ≤ certProjectY cert i ∧ certProjectY cert i ≤ cert.height

theorem NN.Verification.Geometry3D.Box3D.Verified3DBox.projected_corner_in_claimed_bbox {α : Type} [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] {cert : BoxCameraCert α} (h : Verified3DBox cert) (i : Fin 8) : xmin cert - cert.tol ≤ certProjectX cert i ∧ certProjectX cert i ≤ xmax cert + cert.tol ∧ ymin cert - cert.tol ≤ certProjectY cert i ∧ certProjectY cert i ≤ ymax cert + cert.tol

Float JSON checker for exported artifacts

def NN.Verification.Geometry3D.Box3D.formatString : String

Expected schema string for JSON artifacts accepted by this checker.

def NN.Verification.Geometry3D.Box3D.matFloatOfFlat (rows cols : ℕ) (xs : Array Float) : Spec.Tensor Float (Tensor.Shape.Mat rows cols)

Tensor from a flat array. The caller is responsible for checking the length.

def NN.Verification.Geometry3D.Box3D.vecFloatOfFlat (n : ℕ) (xs : Array Float) : Spec.Tensor Float (Tensor.Shape.Vec n)

Vector tensor from a flat array. The caller is responsible for checking the length.

def NN.Verification.Geometry3D.Box3D.requireSize (ctx : String) (xs : Array Float) (expected : ℕ) : IO Unit

def NN.Verification.Geometry3D.Box3D.parseJsonCert (j : Lean.Json) : IO (BoxCameraCert Float)

Parse a JSON artifact into the Float checker representation.

def NN.Verification.Geometry3D.Box3D.checkFile (path : String) : IO Bool

Load and check a JSON 3D-box/camera certificate.

This is the bridge to Cube R-CNN/SAM-3D-style outputs. The JSON is untrusted; Lean recomputes the projection and accepts only if the tensor artifact passes the checker.

def NN.Verification.Geometry3D.Box3D.checkOrThrow (path : String) : IO Unit

Convenience wrapper for CLI fixtures.