lunar-time-budget (tipo de cenário)
Tipo de cenário do motor v0.40.0, família Lunar e cislunar. Consultivo: saída de análise de uma ferramenta de pesquisa e engenharia, não um equipamento de navegação homologado e não um serviço de segurança da vida humana. Todo rótulo aqui é do motor ou da matriz de verificação; um tipo de cenário é MODELLED a menos que a matriz diga outra coisa (como um rótulo é obtido: a seção Evidence do README).
O que faz#
Orçamento de erro de tempo de ponta a ponta do Tempo Lunar Coordenado (LTC), MODELLED: os sete termos de erro do LTC montados como curvas de erro de tempo x_i(τ) sobre toda uma grade de tempos de média, somados em raiz em x_Σ(τ), e o τ de CRUZAMENTO relógio-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 artefato de um único τ. As inclinações em τ são de forma fechada e verificáveis analiticamente (relógio τ^{+1/2}/τ^{+1}, pisos τ^0, medição τ^{-1/2}) e as linhas de relógio reproduzem as especificações publicadas de relógio de um dia (crate::clock_specs); as MAGNITUDES dos pisos do enlace de RF/óptico, da realização do referencial, do resíduo relativístico e das efemérides são alocações modeladas do orçamento (valores padrão documentados, substituíveis por quem chama), não medições. A contribuição é o τ de cruzamento reproduzível, não um número certificado por termo; não certificado para a manutenção operacional da hora.
Uma execução de scenarios/lunar-time-budget.toml resume-se assim: lunar-time-budget | clock passive-h-maser | 7-term x_Σ(τ) over 57 τ-points (1–1e7 s) | crossover τ 8.689e4 s (x 1.001e-9 s) | frame floor 1.001e-9 s | clock 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:
| Campo | Valor | Unidade |
|---|---|---|
clock |
passive-h-maser | texto |
kind |
lunar-time-budget | texto |
Execute#
kshana scenarios/lunar-time-budget.toml
2 cenários incluídos usam este tipo de cenário; os demais estão em scenarios/.
O que ele fornece#
Os resultados escalares dessa execução, com as unidades que o motor declara:
| Resultado | Valor | Unidade |
|---|---|---|
clock |
passive-h-maser | texto |
crossover_tau_s |
86894.284677 | s |
crossover_x_s |
1.0007e-9 | s |
evidence.id_rule |
o id estável da linha da matriz (o ID | texto |
evidence.matrix |
docs/VERIFICATION-MATRIX.md | texto |
evidence.tier |
MODELLED | texto |
frame_term_s |
1.0007e-9 | s |
Rótulo do resultado (o do motor): orçamento de erro de tempo do LTC de ponta a ponta, MODELLED. As inclinações em τ são de forma fechada e verificáveis analiticamente (relógio τ^{+1/2}/τ^{+1}, pisos τ^0, medição τ^{-1/2}) e as linhas de relógio reproduzem as especificações publicadas de relógio de um dia; as MAGNITUDES dos pisos do enlace de RF/óptico, da realização do referencial, do resíduo relativístico e das efemérides
Evidências#
MODELLED: as linhas da matriz de verificação que nomeiam este tipo de cenário.
- MODELLED Uma execução do lunar-time-budget emite uma linha de cruzamento relógio-referencial por classe de relógio contra um único termo de referencial compartilhado, de modo 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 padrão a classe miniRAFS, ou qualquer classe nomeada, ou uma ficha de dispositivo ajustada a pontos de estabilidade declarados) disciplinado ao Tempo Lunar Coordenado e Testes: 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 são nomeadas ali):
- MODELLED Portões determinísticos, com hash de cenário, de SBOM e de golden entre plataformas. Referência independente (ExternalDataset): aderência à norma do SBOM ao JSON Schema oficial do CycloneDX 1,5 (+ identificadores SPDX válidos) — um padrão externo publicado, zero erros de validação em todo o grafo de dependências; a parte de determinismo das FoMs / reprodutibilidade byte a byte continua sendo uma verificação de autoconsistência fixada, de modo que a linha permanece MODELLED
- MODELLED Uma execução do lunar-time-budget emite uma linha de cruzamento relógio-referencial por classe de relógio contra um único termo de referencial compartilhado, de modo que o relógio é a única variável da comp. Referência independente (InternalConsistency): duas computações diferentes dentro da base de código para a mesma grandeza, e não uma só reformulada: a bisseção sobre a curva de lei de potência da IEEE-1139 nada sabe sobre o tipo de ruído, enquanto a forma fechada inverte algebricamente o tipo dominante, de modo que um tipo de ruído mal classificado ou um intervalo inicial ruim aparece como uma diferença relativa que não é minúscula. Os quatro valores também reproduzem a tabela publicada do artigo até metade do seu último dígito impresso -- mas essa tabela era a sua
- MODELLED O cenário lunar-time-budget publica as suas saídas em forma de arranjo como uma tabela em formato longo (índice da grade, tempo de média, termo) ao lado do relatório, de modo que os sete por. Referência independente (InternalConsistency): apenas autoconsistência: o total publicado é verificado contra a raiz da soma dos quadrados dos termos no mesmo arquivo, e a curva emitida reproduz o p3_time_budget_curve.csv divulgado em todos os 57 pontos. As duas verificações compartilham as próprias definições de termos deste motor, de modo que nenhuma é independente. O termo do relógio se apoia em especificações publicadas de relógios, mas as MAGNITUDES dos pisos de enlace, de referencial, relativístico e de efemérides são documentadas
Limitações#
O que o próprio relatório da execução diz que não é modelado ou não é validado:
- Orçamento de erro de tempo do LTC de ponta a ponta, MODELLED. As inclinações em τ são de forma fechada e verificáveis analiticamente (relógio τ^{+1/2}/τ^{+1}, pisos τ^0, medição τ^{-1/2}) e as linhas de relógio reproduzem as especificações publicadas de relógio de um dia; as MAGNITUDES dos pisos do enlace de RF/óptico, da realização do referencial, do resíduo relativístico e das efemérides são alocações modeladas do orçamento (valores padrão documentados, substituíveis por quem chama), não medições. A contribuição (resultado
label) - Orçamento de erro de tempo de ponta a ponta do Tempo Lunar Coordenado (LTC), MODELLED: os sete termos de erro do LTC montados como curvas de erro de tempo x_i(τ) sobre toda uma grade de tempos de média, somados em raiz em x_Σ(τ), e o τ de CRUZAMENTO relógio-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 artefato de um único τ (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}, pisos tau^0, medição tau^{-1/2}) e as linhas de relógio reproduzem as especificações publicadas de relógio de um dia; mas as MAGNITUDES dos pisos do enlace de RF/óptico, da realização do referencial, do resíduo relativístico e das efemérides são alocações modeladas do orçamento (valores padrão documentados, substituíveis por quem chama), não medições. A contribuição é (comentário do arquivo de cenário, linhas 13 a 18)
- Reprodutibilidade e garantia de software é MODELLED, não validada: uma subafirmação é verificada externamente, mas a capacidade inteira compõe peças modeladas, de modo que a capacidade permanece modelada. (matriz de verificação (docs/MODELLED-RATIONALE.md))
- A tabela de cruzamento de tempo lunar por classe de relógio é MODELLED, não validada: verificada contra a sua própria identidade analítica ou de forma fechada, o que detecta erros de transcrição e de coeficientes, mas não é uma referência externa independente. (matriz de verificação (docs/MODELLED-RATIONALE.md))
- A reprodutibilidade do orçamento de erro de tempo lunar é MODELLED, não validada: verificada contra a sua própria identidade analítica ou de forma fechada, o que detecta erros de transcrição e de coeficientes, mas não é uma referência externa independente. (matriz de verificação (docs/MODELLED-RATIONALE.md))
Veja também#
- Página da família: Lunar e cislunar
- Todos os tipos de cenário: KINDS.md
- Página do tema: LUNAR-REFERENCE-STATION.md
- Página do tema: integrations.md