docs/core-proof.md
Cognithamus — Proof of Minimal Core
Status: PROOF. Not implemented. Assume XI never existed. Assume an empty repository. Derive the smallest core that could later support GitHub, Jira, Kubernetes, Datadog, Salesforce, SAP, or a system nobody has designed yet.
The test applied to every module:
- Why must this concept exist?
- Could a future connector function if it were removed?
- Does it describe reality, or a particular operational domain?
A module that cannot be justified without referencing XI or software engineering does not belong in the core.
1. Result
Two modules from the accepted specification fail. One is reducible. One closed vocabulary fails. The fact families are not minimal.
The surviving core is exactly the six concepts originally named — World,
Subject, Fact, Condition, Evidence, Time. My additions of Actor and Place
in the platform specification do not survive their own test, and I would rather
say that plainly than defend them.
| Module (as specified) | Verdict |
|---|---|
time |
Core |
evidence |
Core |
subject |
Core — but its closed kind list fails (§3) |
condition |
Core |
fact |
Core — but seven families reduce to four (§4) |
world |
Core — but must shed spatial content (§5) |
actor |
Reducible — a Subject that holds placements (§6) |
place |
Fails — describes representation, not reality (§5) |
legend |
Fails — describes representation (§5) |
governance |
Peer, not core — verifies the core; must not be imported by it |
2. Module-by-module
time — Instant, Window
Why it must exist. Every assertion is made at a moment, and the world must be evaluable at any instant for replay and determinism. Removed? No connector could report anything: an observation without a time is not an observation, it is a rumour. Reality or domain? Reality. Time is not a software concept. Verdict: core.
evidence — provenance and citation
Why. A value with no traceable origin cannot be verified, and Article VI forbids it. Removed? A connector could still emit values, but nothing could distinguish a measurement from an assertion. The system's central claim collapses. Reality or domain? Reality — epistemics, not engineering. A hospital auditing a reading and a bank auditing a trade need the same thing. Verdict: core.
subject — the thing a fact is about
Why. A condition must hold of something. Without subjects, facts are unattached and cannot be aggregated, deduplicated, or displayed. Removed? No. Identity is what makes two observations of one thing collapse into one fact (Article I.4). Reality or domain? The concept is reality — ontology, not engineering. But its closed kind list is not. See §3. Verdict: core, with a defect to correct.
condition — a state warranting attention
Why. The world exists to surface states that matter. Without a closed vocabulary, every connector invents its own and the world drifts. Removed? Connectors could emit measures, but nothing could be wrong, so there would be no incidents, no queues, no alerts. Reality or domain? Tested against the six families:
| Family | Non-software instance |
|---|---|
| Availability | A ward bed is out of service |
| Progress | A purchase order has not moved in 30 days |
| Capacity | A production line is at its rated limit |
| Integrity | Stock on hand differs from stock recorded |
| Exposure | A signing key is held by a departed employee |
| Economics | A campaign spends beyond its budget |
None requires software to explain. Verdict: core.
world — the canonical state at an instant
Why. Article I: one canonical operational state, projected.
Removed? There would be facts but no coherent whole, and no single thing for
renderers and APIs to agree on.
Reality or domain? Reality — provided it contains no geometry. Today's
World carries buildings, districts and positions, which are not properties of
an operational state. See §5.
Verdict: core, after shedding spatial content.
3. Defect: the subject-kind list fails the test
The approved taxonomy declares subject kinds closed:
repo·service·deployment·environment·datastore·credential·workitem·incident·budget·agent·document·channel
Every one of these is software-engineering vocabulary. Salesforce has
accounts and opportunities. SAP has purchase orders, plants and cost centres. A
hospital has wards, patients and care plans. None of them map, so a Salesforce
connector would be forced either to coerce an opportunity into workitem — a
fabrication — or to invent a kind, which the constitution forbids.
This list would have blocked exactly the systems the platform exists to support.
Proposed correction: abstract kinds with declared subtypes
Six kinds, none requiring software to explain:
| Kind | Meaning | GitHub | Jira | K8s | Salesforce | SAP |
|---|---|---|---|---|---|---|
resource |
Provides capacity or service | repository | — | deployment | territory | plant |
work |
A unit of intent | pull request | issue | — | opportunity | purchase order |
actor |
A participant | user | assignee | — | rep | approver |
agreement |
A commitment | — | SLA | quota | contract | contract |
artifact |
A produced thing | build | — | image | quote | invoice |
environment |
A context resources exist in | — | project | namespace | org | company code |
A connector declares a subtype string (resource/repository,
work/purchase-order) for display and provenance. The subtype is not part of
identity semantics, so it cannot fragment the taxonomy.
This revises an artifact you already approved, so I am flagging it rather than changing it. The condition taxonomy itself survives unchanged; only the subject-kind list needs replacing.
4. The fact families are not minimal
Measured from the current contract — seven families:
PlacementFact ActivityFact IncidentFact ExchangeFact
MeasureFact CapacityFact WorkItemFact
Two redundancies, verifiable by inspection:
IncidentFact ≡ WorkItemFact. Both assert a condition holds on a subject
at time T. They differ only in severity versus priority — and the platform
specification already makes both platform-derived rather than source-supplied.
Two shapes for one assertion is the same defect as two computations for one
question.
ActivityFact ⊂ MeasureFact. Activity is a measure normalised to 0–1. A
separate family buys nothing and creates a second place for "how busy is this".
CapacityFact ⊂ MeasureFact. A capacity is a measure with a limit and a
flag for whether the limit is enforced. Folding it preserves the
constitutional rule that a meter may only be drawn against a real constraint,
provided enforced travels with it. Trade-off: this makes the enforced-limit
rule a field convention rather than a type distinction. I recommend folding, and
flag it as the one reduction that trades a little safety for minimality.
Minimal set — four families:
| Family | Asserts |
|---|---|
condition |
A named condition holds of a subject |
measure |
A subject has a quantity (with optional limit + enforced) |
exchange |
Something moved between two subjects |
placement |
An actor is at a subject, from an instant |
Everything the seven expressed remains expressible. Nothing domain-specific survives.
5. place and legend fail — and so does part of world
The question that settles it: is a building's position a property of the operational world, or of one way of looking at it?
A Salesforce opportunity has no coordinates. A CLI consumer needs no plots. A JSON API has no districts. Position is not a fact about reality; it is a fact about a chosen projection.
But plot stability cannot be per-renderer either — two renderers placing the
same subject differently would violate Article I.3. So place and legend
belong to a projection layer: one canonical spatial interpretation, shared by
every renderer, sitting between core and renderers.
core/ reality — subjects, facts, conditions, time
projection/ interpretation — places, legend, quantisation, scene
renderers/ pixels — SVG, R3F, JSON, CLI
This resolves a tension I had left unexamined: the Spatial Constitution governs the projection layer, not the core. Articles II and III describe how reality is shown; Articles I, VI and XI describe what is true. Both remain binding; they simply bind different layers. No amendment is required — the constitution never claimed geometry was a property of reality.
world therefore keeps state and sheds geometry: today's World mixes both,
which is why world/types.ts needs Vec3.
6. actor is reducible
Why it seemed necessary. Article V demands identity, ownership, memory, movement and history without redesign.
Test each against Subject + Fact:
| Article V requirement | Expressible without an Actor module? |
|---|---|
| Identity | Yes — subject URN, actor kind |
| Movement | Yes — placement facts over time |
| History | Yes — facts are timestamped and append-only |
| Memory | Yes — facts about an actor subject |
| Collaboration | Yes — exchange facts between actor subjects |
| Ownership | Yes — a declared relation in tenant data, not an observation |
All six survive. Actor is a Subject of kind actor that can hold
placements — no separate module earns its place.
Cost of the reduction, stated honestly: type safety. With a distinct Actor
type the compiler prevents placing a repository at a building. Reduced to a
subject kind, that becomes a runtime check. I judge the minimality worth it —
the core is meant to be small enough to hold in your head — but it is a real
trade and you should know I made it.
7. The dependency graph
Target — by construction
┌───────────────────────────┐
│ core/ │
│ time evidence subject │ imports: node: builtins only
│ condition fact world │
└────────────┬──────────────┘
│ (everything below imports core; core imports nothing)
┌──────────────┬───────────┴───────┬──────────────┬─────────────┐
▼ ▼ ▼ ▼ ▼
governance/ connectors/ tenant/ projection/ runtime/
constitution github jira roster place dispatch
ledger k8s datadog estate legend jobs
probes sap salesforce thresholds scene
│
▼
renderers/
svg r3f json cli
Permitted edges only. core has zero outgoing edges. governance verifies
core but is never imported by it — otherwise the thing being checked would
depend on its checker. connectors never import each other. renderers import
projection and core, never connectors or tenant.
Measured — today's graph fails
world/types.ts → hq/roster ✗ core → tenant
world/facts.ts → hq/roster ✗ core → tenant
world/structure.ts → hq/roster, hq/estate, hq/telemetry ✗ core → tenant, connector
world/build.ts → hq/roster, hq/state ✗ core → tenant
world/answers.ts → hq/roster, hq/state ✗ core → tenant
substrate/runtime → db, hq/roster, hq/findings, runtime/dispatch ✗
substrate/telemetry → hq/state, hq/roster, hq/estate ✗
Seven of seven modules violate the target. Zero currently satisfy it.
The proof obligation
A graph of a core that does not yet exist cannot be measured, only specified. The empirical proof arrives with Step 1 and takes this form:
core/ may import only from core/ and node: builtins.
Enforced by a lint rule and an Article XI regression test that fails the build on violation. Until that rule is green, the claim "the core has zero tenant imports" is a design intention, not a proven property — and I will not describe it as proven before then.
8. What changed as a result of this proof
| Before | After |
|---|---|
| 10 core modules | 6 |
actor a module |
a subject kind |
place, legend in core |
moved to projection/ |
governance inside core |
peer that verifies core |
| 7 fact families | 4 |
| 12 closed, SE-shaped subject kinds | 6 abstract kinds + declared subtypes |
| Spatial Constitution assumed to govern the core | governs the projection layer |
Two decisions need your acknowledgement before Step 1:
- The subject-kind replacement (§3) revises an artifact you approved.
- Folding
CapacityFactintomeasure(§4) trades a type distinction for minimality.
Everything else follows from the test as stated.