Skip to content

Materials Validation โ€” sealed cantilever deflection

GFTCL-LION-MATERIALS-001.

What the cell guarantees

Given (spec, P, kind), the cell computes deflection ฮด as an exact-Rat function: - Tip point load (single): ฮด = P ยท Lยณ / (3 ยท E ยท I) - Two-point split: ฮด = ฮดโ‚ + ฮดโ‚‚

Bit-for-bit against the sealed Lean theorems in proof/lean/FirstRoars/CantileverBeam.lean, CantileverTwoLoad.lean, CantileverOffTipLoad.lean, CantileverMixedLoad.lean, ElasticityBar.lean.

Walkthrough

MaterialsDomainPanel โ†’ tap a spec card โ†’ MaterialsValidationWalkthrough opens:

  1. Spec confirmation โ€” (spec_id, length L, Young's E, second-moment I) from sealed substrate row
  2. Load case โ€” sliders for P (and Pโ‚‚, position if two-point)
  3. Live deflection โ€” ฮด in exact reduced Rat (num/den)
  4. Match vs sealed formula โ€” bit-exact equality vs the Lean theorem evaluated on the same inputs
  5. Witness sealed โ€” append-only materials_validations row; signed quintet; broadcast permitted; AFTER INSERT trigger writes a federation_emissions row

Federation

  • NATS subject: gaiaftcl.materials.validation.sealed
  • AlertableDomain: MaterialsAlertableEvents (seedRules: match=true โ†’ GOOD; match=false โ†’ BAD)
  • Peer recompute: GET /federation/witnesses/{emission_id} returns canonical witness JSON; peer recomputes ฮด from public (spec, P, kind) and verifies SHA-256

What stays NAMED OPEN

  • Custom material kinds beyond canonical steel (named-next: summit.engineering.materials.custom_kind)
  • FEM multi-element assembly (summit.engineering.fem.assembly)
  • Plasticity / yield criteria (summit.engineering.plasticity_witness)

Files

  • Lean: proof/lean/FirstRoars/CantileverBeam.lean + 4 companions
  • Engine: cells/xcode/Sources/MaterialsUI/MaterialsEngine.swift
  • Panel: cells/xcode/Sources/MaterialsUI/MaterialsDomainPanel.swift
  • Alertable: cells/xcode/Sources/MaterialsAlertableEvents/
  • Substrate: V123 materials_specs + materials_validations (V129/V130/V131 federation columns + triggers)

Federation-cosigned

This page's source is sealed in the GaiaFTCL federation manifest โ€” page SHA-256 4153bdfa12af7531โ€ฆ, manifest witness a090592e0609adc8โ€ฆ, signed 2026-06-02T18:58:22Z by cell gaiaftcl-mac-cell. Verify with gaiaftcl wiki sign --all and compare wiki-all-signatures.json.