Measurement Rsnative Core

The measurement scaffold

Measurement rsnative core is the formal scaffold Recognition Science uses to record observations. It defines a ledger, a discrete record of events, in which every entry is a measurement: a value, an optional time window, an explicit protocol, an optional uncertainty, and a list of notes. The framework's core theory is native to its own units, with the fundamental tick set to one, and treats SI or CODATA values as optional external calibration that lives outside the core. This keeps the scaffold small and dependency-light, so the central claims do not rest on any particular choice of physical units.

The practical force of this framework is that it makes arbitrary choices visible. Every measurement carries a protocol, a named procedure with a status such as spec, derived, hypothesis, or scaffold. A protocol is hygienic, meaning well-formed, only if it has a nonempty name and, when it is a hypothesis or scaffold, it lists both its assumptions and its falsifiers. This means a scientist cannot hide windowing, coarse-graining, or basis choices behind a bare number. The record also supports uncertainties as either a sigma value or an interval, and notes can be appended to any measurement, so the full context travels with the value.

The scaffold defines typed quantities for the framework's native observables: ticks (the base time step), voxels (spatial cells), coherence, action, skew, cost, meaning, and qualia. Each is a quantity with a real value and a unit tag, so the type system prevents mixing, say, a tick with a cost without an explicit conversion. Windows are defined by a start tick and a length in ticks, with zero length meaning instantaneous. An observable is simply a function from a system state to a measurement, and the framework proves basic algebraic facts such as the value of a sum of quantities being the sum of their values.

In plain language, this framework establishes a discipline: before Recognition Science compares any number to experiment, that number must arrive with its recipe, its error bar, and its stated way to be wrong. Concrete observables live in separate catalog files, so the core remains a clean foundation. What this changes is that a claim in the framework can be audited not just for its mathematics but for the honesty of its measurement, because the protocol and falsifiers are part of the formal record, not an afterthought.

/-- A measurement value with protocol + (optional) time window + (optional) uncertainty. -/
structure Measurement (α : Type) where
  value : α
  window : Option Window := none
  protocol : Protocol
  uncertainty : Option Uncertainty := none
  notes : List String := []

/-- Protocol hygiene predicate (v1/v2).

Rules:
- `name` must be non-empty
- if `status` is `.hypothesis` or `.scaffold`, both `assumptions` and `falsifiers` must be non-empty -/
def hygienic (p : Protocol) : Prop :=
  p.name ≠ "" ∧
    match p.status with
    | .hypothesis | .scaffold => p.assumptions ≠ [] ∧ p.falsifiers ≠ []
    | _ => True

inductive TickUnit : Type

/-- An observable extracts a `Measurement α` from some state type `S`. -/
abbrev Observable (S α : Type) : Type := S → Measurement α

@[simp] theorem val_zero (U : Type) : (0 : Quantity U).val = 0 := rfl
@[simp] theorem val_add {U : Type} (a b : Quantity U) : (a + b).val = a.val + b.val := rfl

What this page does not claim

This module does not define any specific physical observable or experimental result. It does not derive the value of any constant or prove any physical law. It does not claim that native units are more fundamental than SI units, only that they are the framework's internal choice.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/RSNative/Core.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: