Truth values

Types

Two related types, exported from std::core and in the prelude:

pub enum Truth4 { Is, Not, Can, Both }                              // substrate, no payload
pub enum Truth4Of<T> { Is(T), Not, Can, Both(T, T) }                  // parameterized lift

The unparameterized Truth4 is the substrate bilattice carrier — what the Lean spec mechanizes and what Federation.infoJoin, Consistency.append, and Projection.project operate over. The parameterized Truth4Of<T> is the stdlib presentation type used at query-result boundaries that have already produced typed projections — Is(T) carries the witness for the is verdict; Both(T, T) carries the two disagreeing witnesses.

Locked-substrate semantics (per Foundation/Truth4.lean, Standpoint/Consistency.lean, Standpoint/Federation.lean):

• K3 single-standpoint queries return projections containing only Is, Not, Can.
• FDE across [...] queries may return Both(a, b) when standpoints disagree.
• #[consistency(paraconsistent)] standpoints admit Both internally.

Default visibility and K3 projection

Default query return type is the projection type (e.g., Bool, [Lease]); Truth4Of<T> is introduced only when:

• The query has across [...].
• The return type is explicitly Truth4Of<…>.
• A paraconsistent standpoint admits internal Both.

K3 fail-closed projection. When a single-standpoint K3-context query projects to a non-Truth4 type, Can is folded into the projection per Pietz–Rivieccio Exactly-True semantics:

• Boolean projections: Can → false. Only Is(true) is designated.
• Set / list / record projections: Can-valued cells are omitted from the result set.
• Scalar projections: Can collapses fail-closed (omitted for collection-shaped results, false for Boolean predicates).

To preserve the distinction between Not and Can at the surface, declare the return type as Truth4Of<T> explicitly.

The compiler emits Info-level diagnostics on every across query reminding the modeler that Both may arise.