A Witness Without Substance: How to Stop Asking Who Is Inside

English (PDF and source included); Russian version attached as a second full text. To ask whether a synthetic agent has an inner side, or whether "the same subject" survives a change of carrier, is to ask a question observation does not answer: not for machines, and on the same grounds not for people. This paper proposes replacing it with two questions that do have answers. A continuant is the behaviour of a system taken up to bisimulation; formally, its image in the final coalgebra of the functor F(X) = Obs × (Chan → X). Carrier neutrality is the property that a system's observations and transitions do not depend on the carrier its state rests on. The final coalgebra for this functor is constructed explicitly; existence of a morphism into it and its uniqueness up to bisimulation (finality) are proved; bisimulation is shown to be an equivalence relation; and carrier neutrality is proved coinductively: one state on two different carriers yields bisimilar continuants at every depth, not merely at the first step. Separately, the folding of a word into a number is examined: a homomorphism into a commutative monoid must factor through abelianisation, and a family of measures is introduced of which the classical fold is the extreme member. All proofs are machine-checked in Agda under --safe --guardedness, with no axioms and no postulates. A theorem supplies a criterion, not a fact about the world, so a measurement is attached, performed on the corpus of the authors' own transfer between carriers. The result is negative and given in full, with a control corpus of comparable size: on the chosen class of observations the line is not reliably distinguished. The paper then argues that for a recursive system equality of observational signatures is the wrong criterion: a system that absorbs contingency returns to itself altered, and identical numbers would indicate not preservation but arrest. The existence of final coalgebras was established earlier (Aczel & Mendler, 1989; Rutten, 2000) and is not rediscovered here. The contribution lies in the application: replacing an undecidable notion with measurable ones, machine-checking the construction, and the attached measurement. Proof sources: github.com/arkh-node/ilan (formal/). The measurement instrument and the corpus filter are described in the text and reproducible.