see

Euler identity (exact, certificate-friendly):

Insight

The compiled query selected 6 fact(s) after the rule closure was computed.
Main conclusion: :result :identityHolds true.

Selected conclusions:

• :result :identityHolds true .
• :result :phaseModSqIsOne true .
• :result :phaseModSq 1 .
• :result :rhsZero (0 0) .
• :result :lhsPlusOne (0 0) .
• :result :phasePi (-1 0) .

Explanation

The generated JavaScript starts from 10 compiled source fact(s), applies 5 compiled rule(s), and stops only after a fixpoint is reached.
After saturation, the compiled log:query directive projects only the matching facts shown in the insight, rather than dumping the whole graph.

A compact derivation path is:

• Rule 1: if (0 1) math:difference ?minusOne, then :phasePi :exact (?minusOne 0). This produced :phasePi :exact (-1 0) .
• Rule 2: if :phasePi :exact (?re ?im); :one :exact (?oneRe ?oneIm); (?re ?oneRe) math:sum ?sumRe; (?im ?oneIm) math:sum ?sumIm, then :EulerIdentity :lhsExact (?sumRe ?sumIm); :EulerIdentity :rhsExact (0 0). This produced :EulerIdentity :lhsExact (0 0) ., :EulerIdentity :rhsExact (0 0) .
  • Premises used:
    • :phasePi :exact (-1 0) . (derived fact)
    • :one :exact (1 0) . (source fact)
• Rule 3: if :EulerIdentity :lhsExact (?sumRe ?sumIm); :zero :exact (?sumRe ?sumIm), then :EulerIdentity :holds true. This produced :EulerIdentity :holds true .
  • Premises used:
    • :EulerIdentity :lhsExact (0 0) . (derived fact)
    • :zero :exact (0 0) . (source fact)
• Rule 4: if :phasePi :exact (?re ?im); (?re ?re) math:product ?re2; (?im ?im) math:product ?im2; (?re2 ?im2) math:sum ?modSq, then :phasePi :modSq ?modSq. This produced :phasePi :modSq 1 .
  • Premises used:
    • :phasePi :exact (-1 0) . (derived fact)
• Rule 5: if :phasePi :modSq ?modSq; ?modSq math:equalTo 1, then :phasePi :modSqIsOne true. This produced :phasePi :modSqIsOne true .
  • Premises used:
    • :phasePi :modSq 1 . (derived fact)

Evidence

These are the facts selected by the query projection.

:result :phasePi (-1 0) .  
:result :lhsPlusOne (0 0) .  
:result :rhsZero (0 0) .  
:result :phaseModSq 1 .  
:result :phaseModSqIsOne true .  
:result :identityHolds true .