StructuralDerivation
plain-language theorem explainer
A structural derivation packages one internal deduction chain inside a physics framework: a numeric id, a countable step map to dimensionless elements, a distinguished output, input elements, and a flag that only internal structure was used. Exclusivity and zero-parameter arguments cite this as the carrier for finitary internal deductions. The declaration is a plain structure plus a one-line output predicate (equality to the distinguished element or membership in the step trace).
Claim. For a physics framework $F$, a structural derivation consists of an identifier $n\in\mathbb{N}$, a step map $\mathbb{N}\to$ (dimensionless elements of $F$), a distinguished produced element, a finite list of input elements, and a proposition asserting that the derivation uses only internal structure. An element $e$ is produced by the derivation if $e$ equals the distinguished output or $e$ equals the step map at some natural number.
background
This module supplies shared carriers for the NoAlternatives and necessity developments, so those proofs need not import each other. A physics framework is the minimal interface: a state space, an evolution map, an observable type, a measurement map from states to observables, and existence of initial conditions.
Dimensionless elements ("knobs") of a framework pair a natural id, a concrete state witness, and a real value. That encoding lets later arguments treat parameters and derived quantities as finitary objects tied to states rather than free real constants.
Structural derivations mirror measurement procedures in the same file: both keep a numeric identifier and a countable trace of element outputs. The intent is bookkeeping for internal deductions that stay inside the framework's own structure, as opposed to external parameter insertion.
proof idea
No proof obligation: this is a structure declaration. Fields are raw data (id, step, produces_element, input_elements) plus an unconstrained Prop field uses_only_internal_structure left for callers to inhabit.
The companion predicate StructuralDerivation.produces is a one-line definitional expansion: the target element equals the distinguished output, or it appears as step n for some natural n. No lemmas are applied.
why it matters
Exclusivity and necessity arguments need a uniform type for "what the framework derives from itself" before they can state zero-parameter or no-alternative claims. This structure is that carrier, sitting beside siblings such as measurement procedures, non-static dynamics, zero-parameter hypotheses, observable-derivation interfaces, and framework isomorphisms.
In the Recognition Science forcing picture, internal structural derivation is how constants and observables are supposed to arise (J-cost uniqueness, phi as fixed point, eight-tick period, D = 3) rather than by free knobs. The uses_only_internal_structure field is the hook those later theorems will discharge or refute.
No downstream theorems are wired yet in the graph (used_by is empty); the declaration exists to break circular imports between NoAlternatives and the necessity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.