New to this research? This article is part of the Reflexive Reality formal research program. Brief introduction ↗ · Full research index ↗
Series: NEMS on Logic and Mathematics · Part 4: The No-Free-Bits Principle
Every theory makes claims. Some of those claims are genuinely supported by the theory’s internal structure. Others are silently imported from outside — hidden assumptions, implicit selectors, free bits that the theory didn’t earn. The No-Free-Bits calculus is a formal accounting tool that detects exactly this: when a theory is determining facts from within, and when it is outsourcing determinacy to an invisible external source. It is the most general closure audit tool in the program.
The Fundamental Question
Here is a question that should be asked of every theory: does it determine what it claims to determine from within its own resources, or does it secretly depend on something outside itself to make the determination?
This sounds abstract until you see how often the answer is “secretly depends on something outside.” Consider:
- A probability theory that assigns probability 1/6 to each face of a die — but provides no internal resource that selects which face lands up. The probability assignment is complete; the actual outcome determination is outsourced to unspecified physical mechanisms.
- A theory of consciousness that assigns qualia to neural states — but provides no internal resource that explains why these particular qualia and not others. The assignment is claimed, but the determination is outsourced to… what exactly?
- A physical theory with free parameters — fine-structure constant, cosmological constant, particle masses — where the values are observed but not derived. The structure is specified; the values are outsourced to initial conditions, selection effects, or “that’s just how it is.”
- An AI system that claims to have determined the safest action — but used evaluators who share the same biases. The determination is claimed; the objectivity is outsourced to a fiction of independence.
The No-Free-Bits calculus (Paper 27) is a formal framework for detecting exactly this kind of outsourcing — and for distinguishing legitimate theories (which earn their determinations internally) from those that import hidden free determinacy.
The Formal Framework
Paper 27 builds an abstract closure audit calculus. The core construction: an observational semantics Holds : World → Obs → Prop inducing an observational equivalence on worlds — two worlds are equivalent if they are indistinguishable by any observation. The world-type of a world is its equivalence class under this observational equivalence.
The key definitions:
- A selector is a function that picks a representative from each equivalence class — a way of choosing one world from each world-type. Selectors are what happens when you need to make a determination that the theory doesn’t uniquely fix.
- A free bit is a determinacy contribution that the theory does not generate internally — any determination that requires an implicit selector operating outside the theory’s internal resources.
- Audit soundness: a property P is audit-sound if it factors through world-types — if P(world) depends only on the world’s equivalence class, not on which representative of the class was selected. An audit-sound property is determined by what can be observed; a non-audit-sound property is importing extra information that observations don’t justify.
The core theorem: if a property P is decidable on world-types (factors through the observational quotient), then P is invariant under observational equivalence. Any claim that varies between observationally equivalent worlds is importing a free bit — a selector choosing between worlds that the observations cannot distinguish.
Lean anchor: AuditSoundness.audit_soundness. Machine-checked.
The Outsourcing Barrier
Paper 83 (Internality/Outsourcing Schema) extends the No-Free-Bits calculus into a general outsourcing barrier theorem. The framework: a system has a task (a determination to make). If the task is load-bearing (it actually affects what the system does) and not internally realizable (the system cannot complete it from its own resources), then completing the task requires outsourced structure — an implicit external selector.
The Generic Outsourcing Barrier: any load-bearing task that is not internally realizable requires external structure. There are no free completions — you cannot claim a determination without either providing the internal resource that makes it, or importing an external one.
The Outsourcing Witness corollary: if a theory claims to determine X but provides no internal resource for doing so, there exists an explicit witness to the outsourcing — a construction that shows precisely what external structure is being implicitly imported.
Lean anchor: InternalitySchema.generic_outsourcing_barrier, InternalitySchema.outsourcing_witness.
Applications: Auditing Theories
The No-Free-Bits calculus is a general-purpose tool for auditing theories. Here is how it applies in several domains:
Physical Theories
A physical theory with free parameters is importing free bits — the parameter values are not determined by the theory. The NEMS program applies the calculus to show that the Standard Model’s gauge group and Born rule are audit-sound under PSC: they are forced by the observational semantics, not freely chosen. Parameters that remain free (particle masses) are legitimate free bits — the theory earns its structure, but acknowledges that it does not determine everything.
Consciousness Theories
Any consciousness theory that assigns qualia to physical states without an account of why these qualia and not others is importing a free bit: the selection of which qualia attach to which states. If this selection is not determined by the theory’s internal resources, it requires an external selector. Ghost entities (hidden variables, extra physical layers) are typically such selectors — they provide the determinacy the official theory lacks but doesn’t acknowledge. Paper 27 provides the formal tool to detect this.
AI Systems
An AI system that claims to determine “the safest action” but uses evaluators with overlapping coverage sets is importing a free bit: the implicit selection of which evaluator’s judgment is authoritative. The diversity necessity theorem (Paper 31) is a direct consequence of the No-Free-Bits calculus: genuine coverage requires diverse selectors, because a single selector (or correlated selectors) imports all their shared biases as free bits.
Mathematical Foundations
The axiom of choice in set theory is the canonical example of a free bit in mathematics: it asserts a selector exists (a function that picks a member from each non-empty set) without specifying what it is. Under the No-Free-Bits calculus, this is a legitimate outsourcing acknowledgment — the axiom honestly says “we import this selector” rather than hiding the import. The calculus makes the distinction between honest outsourcing acknowledgment and hidden outsourcing precise.
The Papers and Proofs
- Paper 27 — A No-Free-Bits Calculus for Determinacy and Outsourcing
- Paper 83 — Internality/Outsourcing Schema
Lean proof library: novaspivack/nems-lean · Full research index: novaspivack.com/research ↗