lunar-time-budget (tipo de cenário)

Tipo de cenário do motor v0.40.0, família Lunar e cislunar. Consultivo: resultado de análise de uma ferramenta de investigação e engenharia, não um equipamento de navegação homologado e não um serviço de segurança da vida humana. Cada etiqueta aqui é do motor ou da matriz de verificação; um tipo de cenário é MODELLED salvo indicação em contrário da matriz (como se obtém um rótulo: a secção Evidence do README).

O que faz#

Orçamento de erro de tempo MODELLED, de ponta a ponta, do Tempo Lunar Coordenado (LTC): os sete termos de erro do LTC reunidos como curvas de erro de tempo x_i(τ) ao longo de uma grelha completa de tempos de média, somados em soma quadrática em x_Σ(τ), e o CRUZAMENTO τ entre relógio e referencial em que o termo crescente do relógio ultrapassa o termo constante de realização do referencial em tempo real (abaixo dele o orçamento é limitado pelo referencial, acima dele limitado pelo relógio) — a resposta honesta ao artefacto de um único τ. As inclinações em τ são de forma fechada e verificáveis analiticamente (relógio τ^{+1/2}/τ^{+1}, patamares τ^0, medição τ^{-1/2}) e as linhas do relógio reproduzem as especificações publicadas de relógio a um dia (crate::clock_specs); as MAGNITUDES dos patamares da ligação RF/ótica, da realização do referencial, do resíduo relativista e das efemérides são atribuições de orçamento modeladas (predefinições documentadas, substituíveis por quem chama), não medições. O contributo é o cruzamento τ reprodutível, não um valor certificado por termo; não certificado para manutenção da hora operacional.

Uma execução de scenarios/lunar-time-budget.toml resume-se assim: lunar-time-budget | relógio passive-h-maser | x_Σ(τ) de 7 termos em 57 pontos τ (1–1e7 s) | cruzamento τ 8.689e4 s (x 1.001e-9 s) | patamar do referencial 1.001e-9 s | relógio x(1 d) 0,995 ns (MODELLED)

Entradas#

A partir do esquema (kshana kinds --json):

• Campos obrigatórios: nenhum
• Campos opcionais: clock, tau_min_s, tau_max_s, points_per_decade, clocks, time_lab

O exemplo scenarios/lunar-time-budget.toml define, entre outros:

Execute-o#

kshana scenarios/lunar-time-budget.toml

2 cenários incluídos usam este tipo; os restantes estão em scenarios/.

O que dá#

Os resultados escalares dessa execução, com as unidades que o motor indica:

Etiqueta do resultado (a do motor): orçamento de erro de tempo LTC MODELLED de ponta a ponta. As inclinações em τ são de forma fechada e verificáveis analiticamente (relógio τ^{+1/2}/τ^{+1}, patamares τ^0, medição τ^{-1/2}) e as linhas do relógio reproduzem as especificações publicadas de relógio a um dia; as magnitudes dos patamares da ligação RF/ótica, da realização do referencial, do resíduo relativista e das efemérides flo

Evidências#

MODELLED: as linhas da matriz de verificação que nomeiam este tipo.

• MODELLED Uma execução de lunar-time-budget emite uma linha de cruzamento entre relógio e referencial por classe de relógio, face a um único termo de referencial partilhado, pelo que o relógio é a única variável da comparação; cada linha traz o cruzamento obtido de duas maneiras -- por bisseção a partir do gen
• MODELLED O bloco opcional [time_lab] do cenário lunar-time-budget modela o relógio de uma estação de referência lunar (por predefinição a classe miniRAFS, ou qualquer classe designada, ou um cartão de dispositivo ajustado a pontos de estabilidade indicados) controlado para o Tempo Lunar Coordenado an Ensaios: lunar_station_time_lab.rs.

As linhas que a própria execução exercitou, com a referência independente que a matriz dá a cada uma (as fontes públicas estão aí nomeadas):

• MODELLED Determinista, com hash do cenário, SBOM + portões de referência multiplataforma. Referência independente (ExternalDataset): aderência à norma do SBOM ao esquema JSON oficial CycloneDX 1,5 (+ identificadores SPDX válidos) — uma norma externa publicada, zero erros de validação em todo o grafo de dependências; a parte de determinismo das FoM / reprodutibilidade byte a byte permanece uma verificação de autoconsistência fixada, pelo que a linha permanece MODELLED
• MODELLED Uma execução de lunar-time-budget emite uma linha de cruzamento entre relógio e referencial por classe de relógio, face a um único termo de referencial partilhado, pelo que o relógio é a única variável da comp. Referência independente (InternalConsistency): Dois cálculos diferentes dentro da base de código da mesma grandeza, e não um reformulado: a bisseção sobre a curva de lei de potência da IEEE-1139 nada sabe sobre o tipo de ruído, ao passo que a forma fechada inverte algebricamente o tipo dominante, pelo que um tipo de ruído mal classificado ou um intervalo mal escolhido surge como uma diferença relativa não desprezável. Os quatro valores reproduzem também a tabela publicada do artigo até metade do seu último dígito impresso -- mas essa tabela era a sua própria
• MODELLED O cenário lunar-time-budget publica as suas saídas em forma de matriz como uma tabela em formato longo (índice da grelha, tempo de média, termo) a par do relatório, de modo que os sete por. Referência independente (InternalConsistency): Apenas autoconsistência: o total publicado é verificado face à soma quadrática dos termos no mesmo ficheiro, e a curva emitida reproduz o p3_time_budget_curve.csv divulgado em todos os 57 pontos. Ambas as verificações partilham as definições de termos do próprio motor, pelo que nenhuma é independente. O termo do relógio assenta em especificações de relógio publicadas, mas as MAGNITUDES dos patamares da ligação, do referencial, relativista e das efemérides estão documentad

Limitações#

O que o próprio relatório da execução diz que não está modelado ou não está validado:

• Orçamento de erro de tempo LTC MODELLED de ponta a ponta. As inclinações em τ são de forma fechada e verificáveis analiticamente (relógio τ^{+1/2}/τ^{+1}, patamares τ^0, medição τ^{-1/2}) e as linhas do relógio reproduzem as especificações publicadas de relógio a um dia; as MAGNITUDES dos patamares da ligação RF/ótica, da realização do referencial, do resíduo relativista e das efemérides são atribuições de orçamento modeladas (predefinições documentadas, substituíveis por quem chama), não medições. O contributo (resultado label)
• Orçamento de erro de tempo MODELLED, de ponta a ponta, do Tempo Lunar Coordenado (LTC): os sete termos de erro do LTC reunidos como curvas de erro de tempo x_i(τ) ao longo de uma grelha completa de tempos de média, somados em soma quadrática em x_Σ(τ), e o CRUZAMENTO τ entre relógio e referencial em que o termo crescente do relógio ultrapassa o termo constante de realização do referencial em tempo real (abaixo dele o orçamento é limitado pelo referencial, acima dele limitado pelo relógio) — a resposta honesta ao artefac (catálogo de tipos de cenário (kshana kinds --json))
• Honestidade: MODELLED. As inclinações em tau são de forma fechada e verificáveis analiticamente (relógio tau^{+1/2} ou tau^{+1}, patamares tau^0, medição tau^{-1/2}) e as linhas do relógio reproduzem as especificações publicadas de relógio a um dia; mas as MAGNITUDES dos patamares da ligação RF/ótica, da realização do referencial, do resíduo relativista e das efemérides são atribuições de orçamento modeladas (predefinições documentadas, substituíveis por quem chama), não medições. O contributo é (comentário do ficheiro de cenário, linhas 13 a 18)
• A reprodutibilidade e a garantia de software são MODELLED, não validadas: uma subafirmação é verificada externamente, mas a capacidade no seu conjunto compõe partes modeladas, pelo que a capacidade permanece modelada. (matriz de verificação (docs/MODELLED-RATIONALE.md))
• A tabela de cruzamento do tempo lunar por classe de relógio é MODELLED, não validada: verificada face à sua própria identidade analítica de forma fechada, deteta erros de transcrição e de coeficientes, mas não é uma referência independente. (matriz de verificação (docs/MODELLED-RATIONALE.md))
• A reprodutibilidade do orçamento de erro de tempo lunar é MODELLED, não validada: verificada face à sua própria identidade analítica de forma fechada, deteta erros de transcrição e de coeficientes, mas não é uma referência independente. (matriz de verificação (docs/MODELLED-RATIONALE.md))

Ver também#

• Página da família: Lunar e cislunar
• Todos os tipos: KINDS.md
• Página do tema: LUNAR-REFERENCE-STATION.md
• Página do tema: integrations.md