t27.aiРусский

Lucas numbers stay whole

You will learn

Why phi^(2n) + phi^(-2n) is always a whole number, and where the 3 of phi^2 + 1/phi^2 = 3 comes from.

phi is irrational, yet phi^2 + phi^(-2) is exactly 3. That is no accident: phi^k + (-1/phi)^k is the Lucas number L_k, and Lucas numbers are whole: 2, 1, 3, 4, 7, 11, 18 and on, each the sum of the two before it. The spec computes phi^(2n) + phi^(-2n) in f64 and checks it against L_2n for n from 0 to 6, within a tolerance of 1e-9. The 3 of the project motto is L_2.

Try it

Run the tests and read the ladder from n = 0 to n = 6. Then find the invariant that names TRINITY as L_2, and the tolerance the f64 comparison allows.

Open the interactive lesson →

GoldenFloat 3: Lucas numbers stay whole
GoldenFloat 3: Lucas numbers stay whole ↗

phi^(2n) + phi^(-2n) against L_2n, read from lucas_accumulator.t27. Lesson 3 of the GoldenFloat course.

specs/numeric/lucas_accumulator.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/numeric/lucas_accumulator.t27
// Lucas-exact accumulator for the GoldenFloat width ladder (Phase F, leg F1)
// NUMERIC-STANDARD-002
//
// CLAIM STATUS DISCIPLINE (igla-phi-architecture / goldenfloat-ladder):
//   This file captures the ONE genuinely [Verified] leg of the breadth-as-moat
//   bet (FL-004 in docs/nona-03-manifest/RESEARCH_CLAIMS.md): the arithmetic
//   identity phi^(2n) + phi^(-2n) = L_(2n) (an integer Lucas number). It does
//   NOT establish that the phi-ladder is better than posit / takum / OCP-MX --
//   that remains [Open conjecture], falsified by the F2/F3 ablation. F1 verifies
//   the ARITHMETIC, never the MOAT.
//
// WHY THIS MATTERS (integer-backed accumulation):
//   Because phi^(2n) + phi^(-2n) equals the integer Lucas number L_(2n) exactly,
//   a phi-scaled partial-sum accumulator can be carried in plain unsigned-integer
//   storage with no hardware half-type dependency, while base-2 floats (posit,
//   OCP-MX, bf16) accumulate rounding error. Verified to 60 decimal digits with
//   mpmath: max residual over n=0..12 was 7.1e-56 (pure f64-of-irrational noise;
//   the integer track is exact). Anchor for the linear-time integer base-phi
//   (Zeckendorf) arithmetic: Ahlbach, Usatine, Pippenger 2012, arXiv:1207.4497.
//
// L5 IDENTITY: the [Verified] phi-facts here are phi^2 = phi + 1 and the n=1
//   case phi^2 + phi^-2 = 3 = L_2 (Lucas L2, classical 1878; NOT original to
//   this project). f64 tolerance for the float track is < 1e-9 because the
//   storage type is f64; the EXACT track is the integer Lucas recurrence below.

module LucasAccumulator {
    use base::types;

    const PHI     : f64 = 1.6180339887498948482;
    const PHI_INV : f64 = 0.6180339887498948482;  // 1/phi = phi - 1
    const TRINITY : f64 = 3.0;                     // L_2
    const TOL_F64 : f64 = 1.0e-9;                  // f64 storage tolerance

    // Integer Lucas number L_k via the exact recurrence L_0=2, L_1=1,
    // L_k = L_{k-1} + L_{k-2}. Returned as i64 (exact for the range tested).
    fn lucas(k: u32) i64 {
        if (k == 0) { return 2; }
        if (k == 1) { return 1; }
        var a : i64 = 2;  // L_0
        var b : i64 = 1;  // L_1
        var i : u32 = 2;
        while (i <= k) {
            const c : i64 = a + b;
            a = b;
            b = c;
            i = i + 1;
        }
        return b;
    }

    // The F1 accumulator value phi^(2n) + phi^(-2n) computed in f64.
    fn phi_acc(n: u32) f64 {
        const two_n : f64 = 2.0 * (n as f64);
        return pow(PHI, two_n) + pow(PHI, -two_n);
    }

    fn abs_f64(x: f64) f64 {
        if (x < 0.0) { return -x; }
        return x;
    }

    // ---- L5 identity anchors (the only [Verified] phi-facts) ----

    invariant lucas_phi_square_identity
        // phi^2 = phi + 1
        assert abs_f64(PHI * PHI - (PHI + 1.0)) < TOL_F64

    invariant lucas_trinity_is_L2
        // phi^2 + phi^-2 = 3 = L_2  (the n=1 case of the accumulator identity)
        assert abs_f64(PHI * PHI + PHI_INV * PHI_INV - TRINITY) < TOL_F64

    invariant lucas_recurrence_seed
        // exact integer recurrence seeds
        assert lucas(0) == 2 and lucas(1) == 1 and lucas(2) == 3

    // ---- F1: phi^(2n) + phi^(-2n) = L_(2n), the integer-exact accumulator ----

    test lucas_acc_n0_equals_L0
        given acc = phi_acc(0)
        and   l   = lucas(0)
        then abs_f64(acc - (l as f64)) < TOL_F64   // 2.0

    test lucas_acc_n1_equals_L2
        given acc = phi_acc(1)
        and   l   = lucas(2)
        then abs_f64(acc - (l as f64)) < TOL_F64   // 3.0

    test lucas_acc_n2_equals_L4
        given acc = phi_acc(2)
        and   l   = lucas(4)
        then abs_f64(acc - (l as f64)) < TOL_F64   // 7.0

    test lucas_acc_n3_equals_L6
        given acc = phi_acc(3)
        and   l   = lucas(6)
        then abs_f64(acc - (l as f64)) < TOL_F64   // 18.0

    test lucas_acc_n4_equals_L8
        given acc = phi_acc(4)
        and   l   = lucas(8)
        then abs_f64(acc - (l as f64)) < TOL_F64   // 47.0

    test lucas_acc_n5_equals_L10
        given acc = phi_acc(5)
        and   l   = lucas(10)
        then abs_f64(acc - (l as f64)) < TOL_F64   // 123.0

    test lucas_acc_n6_equals_L12
        given acc = phi_acc(6)
        and   l   = lucas(12)
        then abs_f64(acc - (l as f64)) < TOL_F64   // 322.0

    test lucas_value_L12_is_integer
        // the accumulator lands on an exact integer (no fractional part)
        given l = lucas(12)
        then l == 322

    // F1 produces integers across the whole tested range: the storage track is
    // integer-exact, which is the engineering point (not a per-rung quality win).
    test lucas_acc_is_integer_valued_across_ladder
        var ok = true
        var n : u32 = 0
        while (n <= 6) {
            const acc = phi_acc(n);
            const l   = lucas(2 * n);
            if (abs_f64(acc - (l as f64)) >= TOL_F64) { ok = false; }
            n = n + 1;
        }
        then ok == true

    bench lucas_recurrence_latency
        given k = 12
        when  _ = lucas(k)
        then elapsed_time_ns < 200
}

Open the lesson's spec in the player ↗

All lessons