diff --git a/specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 b/specs/port/trios-railway/crates/trios-igla-race/src/invariants.t27 new file mode 100644 index 0000000000..c5e9df0a5c --- /dev/null +++ b/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)); +}