spec(port): port specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 (Closes #9677)

specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27

@@ -0,0 +1,82 @@
+// trios-igla-race invariants — the constitutional phi anchor check.
+// Port of gHashTag/trios-railway:crates/trios-igla-race/src/invariants.rs
+// (at 8b229e9489ee, 15 lines) — Roadmap Stage 6, goal #4548, target t27c
+// gen-rust.
+//
+// The original computes phi as (1 + sqrt(5)) / 2 and verifies the
+// constitutional anchor identity phi^2 + 1/phi^2 = 3 within 1e-10. The
+// language has no sqrt builtin, so the port computes sqrt(5) by Newton's
+// iteration — forty halving steps from 5.0 converge far past f64
+// precision — and the tolerance check carries the 1e-10 bound as
+// 0.0000000001 (the parser's literal set has no scientific notation).
+// Every function is a tested pure decision; no transport exists in this
+// port (issue #9677, "Port the decision, not the plumbing").
+
+module port::trios_igla_race_invariants;
+
+// Newton's iteration for sqrt(5): x <- (x + 5/x) / 2, forty rounds from
+// 5.0 — quadratic convergence, far beyond the f64 tolerance below.
+pub fn sqrt5_newton() -> f64 {
+    var s: f64 = 5.0;
+    var i: usize = 0;
+    while (i < 40) {
+        s = (s + 5.0 / s) / 2.0;
+        i += 1;
+    }
+    return s;
+}
+
+// Original line 2: `let phi = (1.0_f64 + 5.0_f64.sqrt()) / 2.0;`.
+pub fn phi_from_sqrt5(sqrt5: f64) -> f64 {
+    return (1.0 + sqrt5) / 2.0;
+}
+
+// Original line 3: `let anchor = phi * phi + 1.0 / (phi * phi);`.
+pub fn anchor_of_phi(phi: f64) -> f64 {
+    const sq: f64 = phi * phi;
+    return sq + 1.0 / sq;
+}
+
+// Original line 4: `(anchor - 3.0).abs() < 1e-10` — the tolerance bound,
+// carried as its decimal form.
+pub fn within_anchor_tolerance(anchor: f64) -> bool {
+    if (anchor - 3.0 < 0.0) {
+        return (3.0 - anchor) < 0.0000000001;
+    }
+    return (anchor - 3.0) < 0.0000000001;
+}
+
+// Original lines 1-5: the constitutional anchor check itself.
+pub fn check_phi_anchor() -> bool {
+    return within_anchor_tolerance(anchor_of_phi(phi_from_sqrt5(sqrt5_newton())));
+}
+
+test phi_anchor_holds {
+    assert(check_phi_anchor());
+}
+
+test anchor_identity_at_the_golden_ratio {
+    assert(within_anchor_tolerance(anchor_of_phi(1.618033988749895)));
+    assert(within_anchor_tolerance(anchor_of_phi(phi_from_sqrt5(sqrt5_newton()))));
+    assert(!within_anchor_tolerance(anchor_of_phi(1.5)));
+}
+
+test sqrt5_converges_to_the_root {
+    const s = sqrt5_newton();
+    assert(s > 2.2360679774);
+    assert(s < 2.2360679775);
+}
+
+test phi_matches_the_golden_ratio {
+    const phi = phi_from_sqrt5(sqrt5_newton());
+    assert(phi > 1.6180339887);
+    assert(phi < 1.6180339888);
+}
+
+test tolerance_around_three {
+    assert(within_anchor_tolerance(3.0));
+    assert(within_anchor_tolerance(3.00000000005));
+    assert(within_anchor_tolerance(2.99999999995));
+    assert(!within_anchor_tolerance(3.05));
+    assert(!within_anchor_tolerance(2.95));
+}