Metatron is a proof-carrying developmental computer.
The trusted runtime remains deliberately tiny:
Node(kind, payload, premises) Log = tuple[Node, ...] append(Log, Node) -> Log
Everything richer is derived semantics or external policy.
warrant log -> objective world + observer dynamics -> observer-accessible lawful future observations -> compute continuation-safe behavioral quotient -> acquire minimum genuinely novel interface extension when needed -> synthesize missing observations from reusable constructors -> future-demanded residual -> minimum certified causal repair frontier -> earn safe swaps modulo FutureEq -> minimum behavioral commutation basis -> behavioral trace components / finite causal quotient -> independent verification -> warranted promotion -> global reclosure
Blind V3 established the arity-one minimum-basis law. Residual Synergy and Blind Causal Repair established order-sensitive compositional repair. Finite Poset Connectivity removed arbitrary serialization. Earned Commutation discovered exact safe swaps from anonymous transition consequences.
Behavioral Commutation V0 now goes further: raw states need not commute. If two action orders differ only inside the continuation-safe behavioral quotient, Metatron may lawfully identify them.
In the blind quotient-relative test, 4 raw-state commuting pairs expanded to 5 behaviorally commuting pairs; the extra pair changed internal state but no lawful future observation could expose the difference. The 24 schedules collapsed into exactly two behavioral trace classes of size 12, matching independently computed behavioral semantics.
Blind Future Quotient V0 now removes the supplied quotient too: from anonymous transitions plus protected test outcomes alone, Metatron recovered the exact greatest continuation-safe finite partition, exhaustively verified maximal admissibility, and then recovered the same strict behavioral-commutation gain.
Embedded Observer Ontology V0 now places the observer inside the formal system. Absolute world/observer dynamics stay objective, while the observer's current lawful interface induces a mathematically determined relational identity over the world. The same absolute dynamics can therefore support different observer-relative quotients without making those quotients arbitrary or subjective. If a learning transition is already lawful, the current future-equivalence already anticipates it.
Novel Capability Genesis V0 now isolates genuine invention as a strict extension of that lawful interface. In a blind finite test Metatron found that no single new test sufficed, recovered a minimum two-capability interface extension, and preserved the full family of equivalent minimum realizations.
Residual-Generated Capability V0 then removes the supplied completed-candidate list. Given only reusable anonymous observation atoms plus XOR as a constructor, Metatron generated the closure itself and discovered a two-expression invented basis where primitive-only acquisition required three observations.
The Lean Kernel controller remains an external engineering wedge; none of this enlarges Nucleus authority.
See:
- spec/METATRON_V1_INTEGRATION.md
- spec/BEHAVIORAL_COMMUTATION_V0.md
- spec/BLIND_BEHAVIORAL_COMMUTATION_V1_PREREG.md
- spec/BLIND_FUTURE_QUOTIENT_V0_PREREG.md
- spec/EMBEDDED_OBSERVER_ONTOLOGY_V0.md
- spec/NOVEL_CAPABILITY_GENESIS_V0.md
- spec/BLIND_NOVEL_CAPABILITY_V0_PREREG.md
- spec/RESIDUAL_GENERATED_CAPABILITY_V0.md
- spec/BLIND_RESIDUAL_GENERATED_CAPABILITY_V0_PREREG.md
- spec/EARNED_COMMUTATION_BASIS_V0.md
- spec/FINITE_POSET_TOPOSORT_CONNECTIVITY_V0.md
- spec/CAUSAL_TRACE_QUOTIENT_V0.md
- spec/CAUSAL_REPAIR_COVER_V0.md