Strojový překlad, nekontrolovaný rodilým mluvčím. Referenční je anglická verze.

Stránky druhů scénářůUpravit na GitHubuZdroj: docs/kinds/by-kind/lunar-time-budget.md

lunar-time-budget (druh scénáře)

Druh scénáře enginu v0.40.0, rodina Lunární a cislunární. Pouze poradní charakter: výstup analýzy z výzkumného a inženýrského nástroje; nejde o typově schválené navigační zařízení ani o službu z oblasti bezpečnosti života. Každé označení zde pochází z enginu nebo z verifikační matice; druh je MODELLED, pokud matice neuvádí jinak (jak se označení získává: oddíl Evidence v README).

Co dělá#

MODELLED celkový rozpočet časové chyby koordinovaného lunárního času (LTC): sedm členů chyby LTC sestavených jako křivky časové chyby x_i(τ) přes celou mřížku dob průměrování, sečtených odmocninou součtu čtverců do x_Σ(τ), a PRŮSEČÍK hodin a rámce τ, ve kterém rostoucí člen hodin převýší konstantní člen realizace rámce v reálném čase (pod ním je rozpočet omezen rámcem, nad ním hodinami) — čestná odpověď na artefakt jediného τ. Sklony τ jsou v uzavřeném tvaru a analyticky ověřitelné (hodiny τ^{+1/2}/τ^{+1}, podlahy τ^0, měření τ^{-1/2}) a řádky hodin reprodukují publikované jednodenní specifikace hodin (crate::clock_specs); VELIKOSTI podlah spoje RF/optického, realizace rámce, relativistického rezidua a efemeridy jsou modelované alokace rozpočtu (zdokumentované výchozí hodnoty, volající je může přepsat), nikoli měření. Přínosem je reprodukovatelný průsečík τ, nikoli hodnota jednotlivého členu s certifikací; bez certifikace pro provozní udržování času.

Jeden běh scenarios/lunar-time-budget.toml se shrne takto: lunar-time-budget | hodiny passive-h-maser | 7členné x_Σ(τ) přes 57 bodů τ (1–1e7 s) | průsečík τ 8.689e4 s (x 1.001e-9 s) | podlaha rámce 1.001e-9 s | hodiny x(1 d) 0,995 ns (MODELLED)

Vstupy#

Ze schématu (kshana kinds --json):

  • Povinná pole: žádná
  • Volitelná pole: clock, tau_min_s, tau_max_s, points_per_decade, clocks, time_lab

Příklad scenarios/lunar-time-budget.toml mimo jiné nastavuje:

Pole Hodnota Jednotka
clock passive-h-maser text
kind lunar-time-budget text

Spusťte jej#

kshana scenarios/lunar-time-budget.toml

Tento druh používají 2 přibalené scénáře; ostatní jsou v scenarios/.

Co poskytuje#

Skalární výsledky tohoto běhu s jednotkami, které engine uvádí:

Výsledek Hodnota Jednotka
clock passive-h-maser text
crossover_tau_s 86894.284677 s
crossover_x_s 1.0007e-9 s
evidence.id_rule stabilní id řádku matice (ID text
evidence.matrix docs/VERIFICATION-MATRIX.md text
evidence.tier MODELLED text
frame_term_s 1.0007e-9 s

Popisek výsledku (od enginu): MODELLED celkový rozpočet časové chyby LTC. Sklony τ jsou v uzavřeném tvaru a analyticky ověřitelné (hodiny τ^{+1/2}/τ^{+1}, podlahy τ^0, měření τ^{-1/2}) a řádky hodin reprodukují publikované jednodenní specifikace hodin; VELIKOSTI podlah spoje RF/optického, realizace rámce, relativistického rezidua a efemeridy

Graf, který engine zapisuje pro scenarios/lunar-time-budget.toml, druh lunar-time-budget

Důkazy#

MODELLED: řádky verifikační matice, které tento druh jmenují.

  • MODELLED Jeden běh lunar-time-budget vydává řádek průsečíku hodin a rámce pro každou třídu hodin vůči jedinému sdílenému členu rámce, takže hodiny jsou jedinou proměnnou v porovnání; každý řádek nese průsečík dosažený dvěma způsoby -- půlením z obec
  • MODELLED Volitelný blok [time_lab] scénáře lunar-time-budget modeluje hodiny lunární referenční stanice (výchozí třída miniRAFS, nebo libovolná pojmenovaná třída, nebo karta zařízení nafitovaná na uvedené body stability) řízené na koordinovaný lunární čas a Testy: lunar_station_time_lab.rs.

Řádky, které běh sám procvičil, s orákulem, které matice každému dává (veřejné zdroje jsou tam uvedeny):

  • MODELLED Deterministické, hashované po scénářích, brány SBOM a zlatých výsledků mezi platformami. Orákulum (ExternalDataset): shoda SBOM s oficiálním schématem JSON CycloneDX 1,5 (+ platné identifikátory SPDX) — externí publikovaný standard, nula chyb validace přes celý graf závislostí; část o determinismu FoM / bajtové reprodukovatelnosti zůstává zafixovanou kontrolou vlastní konzistence, takže řádek zůstává MODELLED
  • MODELLED Jeden běh lunar-time-budget vydává řádek průsečíku hodin a rámce pro každou třídu hodin vůči jedinému sdílenému členu rámce, takže hodiny jsou jedinou proměnnou v por. Orákulum (InternalConsistency): Dva různé výpočty téže veličiny v kódové základně, nikoli jeden přeformulovaný: půlení na křivce mocninného zákona IEEE-1139 nic neví o typu šumu, zatímco uzavřený tvar invertuje dominantní typ algebraicky, takže chybně klasifikovaný typ šumu nebo špatné ohraničení se projeví jako nezanedbatelný relativní rozdíl. Čtyři hodnoty také reprodukují publikovanou tabulku článku na polovinu jeho poslední vytištěné číslice -- ale ta tabulka byla jeho
  • MODELLED Scénář lunar-time-budget publikuje své výstupy s hodnotami v polích jako dlouhou tabulku (index mřížky, doba průměrování, člen) vedle zprávy, takže sedm každého. Orákulum (InternalConsistency): Pouze vnitřní konzistence: publikovaný součet je kontrolován proti odmocnině součtu čtverců členů ve stejném souboru a vydaná křivka reprodukuje vydaný p3_time_budget_curve.csv přes všech 57 bodů. Obě kontroly sdílejí vlastní definice členů tohoto enginu, takže žádná není nezávislá. Člen hodin se opírá o publikované specifikace hodin, ale VELIKOSTI podlah spoje, rámce, relativistického rezidua a efemeridy jsou zdokumentované

Omezení#

Co zpráva samotného běhu uvádí jako nemodelované nebo neověřené:

  • MODELLED celkový rozpočet časové chyby LTC. Sklony τ jsou v uzavřeném tvaru a analyticky ověřitelné (hodiny τ^{+1/2}/τ^{+1}, podlahy τ^0, měření τ^{-1/2}) a řádky hodin reprodukují publikované jednodenní specifikace hodin; VELIKOSTI podlah spoje RF/optického, realizace rámce, relativistického rezidua a efemeridy jsou modelované alokace rozpočtu (zdokumentované výchozí hodnoty, volající je může přepsat), nikoli měření. Přínos (výsledek label)
  • MODELLED celkový rozpočet časové chyby koordinovaného lunárního času (LTC): sedm členů chyby LTC sestavených jako křivky časové chyby x_i(τ) přes celou mřížku dob průměrování, sečtených odmocninou součtu čtverců do x_Σ(τ), a PRŮSEČÍK hodin a rámce τ, ve kterém rostoucí člen hodin převýší konstantní člen realizace rámce v reálném čase (pod ním je rozpočet omezen rámcem, nad ním hodinami) — čestná odpověď na artefakt jediného τ (katalog druhů (kshana kinds --json))
  • Čestnost: MODELLED. Sklony tau jsou v uzavřeném tvaru a analyticky ověřitelné (hodiny tau^{+1/2} nebo tau^{+1}, podlahy tau^0, měření tau^{-1/2}) a řádky hodin reprodukují publikované jednodenní specifikace hodin; ale VELIKOSTI podlah spoje RF/optického, realizace rámce, relativistického rezidua a efemeridy jsou modelované alokace rozpočtu (zdokumentované výchozí hodnoty, volající je může přepsat), nikoli měření. Přínosem je (komentář v souboru scénáře, řádky 13 až 18)
  • Reprodukovatelnost a zajištění softwaru je MODELLED, nikoli ověřeno nezávislou referencí: dílčí tvrzení je externě zkontrolováno, ale celá schopnost skládá modelované části, takže schopnost zůstává vypočtená z modelu. (verifikační matice (docs/MODELLED-RATIONALE.md))
  • Tabulka lunárních průsečíků času podle třídy hodin je MODELLED, nikoli ověřená: je kontrolována proti vlastní identitě v uzavřeném tvaru / analytické — zachytí chyby přepisu a koeficientů, ale není vnějším orákulem. (verifikační matice (docs/MODELLED-RATIONALE.md))
  • Reprodukovatelnost lunárního rozpočtu časové chyby je MODELLED, nikoli ověřená: je kontrolována proti vlastní identitě v uzavřeném tvaru / analytické — zachytí chyby přepisu a koeficientů, ale není vnějším orákulem. (verifikační matice (docs/MODELLED-RATIONALE.md))

Viz také#