Function literal_identity_eq 

pub fn literal_identity_eq(a: &Literal, b: &Literal) -> bool

THE ONE RULE. Total, reflexive literal equality — bit-exact on floats — offered as a FUNCTION so term.rs and this store cannot hold two different opinions about it.

Why a hash-consed kernel has no second option

Hash-consing is a QUOTIENT: interning maps a term to the equivalence class of its structure, and a quotient exists only for an EQUIVALENCE relation. Literal’s derived PartialEq uses IEEE == on Literal::Float, which is

• not reflexive (NaN != NaN), and
• not a function of the representation (0.0 == -0.0 holds between distinct bit patterns).

So it is not an equivalence relation, and no hash-consing scheme can implement it — not this one, not Lean’s, not any. The choice is therefore not between two tastes: either Literal’s equality becomes bit-exact on floats, or the kernel can never key anything on term identity. Lean made the same call: Literal.ofNat/ofScientific compare by value and its Expr equality is structural, never IEEE.

It is the rule term.rs now has, and this is the INDEPENDENT model it is locked against

Literal’s PartialEq is hand-written and compares f64::to_bits(), which makes the existing impl Eq for Literal {} an honest claim rather than an unsound contract. This function is deliberately NOT a call to it: it is a second implementation, wildcard-free on the diagonal where term.rs’s falls through to _ => false, and W_perf_extra::the_two_implementations_of_the_one_literal_rule_agree_on_every_pair runs the two against each other over a grid that contains three distinct NaN bit patterns, both zeros, and one value of every other variant. Two implementations that agree is evidence; one implementation compared with itself is not.