w_t_display
plain-language theorem explainer
w_t_display supplies a convenience wrapper that evaluates the time-dependent weight in the ILG gravity model by locking the configuration to defaults and extracting the fundamental tick duration from supplied bridge data. Display-layer code in the TruthCore module cites this entry point for rendering results without exposing internal configuration choices. The definition reduces directly to a single application of the underlying w_t_with function.
Claim. Let $P$ be a parameter record containing components $alpha$, $C_{lag}$, $A$, $r_0$, $p$, and $h_z/R_d$, and let $B$ be a bridge record containing the tick duration $tau_0$. Then $w_t(P,B,T_{dyn}) := w_t^{with}(defaultConfig, P, T_{dyn}, B.tau_0)$, where $T_{dyn}$ denotes dynamical time.
background
The Params structure assembles the six numerical inputs required by the ILG model: the fine-structure constant alpha, a lag coefficient Clag, an amplitude A, a reference scale r0, an exponent p, and the vertical-to-disk scale ratio hz_over_Rd. BridgeData supplies the external anchor tau0, which is defined in the Constants module as the duration of one recognition tick and is also derived in Constants.Derivation from the combination of hbar, G, and c in RS-native units.
proof idea
One-line wrapper that applies w_t_with to defaultConfig, the supplied Params, the dynamical time Tdyn, and the tau0 field extracted from the BridgeData record.
why it matters
The definition feeds the display routine ILG_w_t_display in TruthCore.ILGDisplay, which simply forwards the call. It therefore supplies the public interface for time-dependent quantities inside the gravity sector of Recognition Science, where the underlying w_t_with computation rests on the phi-ladder and the eight-tick octave fixed by the T7-T8 steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.