Admissible Semantic Continuations: A Metalanguage of Continuation Structure, Its Meaning Algebra, and the Limits of Observational Reconstruction

A world may be described by listing its objects and their properties. It may also be described by recording, at every realised history, which continuations are admissible. This paper develops the second description in full. The basic object is the continuation space C(h) = {x : hx is admissible}; meaning is an effect on continuation structure; a law is a filter on continuations; and an object is a stable pattern of continuations rather than a bearer of attributes.From this single primitive we reconstruct, in order, a semantic quotient and its internal language, a continuation geometry in which distinguishing depth behaves as anultrametric, a descent theory that glues local presentations into a global semantic space, an algebra of meaning with three operation symbols, a logic of reflective conditions, a space of theories with its self-referential boundary, and finally the theory of projection and observation. The last layer yields the endpoint of the programme: relative to a declared class of admissible observations, science determines the operational object Sop = S/ ker ηS and its observer diagram, not the ontic source S. The quaternion and dihedral groups of order eight witness the gap: they are non-isomorphic, their complete strict-quotient diagrams are isomorphic, and their common operational object is the Klein four-group.The negative results carry the same weight as the positive ones and are stated with the same precision. A source distinction need not be semantic; an immediate effect need not be a semantic effect; semantic structure does not determine utility; correspondence does not supply a causal channel; a Boolean semantic carrier does not force a Boolean logic of conditions; closure axioms do not identify a reflector; a jointly false equation can be exactly true for every observer in an incomplete family. Each is proved by an explicit finite countermodel.The theory is supported by two independent layers of evidence. The first is a corpus of thirty-three sealed experiments covering versions v0.3 through v0.38, each with a preregistered protocol, a pre-outcome hash freeze, negative controls, per-world relabelling of surface symbols, and a byte-level replay audit. The second is a machine-checked development in Lean 4 with Mathlib: forty-two modules and about ten thousand seven hundred lines certifying three hundred and thirty-six claims, of whichtwo hundred and forty-four are proved and ninety-two are refutations with explicit countermodels. The development contains no sorry, introduces no axiom, and forbidsnative_decide; its headline theorems reduce to propext, Classical.choice and Quot.sound. Every point at which the formal statement is weaker than the informal one is recorded in a register of downgrades, reproduced here as an appendix. Two claims the theory does not make are stated as plainly as the theorems: the hypothesis that theobserved world is a projection of a richer semantic source remains a hypothesis, and Gödel incompleteness is neither formalised nor derived anywhere in the development.