weight_observable
plain-language theorem explainer
weight_observable defines the weight proxy w(alpha, cLag, Tdyn, tau0) as 1 plus alpha times cLag times exp(alpha log(Tdyn/tau0)). Researchers establishing continuity of observables in the weak-field GR limit of Recognition Science would cite this definition when constructing proxy models. The definition is a direct expression chosen to remain well-defined for positive Tdyn and tau0 without invoking real powers.
Claim. $w(alpha, c_{Lag}, T_{dyn}, tau_0) := 1 + alpha c_{Lag} exp(alpha log(T_{dyn}/tau_0))$
background
The Observable Limits module constructs four proxy observables that recover general-relativity values when deviation parameters approach zero. weight_observable supplies the first of these, the weight function w, which depends on two small parameters alpha and cLag together with a dynamical time Tdyn and the fundamental tick duration tau0. tau0 is imported from Constants.tau0 (and its Compat and Derivation variants) as the duration of one tick in RS-native units; the algebraic comp from CostAlgebra is listed among dependencies but is not invoked inside this definition.
proof idea
This is a direct definition. It first binds A to the ratio Tdyn/tau0, then returns the explicit expression 1 + (alpha * cLag) * Real.exp(alpha * Real.log A). No lemmas or tactics are applied; the form is written out to guarantee domain safety for positive arguments.
why it matters
The definition supplies the concrete weight proxy whose continuity is proved in the immediately following theorem weight_gr_limit and whose simultaneous limit with the gamma, beta and c_T^2 proxies is recorded in observables_bundle_gr_limit. It therefore occupies the first slot in the module's demonstration that all four observables reduce to their GR values by continuity alone. Within the Recognition Science framework this step belongs to the GR-limit section of the relativity development, where small parameters alpha and cLag are taken to vanish.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.