StructuralSafetyCert
plain-language theorem explainer
StructuralSafetyCert packages a structural engineering safety certificate in Recognition Science terms as a record requiring exactly five failure modes together with a CanonicalCert threshold. Civil engineers optimizing J-cost designs would cite it to confirm that their factor of safety meets the phi-optimal margin. The declaration is introduced directly as a two-field record with no computation or lemmas.
Claim. A structural safety certificate consists of a finite type of failure modes whose cardinality equals 5 together with a canonical certificate satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(ϕ)>0$, $0.11<J(ϕ)<0.13$, and $J(1/ϕ^2)>0$.
background
In the Recognition Science treatment of structural engineering the factor of safety is the reciprocal of the working-stress to ultimate-strength ratio r. The J-cost function then measures the recognition deficit for any chosen r, reaching its minimum at the golden-ratio value ϕ. The module therefore fixes five distinct failure modes (yielding, buckling, fatigue, fracture, creep) whose count equals the configuration dimension in this engineering setting.
proof idea
The declaration is a plain structure definition that simply names the two required fields: the Fintype cardinality condition on FailureMode and the reference to CanonicalCert. No tactics or lemmas are applied; the structure is introduced directly.
why it matters
StructuralSafetyCert supplies the type instantiated by the downstream definition structuralSafetyCert using failureModeCount and a concrete cert. It thereby embeds the five-mode engineering constraint and the phi-band safety threshold into the Recognition Science monolith, linking the J-cost formalism to civil-engineering practice and closing the engineering tier of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.