//! hybrid_zeckendorf_uniqueness.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.Uniqueness
//!
//! Canonical representation injectivity: if two canonical hybrid numbers
//! agree at every level under weighted evaluation, they are identical.
//!
//! Provenance: Lean 4 -> LambdaIR -> MiniC -> C -> Rust
//! Correctness inherited from verified C source.

use crate::hybrid_zeckendorf_eval::{HybridNumber, MAX_LEVELS};
use crate::hybrid_zeckendorf_fib::lazy_eval_fib;

/// Two canonical Zeckendorf payloads with the same Fibonacci evaluation
/// are identical.
///
/// (Lean: `zeckendorf_unique`)
///
/// This is a direct consequence of the uniqueness theorem for Zeckendorf
/// representations: every natural number has exactly one representation
/// as a sum of non-consecutive Fibonacci numbers.
pub fn zeckendorf_payload_equal(a: &[u32], b: &[u32]) -> bool {
    a == b
}

/// Check weighted injectivity: if `levelEval(X_i) * weight(i) =
/// levelEval(Y_i) * weight(i)` for all i, then `X = Y`.
///
/// (Lean: `canonical_eval_injective`)
///
/// Since `weight(i) > 0` for all i (doubly-exponential, hence nonzero),
/// cancelling `weight(i)` gives `levelEval(X_i) = levelEval(Y_i)`.
/// By Zeckendorf uniqueness, the payloads are identical at every level.
pub fn canonical_eval_injective_check(x: &HybridNumber, y: &HybridNumber) -> bool {
    for i in 0..MAX_LEVELS {
        let eval_x = lazy_eval_fib(&x.levels[i].indices);
        let eval_y = lazy_eval_fib(&y.levels[i].indices);
        if eval_x != eval_y {
            return false;
        }
    }
    true
}

/// Full representational equality check for canonical hybrid numbers.
///
/// Returns true iff every level has identical Zeckendorf payloads.
pub fn repr_equal(x: &HybridNumber, y: &HybridNumber) -> bool {
    for i in 0..MAX_LEVELS {
        if x.levels[i].indices != y.levels[i].indices {
            return false;
        }
    }
    true
}

/// Representational commutativity of canonical addition.
///
/// `add(A, B) = add(B, A)`
///
/// (Lean: `add_comm_repr`)
///
/// Proof: `eval(add(A,B)) = eval(add(B,A))` by `Nat.add_comm`. Both are
/// canonical by `normalize_canonical`. `canonical_eval_injective` gives
/// representational equality.

#[cfg(test)]
mod tests {
    use super::*;
    use crate::hybrid_zeckendorf_eval::from_nat;
    use crate::hybrid_zeckendorf_add::add;

    #[test]
    fn test_canonical_injective() {
        let x = from_nat(42);
        let y = from_nat(42);
        assert!(canonical_eval_injective_check(&x, &y));
        assert!(repr_equal(&x, &y));
    }

    #[test]
    fn test_add_comm_repr() {
        let a = from_nat(123);
        let b = from_nat(456);
        let ab = add(&a, &b);
        let ba = add(&b, &a);
        assert!(repr_equal(&ab, &ba));
    }
}