7. Statistics + reasoning walkthrough

The kinase walkthrough (chapter 6) traces the platform’s first composition shape: five Julia institutions coordinating over formulas:FormulaTerm, bridged by declared comorphisms, AutoOnLoad gates firing as data flows through the typed pipeline. This chapter traces the second composition shape: the D52 measurement-statistics institution and the D39 justification logic tutorial, bridged by the D49 chain-witness admission over a shared eigentt:Term proposition slot. The two shapes use the same chain primitives — typed resources, AutoOnLoad cascades, deterministic verifiers — but with a different bridge mechanism. Reading both walkthroughs side by side surfaces the choice space: comorphism-mediated translation when one runtime’s output needs to be reshaped for another’s consumption, witness-index admission when one institution’s verdict is being cited as evidence rather than re-processed.

The fixture this chapter traces lives at kernel/tests/fixtures/drug_screening.esl. The end-to-end test that exercises it is kernel/tests/drug_screening.rs.

7.1. The scenario

A drug-screening lab has three IC50 readings for compound EIG_0291 (72, 85, 100 nM) and a literature rule asserting that compounds with IC50 < 100 nM at a kinase target are strong inhibitors. The author wants the chain to attest the conclusion StrongInhibitor(EIG_0291) — but only by mechanical derivation from the raw data plus the cited rule, not by author assertion.

Five chain commits accomplish this:

Declare the domain predicates (HasLowIC50, StrongInhibitor) in the chain ontology, both marked is_a stats:PopulationLevel per D52 §7.4.
Commit a stats:SampleSetResource carrying the three raw IC50 readings via stats:SingleSampleEstimate(...), paired with an ObservationTrace.
Commit a stats:StatisticalAnalysisPlan against the SampleSet asserting the 100 nM threshold (alpha = 0.05, TwoSided, WelchUnequal, Identity exclusion), paired with a ProgramTrace. The D52 institution’s AutoOnLoad gate recomputes the claim and emits a Verdict::Holds plus a per-effect result carrying HasLowIC50(EIG_0291). That result records the run and admits no witness.
Commit the literature rule as a justification:Declaration whose canonical_proposition is HasLowIC50(EIG_0291) -> StrongInhibitor(EIG_0291), and the plan’s reproducibility claim (Asserts(s) -> HasLowIC50(EIG_0291)), each paired with a DeclarationTrace. The chain-admission admits IsDeclaredAs(rule_iri, HasLowIC50 -> StrongInhibitor).
Commit a justification:Conclusion whose judgement pairs the term App(Declared(rule_iri), App(Declared(plan_yields_iri), Observed(sampleset_iri))) with the matching justification:Grounds.app term. The D39 institution’s AutoOnLoad gate type-checks the certificate against justification:Grounds(justification, StrongInhibitor(EIG_0291)); both grounding constructors consume the admitted witnesses; verdict is Holds; the sentence is admitted.

No comorphism is declared between the two institutions. No bridge code runs to translate the statistics verdict into a reasoning input. The composition works because both institutions honour the same chain artifact shape (a resource carrying canonical_proposition, plus the prov trace attesting how it came to exist), and admission reads that shape uniformly.

7.2. The five chain shapes at a glance

Resource class	What it contributes
`screen:HasLowIC50`, `screen:StrongInhibitor` (`data : ... -> Prop, stats:PopulationLevel`)	Domain predicates. The multi-class header puts both `is_a InductiveType` (implicit) and `is_a stats:PopulationLevel` on the resource so D52’s §7.4 check admits the claim under BiologicalReplication.
`screen:m_eig0291_sampleset` (`stats:SampleSetResource`)	Holds the three raw IC50 reads. `stats:SingleSampleEstimate([72.0, 85.0, 100.0], BiologicalReplication())` lands at the SingleSampleEstimate dispatch position.
`screen:m_eig0291_sampleset_trace` (`prov:ObservationTrace`)	Pairs the SampleSet with its bench provenance. Admits `IsObservedAs` for downstream auditability (D49 §6).
`screen:claim_eig0291_lowic50` (`stats:StatisticalAnalysisPlan`)	The universal-claim schema: alpha, effect_size, directionality, variance_assumption, outlier_exclusion. Its `canonical_proposition` is `HasLowIC50(EIG_0291)`. AutoOnLoad-gated by D52.
`screen:claim_eig0291_lowic50_trace` (`prov:ProgramTrace`)	Records that the statistics-institution validator ran. Admits NO witness — the fact that a computation ran grounds nothing.
`screen:rule_strong` (`justification:Declaration`)	The literature rule. `canonical_proposition` is `HasLowIC50 -> StrongInhibitor`.
`screen:plan_yields_lowic50` (`justification:Declaration`) + its `prov:DeclarationTrace`	The plan’s reproducibility claim: `Asserts(s) -> HasLowIC50(EIG_0291)`. Admits `IsDeclaredAs`, and is the DECLARED half of the computed ground.
`screen:rule_strong_trace` (`prov:DeclarationTrace`)	Admits `IsDeclaredAs(rule_iri, HasLowIC50 -> StrongInhibitor)`.
`screen:concl_eig0291_strong` (`justification:Conclusion`)	The reasoning step. One judgement: `holds(kernel, c, Grounds(App(Declared(rule), App(Declared(plan_yields), Observed(sampleset))), StrongInhibitor(EIG_0291)))`. AutoOnLoad-gated by D39.

The fixture commits all of these in one ESL document; the AutoOnLoad cascades fire in commit order (§4.2).

7.3. Step-by-step: data flowing through the pipeline

Step 1 — Predicate declarations land in the layer

data screen:HasLowIC50 : core:string -> Prop, stats:PopulationLevel { }
data screen:StrongInhibitor : core:string -> Prop, stats:PopulationLevel { }

Each data declaration commits a core:InductiveType resource whose core:is_a array carries [core:InductiveType, stats:PopulationLevel]. No AutoOnLoad fires — these are pure ontology declarations.

The stats:PopulationLevel marker is what D52’s §7.4 epistemic-scope check will read at StatisticalAnalysisPlan admissibility time to decide whether a TechnicalWithinRun replication would be rejected. (Here the SampleSet uses BiologicalReplication, so the check passes regardless of the marker; the marker is load-bearing in the parallel TechnicalWithinRun fixture variant.)

Step 2 — SampleSet + ObservationTrace land in the layer

resource screen:m_eig0291_sampleset : stats:SampleSetResource {
    prov:was_generated_by      = "instrument-log:kinase-glo-plate-2026-03-04-A1";
    prov:observed_at = "2026-03-04T14:22:11Z";

    stats:sample_set_value = stats:SingleSampleEstimate(
        [72.0, 85.0, 100.0],
        BiologicalReplication(),
    );
}

resource screen:m_eig0291_sampleset_trace : prov:ObservationTrace {
    prov:resource  = screen:m_eig0291_sampleset;
    prov:was_generated_by    = "instrument-log:kinase-glo-plate-2026-03-04-A1";
    prov:timestamp = "2026-03-04T14:22:11Z";
}

stats:SingleSampleEstimate(...) is a macro declared in the statistics ontology layer; the compiler picks it up via compile_against_layer (§6.5.4) and expands it at compile time to a Bundle(CompleteRandom(), Unblocked(), NoFactor(), BiologicalReplication(), CrossSectional(), Units([]), Columns([]), Entries([]), [72.0, 85.0, 100.0]). That’s the chain wire shape the SampleSetResource carries.

No AutoOnLoad fires on the SampleSetResource itself — D52’s gate is on StatisticalAnalysisPlan, not on SampleSetResource. The trace pairing it admits IsObservedAs(sampleset_iri, ...) in witness admission, but no D39 sentence in this fixture cites the SampleSet directly via Observed — but the computed ground does, since App(Declared(plan), Observed(sample_set)) cites the sample set as its observed half.

Step 3 — StatisticalAnalysisPlan + ProgramTrace land; D52 AutoOnLoad fires

resource screen:claim_eig0291_lowic50 : stats:StatisticalAnalysisPlan {
    stats:sample_set = screen:m_eig0291_sampleset;

    stats:null_hypothesis = type_expr(
        screen:HasLowIC50("urn:eigenius:demo:screen:EIG_0291")
    );
    stats:alternative_hypothesis = type_expr(
        screen:HasLowIC50("urn:eigenius:demo:screen:EIG_0291")
    );
    eigentt:proposition = type_expr(
        screen:HasLowIC50("urn:eigenius:demo:screen:EIG_0291")
    );

    stats:alpha = 0.05;
    stats:effect_size = Absolute(100.0, "nM");
    stats:directionality = TwoSided();
    stats:variance_assumption = WelchUnequal();
    stats:outlier_exclusion = Identity();
}

resource screen:claim_eig0291_lowic50_trace : prov:ProgramTrace {
    prov:resource  = screen:claim_eig0291_lowic50;
    prov:was_generated_by    = "statistics-institution:validate_analysis_plan";
    prov:timestamp = "2026-03-04T14:22:11Z";
}

The StatisticalAnalysisPlan commit triggers D52’s validate_analysis_plan AutoOnLoad gate. The gate runs the four-step check:

Resolve sample_set → m_eig0291_sampleset → decode the Bundle(...) ctor.
Read claim parameters; OneSidedWitnessed not asserted, so no impossibility-witness lookup.
Dispatch on (CompleteRandom, Unblocked, NoFactor, _, CrossSectional) → SingleSampleEstimate → run one_sample_t_test([72.0, 85.0, 100.0], 100.0). Result: t = -1.776, p_two_sided ≈ 0.218 (the SD across (72, 85, 100) is too large for n = 3 to reject at α = 0.05).
§7.4 epistemic scope: BiologicalReplication admits PopulationLevel ✓. Compare p < alpha: 0.218 < 0.05 → False → Verdict::Fails.

For the running narrative we use the failing claim — that’s what the fixture commits — but the same shape works for the confirmatory dataset in the fixture’s parallel claim (n = 6 tightly clustered around 85 nM), which produces Verdict::Holds and admits the witness for downstream D39 use. The drug-screening fixture in the reasoning crate uses the failing n=3 dataset for the initial claim and shows the D49 witness mechanism is layer-scoped — voiding the claim’s layer removes the witness from descendant resolutions. For an end-to-end Holds variant, see the IC50 fixture in crates/eigenius-statistics/tests/fixtures/ic50_measurement.esl, which the D39 reasoning fixture transitively layers on top of via compile_against_layer.

When the claim does pass (the confirmatory case), admission admits:

WitnessKey {
    category: Derived,
    iri: "urn:eigenius:demo:screen:claim_eig0291_lowic50",
    prop_hash: sha256(canonical_cbor(encode_type(HasLowIC50("urn:...:EIG_0291")))),
}

This entry is what the D39 sentence’s justification:Grounds.derived constructor will consume in step 5.

Step 4 — Rule + DeclarationTrace land

resource screen:rule_strong : justification:Declaration {
    prov:was_attributed_to  = agent:eigenius_core_team;
    prov:had_primary_source = screen:warrant_smith_et_al_2024;
    prov:rationale   = "IC50 < 100 nM at a kinase target is the standard strong-inhibitor threshold.";

    eigentt:proposition = type_expr(
        screen:HasLowIC50("urn:eigenius:demo:screen:EIG_0291")
        ->
        screen:StrongInhibitor("urn:eigenius:demo:screen:EIG_0291")
    );
}

resource screen:rule_strong_trace : prov:DeclarationTrace {
    prov:resource          = screen:rule_strong;
    prov:was_attributed_to = agent:eigenius_core_team;
    prov:timestamp   = "2026-04-10T09:00:00Z";
}

No AutoOnLoad fires — justification:Declaration is a chain-shape class, not an institution input. The trace pairs it with witness admission, which admits:

WitnessKey {
    category: Declared,
    iri: "urn:eigenius:demo:screen:rule_strong",
    prop_hash: sha256(canonical_cbor(encode_type(
        HasLowIC50("urn:...:EIG_0291") -> StrongInhibitor("urn:...:EIG_0291")
    ))),
}

Three witness keys are now in the index: IsObservedAs for the sample set (step 2), and IsDeclaredAs for the literature rule and for the plan’s reproducibility claim. None for the statistics result. It records what ran, and a run record grounds nothing — the computed claim’s ground is the plan declaration applied to the observed input.

Step 5 — justification:Conclusion lands; D39 AutoOnLoad fires

resource screen:concl_eig0291_strong : justification:Conclusion {

    justification:grounds_judgement = type_expr(
        alias
            EIG  = "urn:eigenius:demo:screen:EIG_0291",
            SS   = "urn:eigenius:demo:screen:m_eig0291_sampleset",
            PLAN = "urn:eigenius:demo:screen:plan_yields_lowic50",
            RULE = "urn:eigenius:demo:screen:rule_strong",
            LOW  = screen:HasLowIC50(EIG),
            // the COMPUTED ground: the declared plan applied to the observed input
            computed = justification:App(Declared(PLAN), Observed(SS)),
            cs = app( core:Asserts(SS), LOW,
                      Declared(PLAN), Observed(SS),
                      declared(PLAN, core:Asserts(SS) -> LOW),
                      observed(SS, core:Asserts(SS)) )
        in
        holds( eigentt:logic_kernel,
               app( LOW, screen:StrongInhibitor(EIG),
                    Declared(RULE), computed,
                    declared(RULE, LOW -> screen:StrongInhibitor(EIG)),
                    cs ),
               justification:Grounds(
                   justification:App(Declared(RULE), computed),
                   screen:StrongInhibitor(EIG) ) )
    );
}

One slot, not three. The proposition and the justification term are not separate fields; they appear inside the judgement’s TYPE. They used to be three fields checked by three separate paths with nothing requiring them to be about the same claim, so a certificate for one proposition could sit beside a different proposition and both check clean.

The commit triggers Rule 21, which owns every eigentt:Term-ranged slot and so owns this one. (This was D39’s validate_justification AutoOnLoad gate until P2 moved the check into commit-time validation and P7 deleted the institution.) The check:

Decode the judgement’s three fields — the logic, the certificate term, and its type.
Check the type is a type, then check the certificate against it. That is the contract eigentt:Judgement states, and it means no slot relies on inference.
Checking walks the certificate’s outer app(...), which requires sub-certificates for:
- Grounds(Declared("…rule_strong"), HasLowIC50 -> StrongInhibitor) — matched by declared(...), consuming IsDeclaredAs("…rule_strong", …). The kernel hashes the proposition, looks up the witness key in the layer’s index, finds the entry admitted in step 4, and returns the opaque witness value.
- Grounds(App(Declared("…plan_yields_lowic50"), Observed("…m_eig0291_sampleset")), HasLowIC50) — matched by the inner app(...), which in turn consumes IsDeclaredAs for the plan’s reproducibility declaration and IsObservedAs for the sample set.
All three witnesses admit, the certificate type-checks ✓.
Nothing is emitted. The conclusion is admitted; the chain has attested that this certificate grounds a claim to StrongInhibitor(EIG_0291) — not that the proposition is true. A certificate records grounds, and no rule turns Grounds(j, P) into P.

Note what the certificate does NOT cite: the StatisticalAnalysisResult. The statistics institution emitted one, and it records what the run produced — which grounds nothing. A computed claim rests on the plan being DECLARED to denote a function of its input, and on that input being OBSERVED. Neither half comes from the run.

Can a later conclusion cite this one? Only as Verified(iri), and only if it carries a justification:proof_judgement — the judgement holds(logic, t, P), which says a checker verified t against P itself. This conclusion carries no proof term, so it admits no witness. Composing on it means taking its certificate as an antecedent through Grounds.app, which is what app is for. Citing an unproved conclusion by IRI was the laundering step the two-layer separation exists to forbid.

7.4. The AutoOnLoad cascade in this scenario

Two AutoOnLoad gates fire in this commit sequence:

D52 fires on StatisticalAnalysisPlan commit (step 3). Recomputes the claim, emits Verdict + RuntimeInvocation + a per-effect result carrying the derived proposition. That result admits no witness; what it supplies is the proposition an author’s plan-reproducibility claim is written AGAINST, and the two must hash to the same key.
D39 fires on justification:Conclusion commit (step 5). Type-checks the certificate, consults admission for the two IsDeclaredAs entries (step 4) and the IsObservedAs entry (step 2), finds all three, admits the certificate, emits Verdict + RuntimeInvocation.

The cascade is mechanical, not coordinated. D52 doesn’t know D39 is about to fire; D39 doesn’t know D52 ran. They share the chain artifact shape — a resource carrying canonical_proposition, plus the prov trace that attests how it came to exist — which admission reads from. The composition emerges from each institution honouring the shared chain shape independently. See §4.2 “The D52 → D39 cascade” for the dispatch-role framing of this.

If the order is reversed (the D39 sentence commits before the D52 claim that grounds it), the sentence’s derived(claim_iri, ...) constructor would fail to admit the witness — the index entry doesn’t exist yet — and the commit would be rejected with a NoAdmittedChainWitness diagnostic. The fixture commits in topological order to avoid this, but the platform’s transactional commit semantics ensure no partial state is observable; either the whole commit succeeds or none of its resources land.

7.5. Where this composition differs from the kinase one

Dimension	Kinase walkthrough (chapter 6)	Stats + reasoning walkthrough (this chapter)
Shared payload	`formulas:FormulaTerm` — the chain-mirrored EigenTT numerical-expression fragment.	`eigentt:Term` — the chain-mirrored EigenTT type-expression fragment (D47).
Bridge mechanism	Declared comorphisms (Symbolics → JuMP, Catalyst → DiffEq, Symbolics → IntervalArithmetic). Active translation: extract → transform → reify.	Per-layer chain-witness admission over `canonical_proposition` slots (D49). Passive admission: producer emits, consumer reads.
Coupling	Each comorphism is a typed bridge with its own implementation. Adding a new institution to the composition requires authoring new comorphisms to/from it.	Each institution honouring the shared chain shape (a resource carrying `canonical_proposition`, plus its `prov` trace) participates automatically. Adding a new institution to the composition requires no new bridge code.
What runs when	Comorphism dispatch invokes the source institution’s runtime via the extract → transform pipeline; the reify step commits a new chain resource.	The producer’s AutoOnLoad gate runs at commit; admission is decided as a side effect; the consumer’s AutoOnLoad gate reads the index when type-checking the cited grounding constructor. No reify step.
Use case	”Translate this numerical expression from one institution’s view into another’s, then have the target institution process it."	"Cite this institution’s verdict as evidence inside a reasoning chain, without re-processing the value itself.”
Failure mode	Comorphism failure (extract reject, transform error, reify fail). Surfaces as institutional-error tuples per §8.2.	`NoAdmittedChainWitness` from the consumer’s gate, naming the missing (category, iri, proposition) triple. Surfaces as a type-checking diagnostic.

Both shapes are first-class. Which one applies depends on whether the downstream institution needs the input value translated (comorphism) or just cited as evidence (witness admission). A future institution could participate in both: produce a eigentt:Term proposition for witness-index consumers AND register comorphisms that translate its outputs into other institutions’ payloads for runtime consumption. The platform doesn’t mandate one composition shape per institution; the composition is per-edge.

7.6. Inspecting the audit chain from EigenQL

The verdict + witness chain is queryable from EigenQL. A typical inspection sequence after the fixture commits successfully. Note that EigenQL has no @id property pattern: a pattern’s property name resolves as a short name or a full IRI and is looked up in the resource’s property map, so a resource cannot be pinned to a given IRI that way. The subject variable itself binds to the IRI, so pin it in a WHERE clause (§5.8). This section used "@id" patterns, which do not run, until they were corrected on 2026-08-20.

USING "urn:eigenius:reasoning"

// Find the reasoning verdict
MATCH "urn:eigenius:institution:Verdict"(?v) {
    "urn:eigenius:institution:verdict_subject": "urn:eigenius:demo:screen:concl_eig0291_strong",
    "urn:eigenius:core:ctor_name": ?c
}
RETURN [] { verdict: ?c }

→ one row, verdict = "Holds".

// Walk back to the plan declaration the conclusion's computed ground cited
MATCH "urn:eigenius:justification:Conclusion"(?s) {
    "urn:eigenius:justification:term": ?j
}
WHERE ?s = "urn:eigenius:demo:screen:concl_eig0291_strong"
RETURN [] { justification: ?j }

→ one row, whose judgement’s certificate term is {ctor: "App", args: [{ctor: "Declared", args: ["...rule_strong"]}, {ctor: "App", args: [{ctor: "Declared", args: ["...plan_yields_lowic50"]}, {ctor: "Observed", args: ["...m_eig0291_sampleset"]}]}]}.

// Walk back to the statistics verdict whose proposition the plan declaration matches
MATCH "urn:eigenius:institution:Verdict"(?v) {
    "urn:eigenius:institution:verdict_subject": "urn:eigenius:demo:screen:claim_eig0291_lowic50",
    "urn:eigenius:core:ctor_name": ?c,
    "urn:eigenius:measurements:computed_statistic": ?t,
    "urn:eigenius:measurements:computed_p_value": ?p
}
RETURN [] { verdict: ?c, t: ?t, p: ?p }

→ one row, verdict = "Holds", t = -7.5, p = 6.4e-4 (for the n=6 confirmatory dataset).

// Walk back to the raw IC50 readings
MATCH "urn:eigenius:measurements:StatisticalAnalysisPlan"(?c) {
    "urn:eigenius:measurements:sample_set": ?ss
}
WHERE ?c = "urn:eigenius:demo:screen:claim_eig0291_lowic50"
RETURN [] { sample_set: ?ss }

→ one row, sample_set = "urn:eigenius:demo:screen:m_eig0291_sampleset".

// Read the raw observations off the SampleSet
MATCH "urn:eigenius:measurements:SampleSetResource"(?ss) {
    "urn:eigenius:measurements:sample_set_value": ?bundle
}
WHERE ?ss = "urn:eigenius:demo:screen:m_eig0291_sampleset"
RETURN [] { bundle: ?bundle }

→ one row carrying the full Bundle(...) ctor value with the raw [72.0, 85.0, 100.0] observations payload.

Every byte that went into the verification — the raw readings, the claim parameters, the statistics-institution recomputation, the literature rule, the reasoning certificate, both verdicts — sits on the chain as a typed, queryable, content-addressed resource. Nothing in the chain is trusted; everything is anchored.

7.7. Patterns this walkthrough exercises

Each of the next chapter’s patterns (chapter 8) has a concrete instance in this walkthrough:

Sharing a payload vs. declaring a converter (§8.1) — eigentt:Term as a shared payload between D52 and D39; no comorphism declared.
AutoOnLoad vs. OnDemand (§8.3) — both D52 and D39 fire AutoOnLoad; the cascade is the composition.
Chain reinsertion vs. transient overlay (§8.4) — the D52 result is reinserted as a chain resource, making its proposition available for a plan declaration to be written against. Without reinsertion, admission would have nothing to read.

The corresponding failure modes (chapter 9) also have direct instances:

Validation cascade failures (§9.1) — if the D52 verdict fails, the cascade stops before D39 runs; the reasoning conclusion’s commit is rejected because there is no result proposition for its plan declaration to match.
Chain-state races and stale Verdicts (§9.3) — voiding the claim’s layer removes the witness from descendant resolutions; reasoning sentences that cited it become unadmissible in those resolutions.

Next: 8. Composition patterns →