PUBLIC WORKED EXAMPLE

BS-MIN-01 — Projection ambiguity

A precise introductory mathematical test: one projection admits alternatives; distance relations constrain them; orientation-sensitive evidence can distinguish mirror configurations.

Definitions

Let four labelled vertices in ℝ³ be P1 = (0,0,0), P2 = (1,0,0), P3 = (0,1,0), and P4 = (1,1,t), where t is a real parameter. The observer sees the ordered orthogonal projection π(x,y,z) = (x,y).

All values of t produce the same four projected points: (0,0), (1,0), (0,1), (1,1). Therefore projection alone does not identify t.

Six exact squared distances

Pair	Squared distance
P1–P2	1
P1–P3	1
P2–P3	2
P1–P4	2 + t²
P2–P4	1 + t²
P3–P4	1 + t²

Adding any squared distance incident to P4 determines t², but does not distinguish t and −t when t is nonzero. Distances between the first three points add no information about t.

Symmetry matters

The two configurations with P4 = (1,1,+a) and (1,1,−a), a > 0, are related by reflecting across z = 0. They are congruent under all Euclidean isometries E(3), which include reflections; they are not equivalent under orientation-preserving SE(3) with the ordered labels fixed.

The oriented determinant det[P2−P1, P3−P1, P4−P1] equals t. Its sign distinguishes the two configurations relative to a chosen orientation.

An observation of signed height t, an appropriate second projection, or a distance to an anchored off-plane point can resolve the mirror pair.

Reproduce the worked example

This example includes exact algebraic formulas and a finite checker using only Python's standard library. Save the linked script as bs-min-01-verify.py and run it locally.

python3 bs-min-01-verify.py

Public checker source (text) Recorded sample output Machine-readable definitions

The executable test samples rational t values. It is not a proof checker for the universally quantified mathematical statement, nor a validation of any physical or universal theory.

Lean-checked formal demonstrator

Lean 4 independently type-checked three elementary statements in a newly written, self-contained source file: projection ignores the third coordinate for any coordinate type; the projection equals the first two coordinates; and two distinct integer triples share a projection.

Compiler: Lean 4.33.0-rc1 (pinned, core library only). The local checker exited successfully and reported that each theorem depends on no axioms. You can reproduce it by saving Projection.lean.txt as Projection.lean and running the pinned Lean toolchain.

elan run leanprover/lean4:v4.33.0-rc1 lean Projection.lean

Lean source Pinned toolchain Local compilation and axiom audit output

These Lean theorems formalize only projection invariance and a non-injectivity witness. They do not formalize the real-valued distance-reconstruction theorem, the E(3)/SE(3) classification, or any unpublished ONAR9 theorem. No third-party Lean reproduction is claimed.

Counterexamples to overclaims

Claiming unique signed height from one ordinary distance: t = +1 and t = −1 give identical projections and all six distances.
Claiming that any additional edge helps: measuring P2–P3 gives distance² = 2 for every t.
Dropping the fixed base-plane assumption changes the feasible model class: four free z coordinates remain before additional relations are imposed.