diff --git a/.claude/board/entries/2026-10-22-pal256-egraph-evidence-law-admission.md b/.claude/board/entries/2026-10-22-pal256-egraph-evidence-law-admission.md new file mode 100644 index 000000000..55de575ed --- /dev/null +++ b/.claude/board/entries/2026-10-22-pal256-egraph-evidence-law-admission.md @@ -0,0 +1,20 @@ +# Cold mathematical candidate laws for typed evidence families + +Scope **test-only / not egglog rule admission yet**. The Math Foundry E1 probe (#1690/#1693/#1696/#1698), R2IL and mask-risc remain sole owners. MeTTa/MORK/OpenNARS are source languages or independent differential oracles, never replacement hot execution engines. + +Candidate laws: +1. `tanh(atanh(x)) = x` on the open real unit interval; finite-precision LUT cancellation needs a separate quantization/error proof. +2. `tanh(a+b)=(tanh(a)+tanh(b))/(1+tanh(a)tanh(b))` on finite real operands. +3. NARS positive/negative independent evidence counts merge by additive counts. +4. Bayesian log-likelihood contributions add only with correctly identified prior, likelihood and conditional independence. + +Refuse: +- mapping arbitrary embedding cosine to Pearson sample r or sample-size evidence; +- treating `sum(atanh(cos))` as NARS revision; +- `c=tanh(|z|)` as sample-aware confidence; +- global e-graph `3σ -> 0` equivalence; +- float re-association, saturation, LUT roundtrips, or non-idempotent memory effects without typed guards. + +Next cold stage: attach admitted typed predicates to existing `egglog-r2il-probe` *without* adding a second e-graph, emit R2IL via `FoldDialect`, independent oracle/replay capsule, compare to baseline under altered binding and ABI witness. Keep proof/law, compiled recipe, dataset/source evidence and execution receipts separate. + +Run: `cargo test --manifest-path crates/egglog-r2il-probe/Cargo.toml --test palette256_typed_evidence_laws`. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 296c6e2c8..642b44f77 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -438 entries, 2026-08-06 .. 2026-10-22. +440 entries, 2026-08-06 .. 2026-10-22. | date | entry id | finding | file | |---|---|---|---| @@ -33,6 +33,7 @@ exactly one of them, never both. | 2026-10-22 | `pal256-nars-bayes-evidence-contract` | | [2026-10-22-pal256-nars-bayes-evidence-contract.md](2026-10-22-pal256-nars-bayes-evidence-contract.md) | | 2026-10-22 | `pal256-immutable-needle-distribution-probe` | | [2026-10-22-pal256-immutable-needle-distribution-probe.md](2026-10-22-pal256-immutable-needle-distribution-probe.md) | | 2026-10-22 | `pal256-hebbian-overlay-plasticity` | | [2026-10-22-pal256-hebbian-overlay-plasticity.md](2026-10-22-pal256-hebbian-overlay-plasticity.md) | +| 2026-10-22 | `pal256-egraph-evidence-law-admission` | | [2026-10-22-pal256-egraph-evidence-law-admission.md](2026-10-22-pal256-egraph-evidence-law-admission.md) | | 2026-10-22 | `pal256-bnn-disambiguation` | | [2026-10-22-pal256-bnn-disambiguation.md](2026-10-22-pal256-bnn-disambiguation.md) | | 2026-10-22 | `pal256-argextrema-margins` | | [2026-10-22-pal256-argextrema-margins.md](2026-10-22-pal256-argextrema-margins.md) | | 2026-10-22 | `pal256-64hop-error-containment` | | [2026-10-22-pal256-64hop-error-containment.md](2026-10-22-pal256-64hop-error-containment.md) | diff --git a/crates/egglog-r2il-probe/tests/palette256_typed_evidence_laws.rs b/crates/egglog-r2il-probe/tests/palette256_typed_evidence_laws.rs new file mode 100644 index 000000000..39234a28a --- /dev/null +++ b/crates/egglog-r2il-probe/tests/palette256_typed_evidence_laws.rs @@ -0,0 +1,77 @@ +//! Cold admission probes for mathematical candidate laws, *not* a new runtime +//! e-graph. Keep existing egglog -> R2IL -> mask-risc ownership boundaries. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Domain { + OpenUnitReal, + IndependentCounts, + BayesLogLikelihood, + FisherCorrelation, + QuantizedPalette, +} +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Law { + TanhAtanhCancel, + MergeIndependentCounts, + AddLogLikelihoodRatios, + UnconditionalThreeSigmaPrune, +} +fn admit(law: Law, domain: Domain) -> bool { + matches!( + (law, domain), + (Law::TanhAtanhCancel, Domain::OpenUnitReal) + | (Law::MergeIndependentCounts, Domain::IndependentCounts) + | (Law::AddLogLikelihoodRatios, Domain::BayesLogLikelihood) + ) +} +#[test] +fn exact_identity_is_admitted_only_in_its_declared_numeric_domain() { + for x in [-0.99_f64, -0.5, 0.0, 0.25, 0.99] { + assert!((x.atanh().tanh() - x).abs() < 1e-12); + } + assert!(admit(Law::TanhAtanhCancel, Domain::OpenUnitReal)); + assert!(!admit(Law::TanhAtanhCancel, Domain::QuantizedPalette)); + assert!(!admit(Law::TanhAtanhCancel, Domain::FisherCorrelation)); + assert!(!admit( + Law::UnconditionalThreeSigmaPrune, + Domain::OpenUnitReal + )); + assert!(1.0_f64.atanh().is_infinite()); +} +#[test] +fn bayesian_log_likelihood_addition_is_not_nars_frequency_revision() { + let f1 = 0.7_f64; + let f2 = 0.7_f64; + let nars_revision: f64 = (7.0 + 7.0) / (10.0 + 10.0); + let signed1 = 2.0 * f1 - 1.0; + let signed2 = 2.0 * f2 - 1.0; + let hyperbolic = ((signed1.atanh() + signed2.atanh()).tanh() + 1.0) * 0.5; + assert!((nars_revision - 0.7).abs() < 1e-12); + assert!( + hyperbolic > 0.8, + "different evidence algebra, not a compiler optimization" + ); + assert!(admit( + Law::MergeIndependentCounts, + Domain::IndependentCounts + )); + assert!(!admit( + Law::MergeIndependentCounts, + Domain::BayesLogLikelihood + )); + assert!(admit( + Law::AddLogLikelihoodRatios, + Domain::BayesLogLikelihood + )); + assert!(!admit( + Law::AddLogLikelihoodRatios, + Domain::IndependentCounts + )); +} +#[test] +fn tanh_addition_identity_is_a_distinct_true_mathematical_law() { + let a: f64 = 0.4; + let b: f64 = -0.2; + let left = (a + b).tanh(); + let right = (a.tanh() + b.tanh()) / (1.0 + a.tanh() * b.tanh()); + assert!((left - right).abs() < 1e-12); +}