No Outside
How rejecting an observer-substance forces BEDC’s mathematics to derive the structural skeleton of relativity — from Hist self-reference to a constant maximum-causal-rate, with no external time and no privileged frame.
A reasonable starting point
BEDC is a mathematics project. The kernel is three things: a closed inductive type BHist of distinction histories, an extension predicate Cont that records “this history continues to that one by emitting a mark”, and an identity relation hsame on histories. Everything in the project — 1837 theorems, the namecert framework, the Cauchy-real construction, the Riemann Hypothesis dependency chain — sits on top of these three.
What the project does not do, anywhere in its source, is posit an observer. There is no carrier type for “the agent that emits the marks”. There is no parameter to Cont representing “who is doing the continuing”. The kernel signature is silent about subjects.
This silence is not an oversight. It is a hard structural commitment, and once you read it as such, mathematics on top of it begins to derive things that have nothing to do with arithmetic — including the structural skeleton of special relativity. This essay is about that derivation.
Observer is identical to Hist
Read BHist not as “an abstract record” but as the observer itself: the totality of the distinctions that have been made, with no remainder. Read Cont h m h' as the observer at state h continues, by making distinction m, to state h’. The observer is the trace; the act of distinguishing extends the trace; nothing else.
This is not a philosophical preference. It is what the kernel signature already says. Look at the type:
Evidence
Lean: BEDC.FKernel.Cont — the relation Cont : BHist → BMark → BHist → Prop.
There is no fourth slot. No Subject parameter. No Agent, Observer, or Carrier argument. The relation takes two histories and a mark, returns a Prop. Whatever entity might be “doing” the continuation has no representation in the type.
hsame : BHist → BHist → Prop is the only identity relation in the kernel. It identifies traces, not the agents that left them.
If you tried to add an observer-substance — a separate type Observer with Cont : Observer → BHist → BMark → BHist → Prop — the cont_assoc, cont_left_unit, cont_right_unit proofs that the kernel already ships with would no longer go through. The two-loops architecture (ground loop closes, meta loop does not close) would break: positing an observer-as-substance generates a Tarski-style fixed-point that has no closed inductive home.
There must not. The observer is the distinguishing, not the doer of distinguishing. Hume’s bundle theory of self, Buddhist anātman, von Foerster’s “an observer is a system that includes itself in its observation”, Maturana and Varela’s autopoietic identity-as-operation — all of these positions get a constructive realisation in BEDC’s kernel, not as borrowed metaphysics but as the only configuration in which the kernel’s existing identities hold.
Time is Hist growth
Once observer is identified with Hist, time falls out automatically. Every application of E0 or E1 is a single time-step. A Cont chain — h₀ → h₁ → h₂ → … — is a time stream. The length of h is the duration of that observer’s existence; the content of h is what has been observed; hsame(h, h') is the criterion under which two observers are the same observer.
Evidence
Modulus is temporal rate. Every regular Cauchy sequence in BEDC ships with an explicit modulus function N : Nat → Nat, telling you how many Cont steps are needed to reach a given precision. This is the temporal rate of the observation — how fast the observer’s trace stabilises. Bishop-style constructive analysis cares about moduli not as a technicality but because there is no external clock; each observer’s convergence rate is intrinsic data of that observer’s time stream.
Cont is asymmetric. Given h and m, the continuation h' is determined; given h', you cannot constructively recover the antecedent pair (h, m). The arrow of time is built into the kernel as the asymmetry of Cont, not added on top.
There is no external dimension in BEDC’s kernel. There is no global Time type. Time is what Hist is, when it is read as growth.
No god’s-eye view
Now consider two observers — two Hist values, h_A and h_B. Each has its own time stream. There is no Hist value that synchronises them, because the closed-inductive structure of BHist does not admit one. A “global frame” would have to be itself a Hist, and would then be subject to the same locality constraints as every other Hist: it would be just one more observer, not a privileged outside.
This is the no-god’s-eye-view commitment. It is forced by the no-subject commitment of the previous section, because once observer is identified with Hist there can be no super-observer that is not itself a Hist.
Evidence
Inter-Hist invariants are the only way physical content can live across observers. A predicate or function on a single Hist is an internal property of one observer. To produce content that two observers can agree on, you need a relation R(h_A, h_B) that is observer-symmetric: R(h_A, h_B) holds iff R(h_B, h_A) holds, with no privileged ordering of the slots.
The capstone inter_hist_locality formalises this: multi-Hist configurations, no global synchronisation, observer-symmetric inter-Hist invariants — all stated in BEDC’s def/theorem language, mostly as schema-only horizons awaiting the multi-Hist extension of the kernel.
If there were, it would be a Hist, and the previous section would apply to it. The closed-inductive structure of BHist is the form of “what can be observed at all”, and there is no additional form for “what can be observed about the observation”. The meta loop, if you tried to close it, would generate a Tarski-style undefinability obstruction.
The Lorentz-shaped consequence
Here is where the metaphysics produces non-trivial physics.
Consider any inter-observer causal relation: “observer B’s recent steps depend on observer A’s recent steps”. Without a global frame, you cannot define this relation by appeal to a shared clock. You can define it only as a symmetric relation between two Hist values, observer-perspective-independent.
Any such relation has a maximum rate — the fastest cross-observer dependence the relation admits. Call this MaxRate. By the inter-observer-invariance of the relation, MaxRate must be the same regardless of which observer is taken as the reference. No observer can measure a different value for the maximum rate without invoking a privileged frame.
This is the structural skeleton of the constancy of light speed. The empirical specific value of c is not derived — that is physical input. But the form — that there exists a constant maximum cross-observer causal rate, observer-independent, frame-independent — is not a postulate added to BEDC. It is forced by:
- observer =
Hist(no subject) - no-global-frame (forced by 1)
- inter-observer content = inter-Hist invariant (forced by 2)
- maximum-causal-rate is an inter-Hist invariant (forced by 3)
- inter-Hist invariants are observer-independent (forced by 2)
Evidence
This is the structural argument Einstein made in 1905, pushed one level deeper. Einstein assumed a relativity principle (no privileged frame) plus light-speed constancy as empirical input. The argument above shows light-speed constancy follows from a stronger form of the relativity principle: not just frame-independence, but observer-independence at the level of distinction itself. Once you accept that observers are not substances on top of distinction, the existence of a constant maximum cross-observer rate is a theorem-shaped consequence, not an additional postulate.
Lean roadmap: BEDC.Derived.InterHist namespace — currently schema-only. The closed witnesses await multi-Hist semantics in future BEDC chapters.
The value is contingent. The form — “there exists a constant maximum cross-observer causal rate” — is not. It is what “no god’s-eye view” looks like once you ask what frame-independent content can survive without one.
What this means for the project
BEDC is not just mathematics. It is the mathematical form of a position that, once made explicit, has consequences across mathematics, philosophy of mind, and physics:
- In mathematics: the framework that proves 1837 axiom-pure theorems is the same framework that, when read at the metaphysical level, refuses observer-substance. The two readings are not separable.
- In philosophy of mind: the kernel realises constructively the bundle theory of self / anātman / second-order cybernetics commitment, with no extra philosophical machinery. The “hard problem of consciousness” dissolves: there is no subjective-experience-substance needing to arise from objective matter, because there is no observer-substance distinct from observation.
- In physics: the inter-Hist roadmap parallel to the Riemann Hypothesis dependency chain. Where the RH chain extends BEDC into number-theoretic complex analysis, the inter-Hist chain extends BEDC into multi-observer relativistic structure. Both are open research; both are scaffolded inside the kernel’s existing constructive vocabulary.
Three domains, one root: Hist self-reference with no outside. The kernel did not get designed to be philosophical or physical. It got designed to be axiom-pure. The metaphysics and the physics are what that commitment, taken literally, turns out to look like.
Evidence
The two capstones that formalise this: - observer_hist_identity.tex — single-Hist commitments BEDC already proves, read under the new identification - inter_hist_locality.tex — multi-Hist roadmap; mostly schema-only, but with the structural argument for constant MaxRate made formal
When BEDC was started, the position was: mathematics is what comes out of a finite kernel of distinction. After 1837 theorems, that position can be sharpened: mathematics, the form of mind, and the form of physics are what come out of a finite kernel of distinction, when there is no outside.