The current official Lean language reference makes each structure field and its type explicit; a later field type may depend on an earlier field.
Adapt as a formal stress test. In a SlotSpec, the declaration-local SlotKind and exact participant ValueKind are explicit. FPF does not infer that a Lean structure is a world-side relation or ontic. This disciplines the formal reduced case in A.6.5:5.5, where operand order remains local to the mathematical representation and an explicit correspondence relates operands to RelationSignature SlotSpecs before FPF reuse.
In current TypeDB 3.x syntax, each external role type is declared through a named relation type, with explicit scope when equal labels occur under different relation types.
Adapt the declaration locality. FPF uses SlotKind, not SystemRole, for the declaration-local name of a participant meaning inside a RelationSignature; the exact system-role kind remains the by-value participant under a direct assignment species’ AssignedSystemRoleKindSlot, and occurrence identity remains with A.2.1 rather than storage identity. This prevents HolderSystemSlot, AssignedSystemRoleKindSlot, and InspectorSystemRole from collapsing in A.6.5:5.1.
The RDF 1.2 Candidate Recommendation of 7 April 2026 distinguishes triple terms, propositions, asserted triples, and reifiers used in further statements.
Adopt the separation. A graph term or reifier may represent an assertion, but it does not replace the world-side relation, direct obtaining condition, or SlotSpec. This is the boundary exercised by the episteme case in A.6.5:5.3.
Almeida, Guizzardi, Sales, and Fonseca, gUFO, 2026 preprint
The current comparison line exposes relation aspects, reification choices, and higher-order typing pressure.
Use as a stress comparator. Keep relation occurrence, signature, assertion, and local typed projection distinct without importing the source taxonomy as FPF ontology. This tests the three-way dispatch in A.6.5:4.6 and the result-qualification case in A.6.5:5.4.