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 α [3,4];
• a configurable number of 3D points corners : Tensor α [pointCount,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.

Eight points are the default for a cuboid. The contract covers every supplied point; it does not assert that those points form a cuboid. The JSON parser rejects an artifact with no points, since the pointwise conditions would then hold vacuously.

Matrices, points, and boxes use the shared tensor API. The interval theorems require ordered-field arithmetic and supplied input enclosures. The JSON workflow instead checks host Float projections of one artifact; it does not establish those uncertainty assumptions or a Float-to-real bridge.

Small interval arithmetic layer

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

A closed scalar interval [lo, hi].

Endpoints for the ordered-field camera uncertainty theorems; ordering is required by their membership hypotheses rather than stored in this record.

• 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]=[ac,bd]$ 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\le a$ and $0<c$.

This is the perspective-division primitive. A pinhole projection combines affine camera arithmetic with division of 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\in I$ and $y\in J$, then $x+y\in 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\in I$ and $y\in J$ imply $xy\in[I_{\mathrm{lo}}J_{\mathrm{lo}},I_{\mathrm{hi}}J_{\mathrm{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\in\mathrm{num}$, $z\in\mathrm{den}$, $\mathrm{num}$ is nonnegative, and the denominator interval is bounded away from zero, then $x/z\in[\mathrm{num}_{\mathrm{lo}}/\mathrm{den}_{\mathrm{hi}}, \mathrm{num}_{\mathrm{hi}}/\mathrm{den}_{\mathrm{lo}}]$.

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

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

For $u=f_xx_n+c_x$, with $f_x\ge 0$ and $x_n\ge 0$, interval arithmetic gives $u\in f_{x,I}x_{n,I}+c_{x,I}$.

theorem NN.Verification.Geometry3D.Box3D.pinholePixelIntervalNonnegative_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 (pinholePixelIntervalNonnegative 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 pinholePixelIntervalNonnegative.

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.homogeneousProjectionIntervalNonnegative {α : 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]^\mathsf{T}$, while zI encloses the positive depth row. The actual projected pixel is $(u_{\mathrm{num}}/z,v_{\mathrm{num}}/z)$.

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.Point3 (α : Type) [TorchLean.Storage α] : Type

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

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.CameraP (α : Type) [TorchLean.Storage α] : Type

A 3×4 camera projection matrix.

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

$$ u_{\mathrm{num}}=P_0\mathbin{\cdot}[X,Y,Z,1],\qquad v_{\mathrm{num}}=P_1\mathbin{\cdot}[X,Y,Z,1],\qquad z=P_2\mathbin{\cdot}[X,Y,Z,1]. $$

The projected pixel is $(u_{\mathrm{num}}/z,v_{\mathrm{num}}/z)$, checked only when $z>0$.

@[reducible, inline]

abbrev NN.Verification.Geometry3D.Box3D.Box2D (α : Type) [TorchLean.Storage α] : Type

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

def NN.Verification.Geometry3D.Box3D.corner {α : Type} [TorchLean.Storage α] {pointCount : ℕ} (corners : TorchLean.Tensor α [pointCount, 3]) (i : Fin pointCount) : Point3 α

Extract the i-th supplied 3D point as a [3] tensor.

def NN.Verification.Geometry3D.Box3D.cameraCoord {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [OfNat α 1] [Add α] [Mul α] (P : CameraP α) (x : Point3 α) : α

Positive-depth denominator used by pinhole projection.

def NN.Verification.Geometry3D.Box3D.projectX {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [OfNat α 1] [Add α] [Mul α] [Div α] (P : CameraP α) (x : Point3 α) : α

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

structure NN.Verification.Geometry3D.Box3D.BoxCameraCert (α : Type) [TorchLean.Storage α] : Type

A compact exported 3D-box/camera certificate.

• pointCount : ℕ

  Number of exported 3D points; a cuboid uses eight.

• 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 : TorchLean.Tensor α [self.pointCount, 3]

  Exported 3D points, indexed by the declared count.

• bbox : Box2D α

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

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

Left edge xmin of the claimed 2D bounding box.

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

Top edge ymin of the claimed 2D bounding box.

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

Right edge xmax of the claimed 2D bounding box.

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

Bottom edge ymax of the claimed 2D bounding box.

def NN.Verification.Geometry3D.Box3D.PixelIntervalInsideBBox {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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_nonnegative_interval_inside_bbox_sound {α : Type} [TorchLean.Storage α] [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 := pinholePixelIntervalNonnegative fxI xnI cxI, y := pinholePixelIntervalNonnegative 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

Pinhole-intrinsics interval-to-bbox theorem for nonnegative normalized coordinates.

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

$u\in f_{x,I}x_{n,I}+c_{x,I}$ and $v\in f_{y,I}y_{n,I}+c_{y,I}$

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

This is a quadrant-restricted uncertainty bridge: 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_nonnegative_interval_inside_bbox_sound {α : Type} [TorchLean.Storage α] [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 (homogeneousProjectionIntervalNonnegative 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

Homogeneous projection interval-to-bbox theorem for nonnegative numerators.

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_0\mathbin{\cdot}[X,Y,Z,1]$;
• vNumI encloses the y numerator $P_1\mathbin{\cdot}[X,Y,Z,1]$; and
• zI encloses the positive depth denominator $P_2\mathbin{\cdot}[X,Y,Z,1]$.

If the quotient intervals $[u_{\mathrm{lo}}/z_{\mathrm{hi}},u_{\mathrm{hi}}/z_{\mathrm{lo}}]$ and $[v_{\mathrm{lo}}/z_{\mathrm{hi}},v_{\mathrm{hi}}/z_{\mathrm{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} [TorchLean.Storage α] [OfNat α 1] [Add α] [Mul α] [Div α] (cert : BoxCameraCert α) (i : Fin cert.pointCount) : α

Projected x-coordinate of corner i.

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

Projected y-coordinate of corner i.

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

Camera depth of corner i.

Mathematical certificate predicates

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

Image dimensions must be positive.

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

Validate the reported 2D box and tolerance.

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

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

def NN.Verification.Geometry3D.Box3D.PositiveDepths {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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_nonnegative_interval_inside_bbox_sound starts from nonnegative 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} [TorchLean.Storage α] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] (cert : BoxCameraCert α) (margin : α) : Prop

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

Compared with BBoxEnclosesProjection, this predicate is stricter: corners must land inside $[x_{\min}+\mathrm{margin},x_{\max}-\mathrm{margin}] \times[y_{\min}+\mathrm{margin},y_{\max}-\mathrm{margin}]$. The margin is what pays for future uncertainty.

def NN.Verification.Geometry3D.Box3D.ProjectionPerturbationWithin {α : Type} [TorchLean.Storage α] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] (cert : BoxCameraCert α) (eps : α) (px py : Fin cert.pointCount → α) : 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} [TorchLean.Storage α] [LE α] (cert : BoxCameraCert α) (px py : Fin cert.pointCount → α) : 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} [TorchLean.Storage α] [Field α] [LinearOrder α] [IsStrictOrderedRing α] {cert : BoxCameraCert α} {eps margin : α} {px py : Fin cert.pointCount → α} (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 $\varepsilon\le\mathrm{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} [TorchLean.Storage α] [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] (cert : BoxCameraCert α) : Prop

The checked 3D box statement exposed by the certificate workflow.

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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [OfNat α 0] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (cert : BoxCameraCert α) : Bool

Boolean check for BBoxOrdered.

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

Boolean check for BBoxInsideImage.

def NN.Verification.Geometry3D.Box3D.checkPositiveDepths {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [OfNat α 0] [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {cert : BoxCameraCert α} (h : checkPositiveImageSize cert = true) : PositiveImageSize cert

Acceptance by the image-size check yields the corresponding positive-size proposition.

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

Acceptance by the box-order check yields ordered horizontal and vertical endpoints.

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

Acceptance by the containment check places every claimed box edge inside the image.

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

Acceptance by the depth check proves that all supplied points are in front of the camera.

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

Acceptance by the projection check places every projected corner within the image rectangle.

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

Acceptance by the enclosure check places every projected corner inside the claimed box tolerance.

theorem NN.Verification.Geometry3D.Box3D.checkCert_sound {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] {cert : BoxCameraCert α} (h : Verified3DBox cert) : 0 < cert.width ∧ 0 < cert.height

A verified artifact necessarily has positive image width and height.

theorem NN.Verification.Geometry3D.Box3D.Verified3DBox.bbox_inside_image {α : Type} [TorchLean.Storage α] [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

The claimed 2D bounding box of a verified artifact lies within its image dimensions.

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

Every corner of a verified artifact has positive camera-space depth.

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

Every projected corner of a verified artifact lies within the image rectangle.

theorem NN.Verification.Geometry3D.Box3D.Verified3DBox.projected_corner_in_claimed_bbox {α : Type} [TorchLean.Storage α] [OfNat α 0] [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α] {cert : BoxCameraCert α} (h : Verified3DBox cert) (i : Fin cert.pointCount) : 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

Every projected corner lies within the verified artifact's claimed box, up to its tolerance.

Float JSON checker for exported artifacts

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

Schema string for camera-box artifacts. An artifact declares point_count, which must be positive and match the number of triples in corners3d; a cuboid declares 8.

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

Parse a certificate, rejecting malformed tensor dimensions and non-finite values.

The artifact must declare a positive point_count with corners3d.size = 3 * point_count. An artifact with no points is rejected, since every pointwise condition would hold vacuously.

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

Check a camera-box certificate and raise a readable CLI error if it is rejected.