v0.1.2-alpha — formally verified algorithm core

Frahan StonePack v0.1.2-alpha

Research preview. This release makes the algorithm core formally verified and
wires that verification into CI, then ships two correctness fixes that the
verification itself found.

1. Formally verified algorithm core

The mathematical derivations behind the shipping algorithms are now
machine-checked in Lean 4 + Mathlib (frahan_proofs/).

• Every named result of the derivations spec is proved or explicitly
  documented prose — zero sorry, zero open goals, and exactly one cited
  axiom (KKT necessity under LICQ).
• Covers the trim/clip theorems, no-fit-polygon separation (the nester's
  zero-overlap guarantee), power-cell convexity, Welsh–Powell Δ+1 colouring
  (built from scratch — Mathlib has no such bound), QEM, the Kintsugi pose
  algebra, kriging interpolation, the Lambert equal-area law, phase correlation,
  the CRA safe theorem with its Gale/Farkas converse, and the full
  Graham 1969 LPT 4/3 − 1/3m scheduling bound — the last closed by
  replacing the classical exchange induction with a static pigeonhole argument.
• The library was independently audited (three adversarial statement reviews
  plus a mechanical #print axioms sweep over all public theorems). The audit
  found the single axiom was mis-stated — it omitted feasibility of the
  minimizer, making it false — and that is fixed. No proved result depended on
  it. Audit verdict: PASS after fixes.

2. Verification CI (proofs ↔ shipping C#)

Two GitHub Actions workflows now gate every push:

• lean-proofs.yml — builds the proof library, rejects any real sorry,
  and lists declared axioms.
• verification.yml — runs
  verification/Frahan.Verification.Tests, a 40-fact
  xUnit + CsCheck suite that links the real shipping sources (never copies)
  and tests them against the same machine-checked invariants, with independent
  oracles. Covered: clip/trim, H-rep↔V-rep round-trip, Kahn build order, greedy
  colouring, NFP nesting, joint-set clustering, CRA equilibrium certificates
  (independently rebuilt residual + friction cone), Lambert projection, power
  cells, least-squares plane fitting, Soft-ICP monotonicity, and the saw-bed
  scheduler — the last checked against a brute-force optimum for the Graham
  bound.

A failure in that suite is a regression against a machine-checked invariant.

3. Two kernel fixes (found by the verification)

• ConvexPolyhedron.ClipByHalfSpace (BlockCutOpt) — volume inflation on
  coincident-plane re-clip. Re-clipping by a plane that coincides with an
  existing cut face inflated the computed volume: 2.81 % of random cuts, up to
  ~8× on thin slivers, confirmed against a Monte-Carlo ground truth. Reachable
  through ClipBothSides and staged/recovery re-cuts, so it could overstate
  recovered block yield. Fixed with a scale-aware no-op guard; the general cut
  path is untouched. Idempotence break-rate 2.81 % → 0.00 %.
• BlockGraphColorer.Color — threw on dense contact graphs. The palette was
  hard-capped at 8 (the header wrongly said 4), so any assembly needing more
  colours raised InvalidOperationException — 23.9 % of random graphs, minimum
  trigger a clique of 9 mutually-touching blocks. The Lean theorem both
  certified the properness and prescribed the fix: scale the palette to Δ+1.
  Refusals 4788 → 0; graphs of degree ≤ 7 are coloured identically to before.

Both fixes ship in this release's binaries (the install payload was rebuilt for
this tag) and are re-validated live on canvas — see the delta-audit below.

4. Nester A/B — the archived-version bug resolved

A head-to-head run of the current and Zenodo-archived nester on canvas
established that main's hole-aware nester is the correct one: the archived
build carries a Grasshopper routing bug that the current code does not. This
release supersedes that archived behaviour. (Method note: old tags do not
rebuild in a worktree due to cross-version drift, so the comparison was made
against git-verified deployed binaries.)

Validation for this release

• Test battery: 1067 PASS / 1 FAIL / 154 SKIP (baseline 2026-06-14 was
  1034/0/147; the suite has grown).
• Verification suite: 40 / 40.
• Lean library: builds green, 0 sorry, 1 audited axiom.
• Canvas delta-audit on the rebuilt + redeployed plugin: the colouring example
  and the staged-guillotine example both solve with 0 errors and 0 warnings,
  with block volumes showing no inflation (~20.2 m³ of blocks inside a 38.7 m³
  bench). Evidence and captures are recorded with the release.

Known issues

• KB-14 — Cloud ICP centroid pre-alignment is not outlier robust. The one
  battery failure. A single far outlier in the target cloud drags the
  arithmetic-mean centroid used for the initial guess, and because that runs
  before trimming, trimFraction cannot rescue it. Pre-existing since
  2026-07-10 and unrelated to this release's fixes. A robust-centroid fix is
  proposed and queued with its own property test.
• KB-15 — Masonry Stability (RBE) reports error for a primal-infeasible
  QP. Infeasibility is not a solver malfunction: by the Farkas converse of the
  safe theorem it is the certificate that the assembly is unstable, so the
  verdict should read UNSTABLE rather than error/NaN. Pre-existing;
  solver code unchanged since 2026-07-13.

Both are documented in handoffs/KNOWN_BUGS.md.

Install

git lfs pull, then run install/deploy.ps1 (Windows / Rhino 8) with Rhino
closed. See install/INSTALL.md.

Licence unchanged: GPL-3.0, bundling a research-only component
(Kintsugi / PuzzleFusion++) — research and educational use, not commercial.

v0.1.1-alpha

Frahan StonePack v0.1.1-alpha — research preview (2026-07-07)

Status: Experimental / research prototype. License: GPLv3. Independent
open-source, not an official university or company product.

A patch release over
v0.1.0-alpha. The plugin itself
gains one small additive Core API; the headline work is the surrounding
ecosystem — a browser demo, a verified mathematics layer, and a public risk
register — plus the first Rhino-free steps toward headless deployment. No
breaking changes; component GUIDs are unchanged.

Highlights

Browser nest demo (no install, no backend)

A client-side nesting demo now lives on the docs site:
https://libishm1.github.io/Frahan/nest/. Import a DXF or SVG, nest with the
actual ContactNfpHoleNester engine compiled to WebAssembly, export the
packed layout — all in the browser. The CAD file never leaves your machine.
It is hole-aware: mark defects red in your CAD (or toggle the sample defects)
and parts route around them. This is the same benchmarked engine that beats
OpenNest 2.89 on valid-layout utilization, not a re-implementation.

Verified mathematics + risk register

The mathematics section
documents what each subsystem computes, derived from the shipping code with
22+ code-vs-literature deviations flagged, a four-layer verification ladder,
four Z3 machine-proved theorem instances (NFP, IFP, BLF-vertex, inscribed
friction cone), and a Lean 4 + Mathlib formalization plan. A consolidated
risk register
triages readiness for deployment.

Plugin changes (in the .gha / yak)

• Honest signed-tetra mesh volume (MeshPackItem.MeshVolume,
  MeshPackResult.FillRatioMeshVolume): true closed-mesh volume
  V = (1/6)|sum a·(b×c)| for the honest 3D packing density numerator,
  computed in Core without RhinoCommon (the bbox VolumeEstimate remains for
  the fast over-reporting path).
• KinematicAnalysis is now Rhino-free (risk H2): the geology
  wedge/planar/toppling feasibility component no longer needs RhinoCommon
  (78 → 77 Rhino-bound Core files), a first step toward headless/service use.
• Corrections: the Kriging.Predict variance header comment corrected to
  match the code (latent variance); the multi-probe LSH construction in
  SegmentHashIndex now carries its Lv et al. 2007 citation.

Measurements

• First headless C# 3D density measurement on the real ETH1100 subset:
  16/16 stones packed, honest signed-tetra density 0.073 vs bbox 0.195 — a
  2.68× bbox over-report (the container-independent, measured confirmation
  that bbox density over-states true fill).

Install

Rhino 8 (Windows) → _PackageManager → search FrahanStonePack. Or the
offline zip. See https://libishm1.github.io/Frahan/docs/INSTALL/.

Cite

Murugesan, L. (2026). Frahan StonePack (0.1.1-alpha). Zenodo. (Version DOI
minted on release; concept DOI resolves to the latest version.)

v0.1.0-alpha

Frahan StonePack v0.1.0-alpha — experimental research prototype (2026-06-15)

Status: Experimental / research prototype. License: GPLv3. Scope: independent
open-source implementation, not an official university or company product.

This is an early alpha release of an independent open-source research implementation for
stone / geometry-processing workflows in Grasshopper. The tool is experimental and under
active development, and this release is intended for public testing, feedback, and citation
of the initial implementation.

It is a Rhino 8 / Grasshopper plugin for stone-fabrication readiness: the bridge layer between
design intent and machine-ready fabrication for dimension stone, monuments, and dry-stone
masonry. Expect rough edges; APIs and component GUIDs may still move.

What is in it

End-to-end pipeline, each stage a Grasshopper component family on the Frahan ribbon tab:

• GPR + scan ingest — radargram migration + fracture extraction; point-cloud load,
  downsample, normals, ICP, reconstruction (Geogram Poisson + CGAL fallback).
• Point-cloud discontinuity / joint sets — clean-room CSR worker: PCA normals + FACETS
  facets + Watson joint sets + stereonet + Palmstrom block size (Discontinuity Sets D5F10048).
• Discrete fracture networks — deterministic infinite-plane DFN and stochastic finite-disc
  Baecher DFN (Fisher poles, lognormal persistence) for Monte-Carlo block-yield.
• Block packing + cutting — BlockCutOpt (+ evolved Omni solver), wire-saw staged guillotine,
  recovery cascade; 2D nesting incl. hole-aware HoleNest / ContactNfpHoleNester.
• Masonry — polygonal / rubble wall generation, exact-joint assembly, CRA equilibrium
  certification, Lambda + J interlock metrics.
• Surface + restoration — BFF flatten + pack + lift (Trencadis mosaic), edge-matching, and
  an optional learned 6-DoF reassembly module (Kintsugi; see License).
• Fabrication export — cut plans, robot/KUKA adapters.

Quality

• Test battery: 1034 PASS / 0 FAIL / 147 SKIP (2026-06-14, clean clone, headless; skips are
  Rhino-runtime + optional-dataset gates).
• Benchmarks + figures with methodology: docs/results/RESULTS.md, docs/benchmarks/,
  wiki/research/. Every kept algorithm has a measured benchmark + math derivation + citation.

Install

1. Rhino 8 (Windows). git lfs pull, then run install/deploy.ps1 (or deploy.sh) with Rhino closed.
   The bundle ships the .gha + native libs (install/plugin/). Or build from source per docs/INSTALL.md.
2. Open Rhino + Grasshopper; the Frahan tab appears. Open an examples/ definition for a full workflow.

License + citation (read this)

• GPL-3.0, released for educational and research use (LICENSE, NOTICE.md).
• Bundles PuzzleFusion++ (Kintsugi module + kintsugi.bin), which its authors license
  non-commercial research-only. Do not use this software commercially. A commercial-capable
  GPL-3.0 subset is obtainable by excluding the Kintsugi module. Full attribution:
  THIRD_PARTY_NOTICES.md, data/ATTRIBUTION.md.
• Cite via CITATION.cff. Zenodo DOI minted for this release.

Known limitations (alpha)

• Many heavy nodes ship a default-FALSE Run toggle; press per-stage Run in order (avoids long solves).
• Some example data blobs are gitignored and hosted on Google Drive (see data/DATA_ACCESS.md); a few
  bundled datasets are research-use-only.
• Rhino-runtime tests (147) skip headless; they require a live Rhino install.
• Component set is broad and still consolidating; see docs/SUPERSESSION_MAP.md for evolved-vs-legacy.

Author

Libish Murugesan (ORCID 0009-0004-3238-4202). Independent research.