A Measurement of Excess Antenna Temperature at 4080 Mc/s

The route graph is a measurement pipeline. Instrument setup and reference calibration form the single independent root. Foreground accounting consumes that result. Residual detection then adds uncertainty, robustness checks, interpretation, and evidence transfer. Once detection is established, sky characterization, proof-stage spectral exclusion, and the tentative companion explanation proceed in parallel. A final route retains the calibrated measurement and conjoins all declared predecessor outputs, while the source map names excess detection itself as the principal conclusion.

The setup selects the 20-foot horn-reflector antenna, the zenith observation at 4080 Mc/s, a maser radiometer switching against a liquid-helium reference termination, the raw antenna signal, a contaminant model, and a suite of instrumental and sky checks. Impedance mismatch is negligible in the selected regime.

The Lean setup also realizes an available measurement procedure and records that it was actually performed. Those operational facts precede any conclusion that a physical background exists.

The foreground calculation uses elevation dependence and the atmospheric secant law to estimate atmospheric emission. It separately calculates ohmic heating and back-lobe pickup. The residual-temperature predicate then relates the total signal, selected contaminants, excess component, residual value, and uncertainty. ReportedAccountingValuesAt keeps the printed frequency and temperature budget as real-valued assignments rather than leaving the numbers only in prose.

The 0.8 K ohmic value is a central estimate with a reported 0.4 K error, not an exact physical loss. ForegroundErrors distinguishes reported centers, physical offsets and their explicit bounds. Subtracting central values with a strictly sub-0.1 K backlobe gives (3.5, 3.6] K; this is not the physical residual interval. If all three offsets obey the supplied component bounds, reported_component_bounds_control_actual_subtraction_error bounds the deviation from central subtraction by 1 K. The resulting conditional physical interval is (2.5, 4.6] K.

Concrete controls preserve every center and component bound. A 0.4 K ohmic offset gives a 1.2 K physical ohmic loss, 1.25 K antenna contribution and 3.15 K residual at a diagnostic 0.05 K backlobe. Opposed component offsets give 4.55 K, outside the separately reported 3.5 +/- 1.0 K interval. These are consequences of a specified additive hard-bound model, not new observations or a refutation of the paper's uncertainty estimate. The aggregate error model is independent; no confidence level or statistical independence is inferred.

The numerical budget is not obtained from the total temperature alone. total_temperature_does_not_supply_atmospheric_accounting formally blocks that shortcut when the secant-law calculation is missing. reported_accounting_values_balance_total_temperature checks the literal 6.7 = 2.3 + 0.9 + 3.5 arithmetic, while established_accounting_retains_reported_temperature_values projects the printed values from the checked accounting conclusion. reported_residual_uncertainty_interval_is_strictly_positive proves that the entire 2.5-to-4.5 K reported uncertainty interval remains positive, and established_accounting_retains_uncertainty_robust_positive_excess exposes this genuine excess from the completed accounting. reported_calibration_and_foregrounds_realize_measured_residual additionally realizes the actual 4080 Mc/s calibration, 0.3 K total uncertainty, 2.3 ± 0.3 K atmosphere, 0.8 ± 0.4 K ohmic loss, below-0.1 K back-lobe bound, rounded 0.9 K combined antenna contribution, and 3.5 ± 1.0 K residual. named_accounting_does_not_supply_reported_residual_value preserves that same measured calibration and foreground budget while setting only the candidate residual to zero; it is a physical countermodel, not a Boolean label. EstablishedCalibrationAndAccounting also retains the resulting background-separation fact, so later uncertainty and detection steps consume the checked accounting conclusion rather than replaying the subtraction.

After foreground separation, an uncertainty calculation assigns the residual uncertainty. The robustness calculation records negative seam-leakage and rotary-joint tests, bounds ground back-lobe pickup, applies the selected check suite, verifies residual stability, and concludes that the selected contaminants are insufficient within that uncertainty.

Detection still has two logical stages. First, a stable separated residual with insufficient contaminant account makes a background interpretation admissible. Second, a bridge turns that admissible interpretation into the physical predicate that the excess background is detected.

This detected excess is the source map's declared main conclusion. retained_accounting_and_detection_contracts_establish_excess_background_detection and retained_accounting_and_detection_contracts_record_residual_estimate rebuild detection and the operational residual value from retained accounting plus the declared uncertainty, robustness, interpretation, and bridge contracts. The route additionally establishes evidence for the residual model and transfers that evidence to the calibrated-observation theory through a named bridge.

Directional, polarization, and seasonal checks

The sky-characterization calculation consumes detection. Within the observations, the residual is isotropic, unpolarized, and stable over the observing interval.

The qualifiers matter. Isotropy is a characterization of the already accounted residual; it does not itself supply instrumental or atmospheric accounting. The countermodel isotropy_does_not_supply_instrumental_accounting preserves that direction of inference.

Note added in proof

A separate calculation retains the previous 404 Mc/s minimum-temperature measurement, the literal 16 K minimum, the 4080 Mc/s and 3.5 K residual values, and the source's no-steeper-than λ^0.7 ratio. The frequency ratio is the inverse-wavelength ratio; the formalization keeps the inequality as a sourced two-frequency bound, not a broadband fit. named_proof_stage_spectrum_does_not_supply_reported_formula retains both measured frequencies, both temperatures, and the positive formula domain while substituting exponent zero, showing that the measured comparison cannot manufacture the printed 0.7 exponent. Only then does the sourced route exclude radio-source classes then known because the spectra they would require are steeper.

The exclusion is now a Lean deduction, not an output assumed in ProofStageSpectralExclusionCalculation. Each candidate population has actual antenna-temperature values at the two selected frequencies. To account for the whole residual it must supply the high-frequency residual and contribute a nonnegative low-frequency temperature no larger than the observed minimum. A strictly steeper candidate then contradicts the retained temperature-ratio bound. Membership in the compared known-source family and its spectra are independent inputs; that family is required to be inhabited.

The interactive review includes two constructed controls: equality at the spectral bound permits a whole explanation, and a smaller steep component can remain inside both temperature budgets. The 2 K comparison used in these controls is not the historical 16 K and 3.5 K observation. The result does not exclude every partial radio contribution, establish a broadband power law, or identify a cosmological origin.

The article states that the companion Dicke et al. letter offers a possible explanation. The corrected Lean evidence relation leaves cosmological support to a separate assessment. Under the performed horn setup, companion_support_iff_separate_assessment identifies that remaining input exactly. The source does not supply its negation.

complete_result_does_not_depend_on_companion_support_assessment proves that changing this assessment leaves the complete paper result unchanged; the shared detection context is also definitionally unchanged. This structural independence does not decide support in either direction. companion_model_assignment_iff_separate_model_use likewise leaves cosmological model assignment to the existing explicit theory/model-use relation; it is not excluded by a constructor test.

ResidualOrigin.originRecordAccess supplies concrete scalar-attribution controls. Nonnegative cosmological/other components (3.5, 0) K and (0, 3.5) K yield the same 3.5 K residual. The record therefore forces neither a positive cosmological contribution nor its absence, and cannot identify an exact cosmological temperature. established_accounting_residual_does_not_identify_its_origin connects the actual retained residual value to those alternatives. They are not complete competing cosmologies, nor asserted solutions of the separate spectral assumptions. The other contribution is not the already-subtracted atmosphere or antenna loss, and is not identified with a known radio-source population.

A separate strict upper bound on all other residual contributions would force a positive cosmological remainder. The conditional Lean deduction retains that extra premise; the possibility statement supplies no such bound.

Mathematical residual and physical value

The residual-temperature functional is a mathematical object tied to the selected description. The recorded raw signal, foreground separation, detection interpretation, valid functional, and assigned residual form a concrete value-bearing estimate. Its center is not thereby the exact physical temperature. The actual-temperature relation is independent of the calculation; only a separately supplied faithfulness premise permits exact-value establishment.

complete_result_does_not_depend_on_exact_physical_temperature proves that changing the independent actual-temperature relation preserves the complete source result. recorded_estimate_allows_a_distinct_physical_temperature retains the same performed estimate and an inhabited alternative physical value while rejecting exact-value establishment. This does not assert that an arbitrary alternative is compatible with the error model. The stronger recorded_estimate_and_faithfulness_establish_exact_residual_value requires a separate faithfulness premise.

Operational access and evidence

The horn setup realizes an accessible procedure and an actually performed measurement. Adding the calibrated detection route yields the formal observer-independent-existence predicate for the excess background. The performed measurement supports the residual model, while an explicit transfer theorem carries that support to calibrated radio observation.

The shared model selects the description, horn, zenith observation, helium reference, raw signal, excess component, contaminant set, check suite, uncertainty, and regime. Applicability requires exact selected semantics and six successive inputs: setup, calibration, background separation, uncertainty assignment, robustness checks, detection interpretation, and the final detection bridge. At each calculated stage the adapter rebuilds the horn setup from shared validity, observation, reference, raw-record, contaminant, and check-suite facts plus the paper-local horn, switching, and impedance facts before rerunning the paper-local calculation.

The output-led established result is exact selected semantics plus NonvacuousCalibratedResidualBackgroundDetectionAt. It keeps the actual horn setup and all eight consumed detection outputs at one shared model; the six implication-valued calculations or bridges are reconstructed afterward.

calibrated_excess_realizes_controlled_experimental_detection projects the same established route into the neutral experimental-inference paradigm. The helium-reference calibration, separated residual, witnessed check suite, selected contaminant insufficiency, admissible interpretation, and physical detection are retained as distinct stages; no exhaustive claim about unselected contaminants is added.

The final theory–world step is conditional. horn_setup_realizes_shared_selected_setup first combines exact model retention with the actual horn setup. Grounding then separately requires that calibrated radio-observation theory use the selected model, that the model represent the selected zenith sky, and that every model claim transfer to both theory and physical-world predicates; no detection output is a premise.

The separate CompletePaperResult retains EstablishedCalibratedMeasurement and then conjoins accounting, detection, operational residual value, evidence transfer, sky characterization, spectral exclusion, and tentative explanation. The source-mapped main conclusion remains the detected excess itself.