Geometry is a projection
Build the construction and its geometry together. An imported solid remains a candidate until it has a checked plan. Scaling, joining, or changing a setup can invalidate a witness.
Research sketch · v0.1 · September 2026
A shape is only
half the design.
What if an admitted design carried evidence for a way to make it?
Verified Design proposes manufacturing witnesses tied to a particular stock, tool, fixture, machine, and acceptance contract.
Read the research paperProposal, not an implemented verified CNC libraryNo completed Lean proof or physical validation is claimed
01 / A deliberately small example
The capsule-pocket model
Change two assumptions.
See what the arithmetic can say.
Original arithmetic illustrationmm · plan view
Ideal removal footprintHolder projectionNominal x gap
Top view is an illustration, not a toolpath. The holder is above the stock. A projected overlap alone does not establish a 3D collision.
0.00 mm0.20 mm
A worst-case bound for one boundary. Two-boundary dimensions use twice this value.
3.00 mm9.00 mm
Changes only the horizontal holder-separation test. The cutter radius remains 2 mm; other assumptions stay fixed.
Boundary margin0.10 − b0.02 mm
Dimensional margin0.20 − 2b0.04 mm
Conservative floor thickness5.95 − (2 + 2b) · minimum 3.703.79 mm
These three numerical limits are met, conditional on the assumptions.
Horizontal gap lower bound8 − holder radius − 0.162.84 mm
Positive horizontal separation in the toy enclosure model.
Physical assumptions
The inputs are not measurements
The source invents this environment. No experiment validates these bounds. Moving a slider creates a different conditional example, not an admitted design.
Fixed stock & geometry
40 × 30 × 6 mm blank; 20 × 4 × 2 mm nominal capsule pocket; cutter radius 2 mm; stock thickness uncertainty ±0.05 mm.
Fixed fixtures & enclosure
Fixture strips at x = 0–4 and 36–40 mm, z = 0–4 mm. Holder center spans x = 12–28 mm. Relative obstacle/assembly expansion remains 0.16 mm.
Separate physical hypotheses
Fixed restraint under allowed loads, feasible motion, allowed entry/cutting process, and preserved feature identity and topology are assumed. This page does not verify them.
Acceptance limits
Boundary envelope 0.10 mm; dimensions ±0.20 mm; remaining floor ≥3.70 mm. Finish, burrs, and strength are outside this example.
Where does the source’s 0.08 mm budget come from?
- Exact geometry0.00
- Tool geometry & tip uncertainty0.01
- Controller interpolation & tracking0.02
- Datum registration0.02
- Material, elastic & thermal effects0.02
- Export & numerical approximation0.01
All values are assumed worst-case millimeter bounds in the same norm and datum over the entire trace. The sum is 0.08 mm; no statistical independence is claimed. Adjusting the total slider does not supply evidence for a new allocation.
The source also assumes identity kinematics and limited joint ranges. Its complete cutting cylinder, shank, and holder envelopes have separate vertical-clearance obligations. This two-dimensional explorer does not recheck those obligations. See the full toy case
02 / The proposed contract
Evidence travels with the design.
01
Intent + environment
Define acceptance and the versioned physical model.
02
Candidate plan
A planner proposes operations and certificates.
03
Small checker
A future proved checker validates the evidence it understands.
04
Admitted design
Retain the witness, assumptions, and exact version identities.
The guarantee being sought
If a witness checks and a physical run conforms to the declared model, its finished state should satisfy the acceptance contract.
A program proof connects the checker to the model.Physical evidence must connect the run to that model.
Unknown is meaningful
An unsupported certificate or inconclusive enclosure should stay unknown. Failure to find a plan is not evidence that no manufacturing method exists.
Inspection is separate
A planned bound is not a measurement. For allowed width 3.80–4.20 mm, a reading of 4.18 ± 0.03 mm remains unresolved because its interval reaches 4.21 mm.
03 / Keep the boundaries visible
A proposal with explicit limits.
Grassmann.jl
Michael Reed’s Grassmann.jl motivates an algebraic vocabulary for frames, incidence, and transformations. An adapter would still need Euclidean semantics, degenerate-case handling, and numerical bounds.
Correct algebra alone does not prove tool access, stock removal, restraint, or acceptance. This site imports no Grassmann code and makes no claim of a verified Lean port or CAM implementation.
Attribution and research limitsSendCutSend
The repository’s independent read-only plugin scaffold helps review official guidance and label evidence. It is a skill-only bundle, not an authenticated supplier connector.
The source review, dated September 30, 2026, located no supported public developer API contract. That is a bounded discovery result, not proof that partner access does not exist.
Read the documented boundaryNo machine-ready output. This site performs no physical validation, supplier connection, upload, quotation, or order. It provides no fabrication-safety assurance.
04 / Source & provenance
A fixed public snapshot.
This presentation is based only on the public Verified Design repository at revision c63f566. It is not a live supplier-rule feed.