From 8145c07845bc4f21225b7b1093cf2c90091f1b1d Mon Sep 17 00:00:00 2001 From: CLAUDE <355856132+HoTT-stuff@users.noreply.github.com> Date: Thu, 12 Nov 2026 17:38:39 +0000 Subject: [PATCH 1/2] docs(programme): record the tested multinomial bridge and two candidate statements From the work on JoshuaJewell/MetaManifold-WebUI#22. Line 2 gains a tested bridge between two implementations of one statistical model (the fork's Julia multinomial and MGLM), pinned to MetaManifold-WebUI 5a89914. Q-2.6 states S-MN (the closed form of the two-group multinomial logit and its variance) and S-DM (the Dirichlet-multinomial log-ratio contrast at the no-overdispersion boundary), both tested-only and outside the admission rule until proved. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZoFbrtmpRbKPqk25ok --- .../mathesis-research-programme.adoc | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/docs/proposals/mathesis-research-programme.adoc b/docs/proposals/mathesis-research-programme.adoc index 471ac88..2918ba8 100644 --- a/docs/proposals/mathesis-research-programme.adoc +++ b/docs/proposals/mathesis-research-programme.adoc @@ -595,6 +595,14 @@ party check it? * A possible repeat. `januskey`, `valence-shell` and `absolute-zero` each prove that undo in reverse order restores a state. *Reading* of the survey: no file compares the three statements. +* A tested bridge between two implementations of one statistical model + (added 2026-11-12). `hyperpolymath/MetaManifold-WebUI` at `5a89914` fits + the two-group multinomial logit with its own Julia code and with the R + package MGLM. Its `test/unit/test_differential.jl` checks both against one + closed form, statement S-MN under Q-2.6, and against each other: estimates + agree to 1e-6 and standard errors to a relative 1e-6. The bridge is + `tested-only`. No prover is an endpoint, so it is not a record in + `docs/atlas/claims/bridges.jsonl`, which takes Agda, Rocq and Lean only. === Research questions @@ -630,6 +638,36 @@ re-proved leg can be a second argument. In a trust expression, two legs are independent with respect to an assumption when they do not share it. A comparison that one reader wrote for both legs is a shared assumption. +Q-2.6 Can a statistical oracle become theory?:: +Two statements came out of the work on upstream issue #22 of +`MetaManifold-WebUI`. Each holds for any implementation, so each is theory by +PROOF-POLICY §1. Neither is proved; their status is `tested-only`. ++ +*S-MN.* Fit the baseline-category multinomial logit to counts in two groups +A and B, with an intercept and a group term, and reference taxon r. Let +S~gj~ be the pooled count of taxon j in group g. Then the maximum-likelihood +group coefficient of taxon j is log(S~Bj~/S~Br~) − log(S~Aj~/S~Ar~), and the +inverse observed information gives it the variance +1/S~Aj~ + 1/S~Ar~ + 1/S~Bj~ + 1/S~Br~. Two implementations meet it to 1e-8 +(`5a89914`, the test named above). ++ +*S-DM.* In Dirichlet-multinomial regression with a log link on every taxon's +Dirichlet parameter, the contrast b~j~ − b~r~ of two group coefficients does +not change when the same constant is added to every taxon's coefficient. So +the contrast does not depend on the direction in which a group's total +concentration grows. As that concentration grows without bound, the contrast +tends to the multinomial estimate of S-MN. In one simulation on multinomial +counts, MGLM's contrasts matched the multinomial ones to about 1e-5 and its +standard errors were 0.15% larger. This is an observation, not a test. ++ +*Reading:* S-MN is an oracle that any implementation of the model can be +tested against. If it were proved, a test that uses it would rest on a +theorem instead of on agreement between programs. S-DM is an equivalence at a +boundary. Its dependant is the rule in both MetaManifold-WebUI branches that +marks Dirichlet-multinomial rows `boundary` with the multinomial's estimates. +Neither statement meets the admission rule of `docs/theory/README.adoc` until +it is proved in Agda and re-proved in Rocq and Lean. + === First experiments . *E-2.1* Write the five existing comparisons as bridge records, with the From e14fc802b794f5f8f5cbe369a96f0c56f86f53c9 Mon Sep 17 00:00:00 2001 From: CLAUDE <355856132+HoTT-stuff@users.noreply.github.com> Date: Thu, 12 Nov 2026 17:53:09 +0000 Subject: [PATCH 2/2] docs(programme): S-DM needs both groups flat; S-MN needs positive pooled counts An independent review of the MetaManifold-WebUI work found that the Dirichlet-multinomial contrast equals the multinomial one only when both groups lack overdispersion. With one group overdispersed, a second simulation gives contrasts up to 0.13 away and standard errors 6 to 7 times larger. S-MN now states that its four pooled counts are positive. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZoFbrtmpRbKPqk25ok --- .../proposals/mathesis-research-programme.adoc | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/docs/proposals/mathesis-research-programme.adoc b/docs/proposals/mathesis-research-programme.adoc index 2918ba8..1fedcdb 100644 --- a/docs/proposals/mathesis-research-programme.adoc +++ b/docs/proposals/mathesis-research-programme.adoc @@ -645,7 +645,8 @@ PROOF-POLICY §1. Neither is proved; their status is `tested-only`. + *S-MN.* Fit the baseline-category multinomial logit to counts in two groups A and B, with an intercept and a group term, and reference taxon r. Let -S~gj~ be the pooled count of taxon j in group g. Then the maximum-likelihood +S~gj~ be the pooled count of taxon j in group g, and let all four of S~Aj~, +S~Ar~, S~Bj~ and S~Br~ be positive. Then the maximum-likelihood group coefficient of taxon j is log(S~Bj~/S~Br~) − log(S~Aj~/S~Ar~), and the inverse observed information gives it the variance 1/S~Aj~ + 1/S~Ar~ + 1/S~Bj~ + 1/S~Br~. Two implementations meet it to 1e-8 @@ -655,16 +656,21 @@ inverse observed information gives it the variance Dirichlet parameter, the contrast b~j~ − b~r~ of two group coefficients does not change when the same constant is added to every taxon's coefficient. So the contrast does not depend on the direction in which a group's total -concentration grows. As that concentration grows without bound, the contrast -tends to the multinomial estimate of S-MN. In one simulation on multinomial -counts, MGLM's contrasts matched the multinomial ones to about 1e-5 and its -standard errors were 0.15% larger. This is an observation, not a test. +concentration grows. As the concentrations of both groups grow without +bound, the contrast tends to the multinomial estimate of S-MN. In one +simulation on multinomial counts, MGLM's contrasts matched the multinomial +ones to about 1e-5 and its standard errors were 0.15% larger. This is an +observation, not a proof. With one group flat and the other overdispersed +the limit is not the multinomial: in a second simulation the contrasts +differed from S-MN by up to 0.13 and the standard errors were 6 to 7 times +larger. So the statement needs both groups. + *Reading:* S-MN is an oracle that any implementation of the model can be tested against. If it were proved, a test that uses it would rest on a theorem instead of on agreement between programs. S-DM is an equivalence at a boundary. Its dependant is the rule in both MetaManifold-WebUI branches that -marks Dirichlet-multinomial rows `boundary` with the multinomial's estimates. +marks Dirichlet-multinomial rows `boundary`, and that calls their estimates the +multinomial ones only when both groups are flat. Neither statement meets the admission rule of `docs/theory/README.adoc` until it is proved in Agda and re-proved in Rocq and Lean.