From 279aec627a3d34f81652469211515ad93e31e16e Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Sat, 3 Oct 2026 07:10:04 -0300 Subject: [PATCH] specs/math: sacred_physics checks every member of its finite sets instead of a dropped prose tail (#5726) phi_pow_inverse_reciprocal ("for n in {1, 2, 3, 4, 5}") and phi_pow_additive_exponents ("for a, b in {1, 2, 3}") lost their whole assertion to the parser. Both sets are finite, so each member is now its own assertion (5 + 9), same tolerance. Seals regenerated with this tree's t27c; the parse-no-discard ledger entry is removed. Closes #5726 Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/SacredPhysics.json | 13 ++++++++----- .trinity/seals/math_SacredPhysics.json | 15 +++++++++------ ...0-03-sacred-physics-finite-sets-checked.md | 19 +++++++++++++++++++ docs/reports/suite_expectations.json | 12 ------------ specs/math/sacred_physics.t27 | 18 ++++++++++++++++-- 5 files changed, 52 insertions(+), 25 deletions(-) create mode 100644 docs/now/2026-10-03-sacred-physics-finite-sets-checked.md diff --git a/.trinity/seals/SacredPhysics.json b/.trinity/seals/SacredPhysics.json index 97cdcd4b0a..8aedd1c5e9 100644 --- a/.trinity/seals/SacredPhysics.json +++ b/.trinity/seals/SacredPhysics.json @@ -1,11 +1,14 @@ { - "gen_hash_c": "sha256:1834bfa53d90f01917ba4387adf433fd509ecb37ab409ca20571194aced83ccf", + "gen_hash_c": "sha256:0577373af4ec884dc199323efa57dbd2397b6720505cd81f1201127cd259b31a", "gen_hash_rust": "sha256:87280ffe0736ee63e7c3e7e4703c843125cb7f719ebe0ef571f1cb805dee5a53", "gen_hash_verilog": "sha256:5446262d32d6ea25f9750a9373171fec7e7b80cf073837674e2cd3554326a2ff", - "gen_hash_zig": "sha256:c00aab5bf1d11a856b515ce4f79f4ffaf06a37003873ccc2614e4129896b9cfe", + "gen_hash_zig": "sha256:800dabaac79a79ae2d4d9503309759f6b4117f9e7659ec7baf3ab42a4a26671f", "module": "SacredPhysics", "ring": 12, - "sealed_at": "2026-09-08T14:07:50Z", - "spec_hash": "sha256:67898bda2d551b7dd1d6973582c81aafddc17d63055d8213c6bf1152dad01f3c", - "spec_path": "specs/math/sacred_physics.t27" + "sealed_at": "2026-10-03T10:07:22Z", + "spec_hash": "sha256:6f0c02de93fc908bcae88bd48037b8b06c54efe3fc0105ab09288fb2102e74d9", + "spec_path": "specs/math/sacred_physics.t27", + "tests": { + "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-sacred_physics-20455/spec.zig:101:19: error: use of undeclared identifier 'PI_lv'" + } } \ No newline at end of file diff --git a/.trinity/seals/math_SacredPhysics.json b/.trinity/seals/math_SacredPhysics.json index 5f9ad723b0..b312d7afc9 100644 --- a/.trinity/seals/math_SacredPhysics.json +++ b/.trinity/seals/math_SacredPhysics.json @@ -1,12 +1,15 @@ { - "gen_hash_c": "sha256:1834bfa53d90f01917ba4387adf433fd509ecb37ab409ca20571194aced83ccf", + "gen_hash_c": "sha256:0577373af4ec884dc199323efa57dbd2397b6720505cd81f1201127cd259b31a", "gen_hash_rust": "sha256:87280ffe0736ee63e7c3e7e4703c843125cb7f719ebe0ef571f1cb805dee5a53", "gen_hash_verilog": "sha256:5446262d32d6ea25f9750a9373171fec7e7b80cf073837674e2cd3554326a2ff", - "gen_hash_zig": "sha256:c00aab5bf1d11a856b515ce4f79f4ffaf06a37003873ccc2614e4129896b9cfe", + "gen_hash_zig": "sha256:800dabaac79a79ae2d4d9503309759f6b4117f9e7659ec7baf3ab42a4a26671f", "module": "SacredPhysics", "ring": 12, - "sealed_at": "2026-09-08T14:07:50Z", - "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:67898bda2d551b7dd1d6973582c81aafddc17d63055d8213c6bf1152dad01f3c", - "spec_path": "specs/math/sacred_physics.t27" + "sealed_at": "2026-10-03T10:07:22Z", + "sealed_by": "t27c-bootstrap@0.4.0", + "spec_hash": "sha256:6f0c02de93fc908bcae88bd48037b8b06c54efe3fc0105ab09288fb2102e74d9", + "spec_path": "specs/math/sacred_physics.t27", + "tests": { + "blocked": "does not compile: /var/folders/jz/zcjlxjps7gs81jtkwvkbryzc0000gn/T/t27c-test-report-sacred_physics-20455/spec.zig:101:19: error: use of undeclared identifier 'PI_lv'" + } } \ No newline at end of file diff --git a/docs/now/2026-10-03-sacred-physics-finite-sets-checked.md b/docs/now/2026-10-03-sacred-physics-finite-sets-checked.md new file mode 100644 index 0000000000..d0088f2b90 --- /dev/null +++ b/docs/now/2026-10-03-sacred-physics-finite-sets-checked.md @@ -0,0 +1,19 @@ +# NOW -- sacred_physics checks every member of its finite sets (2026-10-03) + +## What was read + +- `t27c parse-complete` on master 8fdf7155: `specs/math/sacred_physics.t27` discarded 48 top-level tokens on lines 399 and 403. +- `--show` named them: `phi_pow_inverse_reciprocal` ended in `for n in {1, 2, 3, 4, 5}` and `phi_pow_additive_exponents` in `for a, b in {1, 2, 3}`. The parser cannot read that tail, so it dropped the whole assertion; both invariants kept their names and checked nothing. + +## What changed + +- Both sets are finite and spelled out, so the claims are now checked completely: one assertion per n (5) and one per pair (a, b) (9), with the original tolerance 1e-12. A comment above each says which set it covers. +- These are not the open-domain `forall` quantifiers of #2774; nothing of that kind was touched. +- Both seals (`SacredPhysics.json`, `math_SacredPhysics.json`) were regenerated with the t27c built from this tree (`seal --verify`: all hashes MATCH). +- The spec's `parse-no-discard` entry left `docs/reports/suite_expectations.json`; `t27c suite --ratchet --corpus-only` is CLEAN. + +## Not verified + +- `t27c test-report` is BLOCKED on master and here alike: the generated Zig uses an undeclared `PI_lv` (2 `ast-check` errors before and after). The 14 new checks are in the Zig output, but none of them ran. + +Closes #5726 diff --git a/docs/reports/suite_expectations.json b/docs/reports/suite_expectations.json index e751b0fef6..24157aaeb2 100644 --- a/docs/reports/suite_expectations.json +++ b/docs/reports/suite_expectations.json @@ -717,18 +717,6 @@ "bdd-block-fallback": 55 } }, - { - "path": "specs/math/sacred_physics.t27", - "phase": "parse-no-discard", - "reason": "top-level drop-recovery discards tokens; parser reaches EOF so `parse` reports success (T42)", - "issue": 1959, - "expires": "2026-11-30", - "discard_tokens": 48, - "discard_by_channel": { - "bdd-block-fallback": 34, - "brace-body/in-fallback": 14 - } - }, { "path": "specs/memory/notebooklm.t27", "phase": "parse-no-discard", diff --git a/specs/math/sacred_physics.t27 b/specs/math/sacred_physics.t27 index 184253a11e..31e3938064 100644 --- a/specs/math/sacred_physics.t27 +++ b/specs/math/sacred_physics.t27 @@ -396,11 +396,25 @@ module SacredPhysics { invariant phi_pow_inverse_reciprocal // Claim: C-phi-001 (EXACT), tolerance: EXACT - assert abs(phi_pow(n) * phi_pow(-n) - 1.0) < 1e-12 for n in {1, 2, 3, 4, 5} + // Checked at every n of the claim's set {1, 2, 3, 4, 5}. + assert abs(phi_pow(1) * phi_pow(-1) - 1.0) < 1e-12 + and abs(phi_pow(2) * phi_pow(-2) - 1.0) < 1e-12 + and abs(phi_pow(3) * phi_pow(-3) - 1.0) < 1e-12 + and abs(phi_pow(4) * phi_pow(-4) - 1.0) < 1e-12 + and abs(phi_pow(5) * phi_pow(-5) - 1.0) < 1e-12 invariant phi_pow_additive_exponents // Claim: C-phi-001 (EXACT), tolerance: EXACT - assert abs(phi_pow(a + b) - phi_pow(a) * phi_pow(b)) < 1e-12 for a, b in {1, 2, 3} + // Checked at every pair (a, b) of the claim's set {1, 2, 3} x {1, 2, 3}. + assert abs(phi_pow(1 + 1) - phi_pow(1) * phi_pow(1)) < 1e-12 + and abs(phi_pow(1 + 2) - phi_pow(1) * phi_pow(2)) < 1e-12 + and abs(phi_pow(1 + 3) - phi_pow(1) * phi_pow(3)) < 1e-12 + and abs(phi_pow(2 + 1) - phi_pow(2) * phi_pow(1)) < 1e-12 + and abs(phi_pow(2 + 2) - phi_pow(2) * phi_pow(2)) < 1e-12 + and abs(phi_pow(2 + 3) - phi_pow(2) * phi_pow(3)) < 1e-12 + and abs(phi_pow(3 + 1) - phi_pow(3) * phi_pow(1)) < 1e-12 + and abs(phi_pow(3 + 2) - phi_pow(3) * phi_pow(2)) < 1e-12 + and abs(phi_pow(3 + 3) - phi_pow(3) * phi_pow(3)) < 1e-12 invariant gamma_lqg_less_than_one // Claim: C-phi-001 (CONJECTURAL), tolerance: CONJECTURAL