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)