00:00:00.000 01. Start here: question, model, comparison Welcome to G H U Lab. This revised walkthrough covers every menu section, the three Simulator modes and the embedded research experiments. It now demonstrates the S U seven certificates, approximation errors, uncertainty budget, thermal solver comparison, named collider references and the first Kaluza Klein gluon against L H C data. Every section and card also has a Demo button that runs a guided simulation. Choose a chapter to revisit a topic. The boundary research chapter now adds linked two and three-dimensional mass views, independent profiles and scoped anomaly diagnostics. Start with a named model or reference. Change one assumption at a time, and read the result with its units and scope. Theorem, verified, measured and unknown describe different kinds of evidence. A computed scenario value is not automatically an experimental measurement. 00:00:55.133 02. Hierarchy Open Hierarchy. For a bulk content of the S U seven model, inspect the compactification scale and Higgs mass under the displayed conventions. The ceiling belongs to the stated small-angle moment approximation. Change the diagnostic gauge coupling to zero point seven. The response plots separate a change of model convention from propagation of the measured W input and from winding convergence. Read the axes and the central values together. The calculated phase does not reproduce the printed phase. The mismatch varies between rows, and an overall multiplication of the potential cannot move its stationary points. Absolute scales remain conditional on resolving this discrepancy. The arithmetic identities are separate statements. Load the first certified benchmark. The table encloses two different stationary points: the quartic logarithmic approximation and the full Fourier minimum. Phase, Higgs mass and compactification scale have separate absolute and relative error intervals. They apply to the displayed matter content, gauge choice and fixed mass inputs. What limits the precision? Read approximation bias, root-location bounds and the Fourier remainder separately from the propagated W-mass uncertainty. The ten percent coupling variation is a chosen scenario, without an assigned probability. Physical theory uncertainty is explicitly not quantified; there is no combined physical error bar. Save the error certificate. The download keeps the rational enclosures, numerical budget, W input and attribution. The full mass enclosure already includes root and Fourier errors; do not add its half-width again. A different matter content or mass convention needs a matching certificate of its own. The ATLAS and C M S rows are separate published Higgs-mass references. Compare the certified curvature mass with each stated channel and error band. The listed difference is not an exclusion significance. Connecting a one-loop curvature mass to a measured pole mass still requires matching and higher-order uncertainties. The dataset links explain the route to a fuller comparison. Channels have not been combined into a likelihood. C E R N hosts the experiments and is not a third independent measurement. Archive the inputs and sources beside the result; a certified numerical calculation alone does not establish agreement with nature. 00:03:19.867 03. Design a scale Open Design a scale. The map run backwards: name a compactification scale and a Higgs-mass window, and get a bulk content that lands there — or a named certificate that none exists. Enter a target compactification scale of two teraelectronvolts and run the design. Inspect the returned content or the named certificate. A search budget is a stopping condition, not evidence that no solution exists. `budget` means the search stopped, not that the rung is empty; the page keeps the two apart on purpose. The reachable-set panel resolves each cluster into the finite set of points it really is. 00:03:58.867 04. Count a rung Open Count a rung. How many bulk contents sit on a rung — counted, not built. The counting graph is generated when the section opens. Click a different horizontal position to move the moment probe and compare counts across the rungs. These are counts of contents, not a list of experimentally viable models. The four published-seed totals reproduce an independent enumeration of 69 022 464 contents. The candidate uses even rungs and half-integral A₄; its counts are computed separately, without transferring the published measured-mass fibre. 00:04:37.133 05. Atlas Open Atlas. Every bulk content of at most five multiplets — 1 286 of them — with its potential drawn as one tile. Draw the lattice of one thousand two hundred and eighty-six contents. Each tile is a different potential. Inspect its colour and shape; a flat or blank potential is itself a result. Clicking a tile transfers that content to the model. One tile is green in the Higgs window, and it is the published row (2). A blank tile is a content whose potential is flat, and the harness predicts which tiles blank before they are drawn. 00:05:14.733 06. Same potential? Open Same potential?. Whether two bulk contents are the same one-loop potential, by Part VII's Theorem 3. Copy the first content and construct its canonical representative. Compare the potential curves and the five coordinates. Different lists of matter can produce exactly the same one-loop potential under the stated theorem. Same five coordinates ⟺ identically the same potential. The dashed curve riding exactly on the solid one is the theorem, not a coincidence. Load the equal-moment example and inspect the local range. These two contents have exactly the same D, A four and G through their integer coordinates, while their endpoint coordinate differs. Matching the small-angle expansion is a weaker condition than matching the complete potential. Switch to the full phase interval. The plotted full potentials separate even though the local expansions match. These curves illustrate finite Fourier sums; the exact coordinate statement and the interval proof are recorded separately. Use the full potential when judging a global vacuum. For content B, the endpoint at alpha equal to one has certified energy below its local minimum. This rules out that local minimum as global. It does not prove that the endpoint itself is global. Save the comparison to retain the exact inputs and the scope of this mathematical example. 00:06:38.933 07. Anomalies & proton Open Anomalies & proton. What each multiplet contributes to the anomaly bill, in eighths, and what the proton-decay escape costs. Read the signed contributions to the anomaly bill and the rung ladder. A nonzero bulk bill does not, by itself, make the theory inconsistent: possible brane matter must be considered separately. The research card later in this section studies a different warped model. A non-zero bill is not an inconsistency: brane fermions pay into the same channels with the opposite sign. What the ladder forbids is a rung, not a model. 00:07:16.267 08. Escape from proton decay Open Escape from proton decay. The escape from proton decay, constructed: type a brane content and watch the six channels, the assignments and the selection rule recompute. Choose the scalar charge associated with the eighty-four representation. The rational anomaly channels and charge assignments update together. Inspect which assignments meet the displayed proton-protection rule; the calculation does not supply a measured proton lifetime. Every assignment that protects the proton can also cancel all six channels — protection never costs an anomaly. That is an enumeration, not an argument. 00:07:55.467 09. Multiplets & parities Open Multiplets & parities. The layer under the term tables: every representation broken into multiplets with their three Z₂ parities. Select the eighty-four representation and change its parity assignment. The decomposition and parity picture update from the representation data. Use the table to connect a surviving zero mode with the sign of its potential contribution. The term tables here are DERIVED and then checked against the ones the rest of the page computes with. If the two ever disagreed, this panel is where it would show. 00:08:30.667 10. Screen a table Open Screen a table. Arithmetic screens for a published row, with conditional rung certificates and independent full-potential witness checks. Enter a candidate resonance at four thousand gigaelectronvolts. The comb samples nearby teeth for the displayed rungs. Its filters, spacing table and download now use the same conditional-bound check for the chosen inputs. A surviving tooth is not proof of an attainable physical vacuum. The moment ceilings remain conditional on the small-angle approximation. The five printed phase rounding intervals contain no stationary point for the implemented potential. All eight fermion coefficient tables now agree with an independent reconstruction. The physical gauge determinant and the origin of the printed numerical mismatch remain open. Expand Certified S U seven benchmarks. Twenty-six Lean theorems verify finite algebraic identities. Separate interval proofs certify ten global minima on the stated one-phase domain: five reference contents under each of two gauge prescriptions. These statements do not certify an arbitrary edited model. Download the certificate bundle. It contains rational enclosures, continuum partitions, checksums and reproduction records. The infinite Fourier analysis is computer-assisted and has not been formalized in Lean. A global-minimum certificate is conditional on its potential and assumptions; it is not a certificate of physical viability. The English dossier assigns the model to Komori and Maru, the expansion antecedents to Haba, Takenaga and Yamashita and to Sakamoto and Takenaga, and the S U seven application in Part Seven to Carles Marín. Verification does not establish originality. The dossier keeps the remaining physical questions explicit. 00:10:19.533 11. Collider Open Collider. Which state a dijet search bounds, plus a separate Higgs-rate scenario checked against pinned experimental datasets. Move the dijet mass probe to five point two. Read the selected state, mass scale and published comparison under its colour hypothesis. The separate Higgs experiment below uses another explicitly supplied scalar scenario. The dijet Δχ² values are quoted from the published record; the Higgs experiment computes its own comparison. Its 159 HiggsSignals observables are not 159 independent degrees of freedom. Coupling and width assumptions can compensate in visible rates, so this scalar comparison is not a complete GHU fit. The displayed recast table belongs to the earlier archived calculation. Separately, the dossier now records the C M S angular dataset at one hundred thirty-eight inverse femtobarns: seven distributions and seventy-seven bins. Integrity checks validate the imported tables. Importing them has not produced a new G H U fit. The released correlation matrix describes fitted signal strengths. It cannot automatically be used as the covariance of the normalized unfolded distributions. A new reinterpretation requires the G H U signal, selections and nuisance parameters, with a justified statistical model. The dossier distinguishes reviewed resources from analyses actually executed. 00:11:47.933 12. Selection rule Open Selection rule. Which α-domain a search may legally use, and which SU(4) representations can hold a quark generation. Select the representation with Dynkin labels one, zero, one. The centre-charge and chiral-projection results determine which search domain is permitted and which content can host a generation. The domain is computed from the representation, not chosen for convenience. The centre-charge gate is classical and is credited as such. What is ours is the chiral projection that gives the closed count. 00:12:23.333 13. Model calculator Open Model calculator. A matter content in, the Higgs out — the AHMN model recomputed in front of you. Load the named A H M N reference model. Its terms, potential and derived quantities are recalculated by the browser. Start with this anchored content before changing multiplicities or boundary signs, and retain the stated normalization caveat for absolute scales. The mass ratio carries no normalisation and no caveat. Absolute scales do. 00:12:56.867 14. eta-meter Open eta-meter. What the boundary sign η does to a multiplet's contribution — in closed form, from one integer. Load the supplied example made from a blind multiplet, then flip every eta sign. In this example the potential is insensitive to that change. The eta-difference view exposes the cancellation; it is not evidence that boundary signs never matter. In difference mode every blind multiplet goes blank. That is Part V's theorem seen without reading a number. 00:13:29.667 15. Five dimensions Open Five dimensions. Haba–Yamashita's own 5D SU(3) model, with the vacuum their paper leaves undone. Compare the pure-gauge case with the supplied marginal trio. Read the potential and vacuum together. This panel uses the five-dimensional S U three reference, so its arithmetic and assumptions must not be borrowed from the six-dimensional S U seven benchmark. Pure gauge never breaks the symmetry (D = −9). In this whole 5D class 8D is even: the odd rung the SU(7) ceiling stands on needs the sixth dimension. 00:14:06.533 16. SU(N) builder Open the S U N builder. Boundary conditions and supported bulk representations define the implemented one-loop Wilson-line potential in five dimensions. The model is the input. Load section four point three of the source paper. This pure-gauge example prefers the endpoint at one. Read the surviving group from the joint commutant: being at an endpoint does not prove that the generators at zero survive. The potential plot and the reported minimum now use the same V over C normalization. The four worked examples are checked against the implemented formulas. With one Wilson phase, the cosine terms admit the same moment construction. Its closed stationary branch is a small-angle approximation. The numerical Fourier minimum is a separate calculation, and a finite grid is not a certificate of the global minimum. 00:14:58.200 17. Paper models Open Paper models. Four models somebody else published, taken off their pages and run through this instrument's engine. Change the triplet Dirac-fermion count to five in the supported reference. Inspect which outputs are actually computed and which remain structural statements. Where offered, the load button transfers the supported content into the general builder. Three of the four are supersymmetric and this engine's potential is not, so their rows are boundary-condition and zero-mode statements only. An amber row disagrees with one printed equation, not with a paper, and names which of that paper's own equations agrees with which. 00:15:38.400 18. 4D spectrum Open 4D spectrum. What the model on the builder CONTAINS: the four-dimensional fields and their Kaluza–Klein towers. Load the S U six example and move the Wilson-line probe. Compare the potential families with the exact low-lying tower. The lowest levels can require a different reading from the families used to construct the potential. The cosine families reconstruct the potential, but do not by themselves determine every lowest level of the exact tower. The moved probe is a chosen phase, not necessarily a vacuum. Read its surviving group separately; a boundary coordinate alone does not determine symmetry breaking. 00:16:19.000 19. Anomalies Open Anomalies. What that content owes: every anomaly channel of the unbroken group, in exact rationals. Load the S U six example. The ledger evaluates each anomaly channel of the unbroken group in exact rational arithmetic. Distinguish a vanishing bill from a case with no massless fermions to test. Brane cancellation is a separate calculation. A non-zero row is a BILL, not an inconsistency: the brane fermions such a model needs pay into the same channels with the opposite sign. And a model with no massless fermion has nothing to cancel — that is `no subject`, not `cancels`. 00:16:59.000 20. Brane matter Open Brane matter. Who pays that bill, and what it costs: matter on the two fixed points, held at once to the anomaly ledger and to Part I's boundary-mass gate. Load the supplied S U five brane example and solve its supported linear charge channels. Compare the anomaly ledger with the surviving massless fields. Paying an anomaly bill and giving a field a mass are different requirements. Two verdicts, kept apart on purpose: the bill before and after, and the massless count before and after. The same field can pay one and not the other, because the charge that cancels an anomaly is not in general the charge a mass term needs. The surviving count is a lower bound — the rank test assumes generic couplings. 00:17:44.267 21. Scan Open Scan. Walk the displayed finite space of boundary conditions and matter contents through the selected filters. The breaking filter tests which generators at phase zero survive at the numerically located minimum. Run the displayed finite sweep. Read the denominator, each filter in the funnel, the survivors and the unresolved cases. The interface counts boundary conditions and equivalence classes separately, so surviving rows are not automatically distinct theories. Surviving boundary conditions are not surviving theories: [p,q,r,s] ~ [p−1,q+1,r+1,s−1] is the same theory, so the headline is a pair of numbers. An undecided vacuum is counted apart from a no. 00:18:28.867 22. One model, every verdict Open One model, every verdict. Which of the instrument's answers about this model are about the THEORY, and which only about the frame you are standing in. Start the built-in example, then choose its displayed equivalent boundary condition. Compare the tags identifying properties of the theory and properties of the chosen frame. A changed coordinate description can move a displayed quantity without changing the physical theory. The tags compare quantities in the evaluated frames. Read boundary coordinates and the surviving symmetry separately. Reported energies share the potential normalization. Numerical agreement between the located minima is evidence for these evaluations, not an exhaustive global-minimum certificate. 00:19:14.133 23. Simulator Open Simulator. Choose builder predictions, a top-KK Higgs-rate reference or the neutrino ring; compare calculated responses with their explicitly scoped experimental references. Load the published builder example and set the gauge coupling to one. Higgs masses now use analytic Fourier second derivatives, with an explicit truncation error bound. The export retains the actual coupling and phase, and distinguishes a chosen probe from a numerically located minimum. The thermal history belongs to a separate S U three benchmark and the stated supported regime. It is not a detector forecast or the thermal history of this builder. At commuting endpoints, the present mass dictionary does not identify a shifted W candidate to set the scale. That limitation does not imply that the phase-zero gauge group survives. 00:20:05.867 24. Boundary conditions Open Boundary conditions. Which boundary conditions are the same theory, walked as orbits rather than quoted as a theorem. Switch from the interval orbifold to the two-dimensional Z three example. The orbit structure and class count change with the specified boundary problem. Equivalence classes identify descriptions connected by the allowed transformations. The counts come out (N+1)² at every N on S¹/Z₂, which is Haba–Hosotani–Kawamura's theorem as a measurement. Press T²/Z₃ and the answer changes. 00:20:43.467 25. Classify an orbifold Open Classify an orbifold. The alphabet of an orbifold, derived from its rotation matrix and nothing else. Select the two-dimensional Z four rotation and classify it. The group-theoretic alphabet is derived from the matrix. You can enter another supported matrix, but an invalid finite-order hypothesis must be refused rather than silently classified. Nothing is entered but the matrix. A matrix of infinite order, or one whose characteristic polynomial is not a power of the m-th cyclotomic, comes back REFUSED rather than classified. 00:21:21.200 26. Name the relations Open Name the relations. Which equivalence relation on boundary conditions the literature already owns, and whether a proposed move set connects a class. Switch to the Z four boundary problem and judge the displayed proposed move. Read the local and global qualifications and the source attribution. A useful move in one boundary problem is not automatically a complete equivalence relation in another. The local/global distinction is the one that gets misquoted, and the page carries it explicitly. 00:21:54.133 27. Conjugate boundary conditions Open Conjugate boundary conditions. How many inequivalent CONJUGATE boundary conditions there are on S¹/Z₂ — and, because that count rests on a hypothesis nobody has settled, what each of the two answers would be. Increase the group rank and compare the two hypotheses printed in the table. Conjugate twists transform by congruence. Independent boundary transformations and one linked transformation lead to different classification questions, so the hypothesis travels with the count. What the panel puts on screen is the disagreement, not a number, and that is the point: the twists move by congruence rather than similarity, and independence decides between four classes flat in N and no finite count at all. What the label leaves unbroken is not a property of the label — the same verdict the ordinary panel reaches by another route. The exported card carries the hypothesis beside the count, so a number never travels without the condition it rests on. 00:22:52.133 28. Brane kinetic terms Open Brane kinetic terms. What happens to the tower when brane-localised kinetic terms make the masses stop being n/R. Increase the brane kinetic coefficient to twelve. The spectrum responds because the roots are no longer a simple integer tower. Compare the root conditions and normalization, then use the separate warped-unification card for coupling-running questions. The special functions are checked against mpmath at forty digits, and the c → 0 limit is computed in closed form by code that shares nothing with the solver. That limit found three real defects. 00:23:29.333 29. Gravity–gauge · 3D Open Gravity–gauge · 3D. Which physical information a complete tower of masses leaves undetermined in a controlled gravity-gauge example. Select eta equal to minus zero point nine, then display the gauge kinetic function. The paired masses and the source response carry different information. The Wilson quantity here is a kinetic normalization, not a Higgs-mass prediction. The positive paired tensor NN and vector DD masses are protected by their common canonical operator. The gauge NN control has different boundaries and moves. The source position is in the extra dimension, not a laboratory location; the Wilson kinetic scale is not a Higgs mass. For p=1.1 a canonical bulk scalar realizes the family, with stability and cutoff still open. 00:24:18.600 30. The literature Open The literature. The reading list behind the series: what each paper publishes, and which ones a person has actually read. Filter the reading list to the complete-triple selection. Inspect the recorded sources and what each paper actually supplies. Keyword signals help navigate this corpus; they are not proofs, and this reading list is not an exhaustive map of the field. A signal is a keyword, and a keyword sweep misses whatever is phrased differently. Nothing is asserted from a signal alone, and the corpus is our reading list rather than the field. 00:24:55.533 31. Simulator: top-KK Higgs production The second Simulator mode is the top Kaluza Klein Higgs-production reference. Its leading rate, finite tower and resummed comparison answer one specified model question. Move the Kaluza Klein scale to fifteen hundred gigaelectronvolts. Inspect the rate curve and the separate convergence display. The chosen comparison window is conditional, and a custom window is a user-supplied scenario. 00:25:22.200 32. Simulator: the neutrino ring Select the four-dimensional neutrino ring. Calibration can hold the light mass and active-current deficit fixed while the required couplings are reconstructed. Six heavy pairs belong to this base model. Compare mu B equal to zero with five thousand kilo electron volts. The leading light mass and the heavy pair splittings carry different information. Read the approximation indicators alongside the spectrum. 00:25:49.333 33. CMS heavy-neutral-lepton references The CMS comparison uses published observed and expected curves with their bands. The overlay keeps the selected flavour and Dirac or Majorana hypothesis visible. Choose muon flavour and the Majorana reference. Inspect the per-component convention, mass domain and reference ratios. The ring overlay is not a likelihood that includes its complete flavour structure, decay acceptance and multi-state interference. 00:26:17.067 34. Decays, Majoron channels, flight and coherence The decay card starts from the weak-channel scenario. Select a heavy pair and inspect where its width goes, its lifetime and the fixed-boost flight estimate. Include the calculated Majoron channels. The width and the derived lifetime respond together. An extra width is a separate user hypothesis. Read the isolated-pair and overlap diagnostics before interpreting the same-sign over opposite-sign ratio. Change the fixed boost to ten and inspect the flight curve. This illustrates the supplied kinematic scenario; it does not integrate a detector acceptance or a production spectrum. 00:26:55.333 35. Three active flavours and vacuum oscillations Three sterile copies reconstruct the chosen light masses and mixing orientation. The mass ordering, phases and active deficits are inputs. The card also displays eighteen heavy-pair flavour weights. Change the Dirac phase to ninety degrees. Compare neutrino and antineutrino appearance in the unitary vacuum limit, then inspect the flavour fractions. Majorana phases cancel from these oscillation curves but can affect the displayed light-sector double-beta quantity. 00:27:26.200 36. Fixed light inputs: what can distinguish the ring? This experiment holds the chosen light masses and mixing orientation fixed while reconstructing a parameter path. The green strip tells you what is fixed. The five figures separate heavy masses, splitting, current factors, small differences and reference data. Move the selected position from one tenth to eight tenths along the mu B path. The mass stays fixed while the pair splitting changes. The open circle tracks the selected point. Equal light inputs therefore do not determine every heavy-sector response. Now choose the common active deficit and its upper endpoint. The raw vacuum current factor is suppressed, but the specified near normalization cancels the common factor. The difference figure labels numerical coincidence rather than amplifying roundoff. Choose deficit direction three. Unequal deficits can leave a shape response. The fourth graph magnifies an absolute difference that is difficult to see in the overlapping curves. Its scale is explicit, and the exported samples retain their original precision. The DeepCore map uses the archived twenty-eighteen standard-three-neutrino tables. The cross stays fixed along the ring path because these light inputs stay fixed. The map is not a nonunitary ring likelihood and is not added to NuFIT. To move the cross, change sine squared theta twenty-three in the flavour card. Here it is set to zero point six. The reference updates for the new light input. Outside its published grid the laboratory withholds a value instead of extrapolating. 00:29:01.600 37. Maru–Nago SU(6): content and convergence This paper-model experiment reconstructs the stated flat S U six potential. Matter content and the winding cutoff are explicit controls. A small Wilson minimum must be read with its convergence check. Set the winding cutoff to ten and inspect the shifted minimum and comparison. A finite truncation can change the apparent result. The supported potential can be transferred to the builder; this does not certify a complete flavour model. 00:29:30.400 38. Warped SU(6): differential gauge running The warped-unification card compares differential gauge running under the selected matter assignment. Required ultraviolet boundary terms and their residuals are outputs of that stated approximation. Switch the matter assignment to C two. The running differences and required boundary terms respond. The naive-dimensional-analysis reference is a scale estimate. The separate localization probe is not a complete fermion-spectrum calculation. 00:29:58.800 39. Thermal potential and phase coexistence The thermal card is its own S U three benchmark. It uses named paper cases and compares potential cutoffs. A stored matching PhaseTracer result is available offline for the recorded inputs. Load paper case two and compare the potential and phase flow. Coexistence and a nucleation proxy are different questions. A new point needs a matching bounce calculation; changing the builder model does not turn this benchmark into its thermal history. The new comparison runs PhaseTracer and CosmoTransitions on the same S U three potential and canonical field. Nine matched temperatures compare the bounce action. The programs share shooting-method ancestry, so agreement is a numerical cross-check, not an independent interval proof or an experimental validation. The table changes the spatial and thermal Fourier cutoffs together. T one-forty solves S three over T equal to one hundred forty. It is a proxy, separate from the integrated nucleation and percolation results. The older displayed proxy used a looser shooting tolerance; compare like settings before interpreting a difference. Open the numerical diagnostics. Tolerance shifts, profile sampling and the virial residual test different aspects of the calculation. The targets are numerical criteria, not confidence levels. Higher loops, thermal resummation and plasma dynamics remain unquantified. These S U three examples are separate from the S U seven mass certificates. Change the coupling away from the reference. The archived solver comparison disappears because all thermal inputs must match. A stale certificate must not follow an edited point. Load a named paper case again to recover its evidence; a new point needs a new calculation. Reload case two and save the experiment JSON. It retains both solver versions, tolerances, cutoffs and sources. The thermal potential is credited to Hirose and Shibuya, CosmoTransitions to Carroll Wainwright, and PhaseTracer to Athron and collaborators. Keep this provenance with every exported result. 00:32:06.333 40. Nucleation, percolation and conditional waves Integrated transition history uses refined action tables. Read nucleation, percolation and completion separately. The false-vacuum fraction and physical-volume condition make those distinctions visible. Set the assumed wall speed to zero point eight and the fluid efficiency to zero point one. Compare the history and conditional acoustic spectrum. Wall friction, plasma evolution and detector significance are not calculated by these controls. 00:32:35.933 41. RS anomaly flow and baryon current This warped-model experiment separates ultraviolet and infrared anomaly factors, gauge cancellation and the baryon-current matrix. Its sources and approximation are distinct from the base S U seven ledger. Remove the lepton generations in this test configuration. The imbalance exposes a gauge anomaly that needs completion. A nonzero baryon-current anomaly is a separate statement; it is not a computed proton lifetime or baryogenesis yield. 00:33:05.267 42. Higgs rates and matching experimental tests Begin with the stored Standard Model-like scalar reference. Local couplings determine production rates, partial widths and branching fractions. Matching HiggsBounds and HiggsSignals calculations use pinned experimental datasets. Add one mega electron volt of invisible width. The local predictions update, and the old experimental result is withdrawn because its inputs no longer match. Run the optional engine or import a matching result before assigning a new experimental verdict. 00:33:36.867 43. First KK gluon at the LHC Every menu section, Simulator mode and experiment card now has a Demo button, marked with a film clapper. It presses the real controls, explains each step in a banner, and ends with how to read the result. Here the Kaluza Klein gluon card starts its own demo. Stop the demo and take over: load the published R S point of Casagrande and collaborators, with all nine of its quark bulk masses. The card computes the couplings of a warped Kaluza Klein gluon to zero-mode quarks, its width and branching fractions, and compares its leading-order rates with the ATLAS top-pair limit and the C M S dijet limit as r, prediction over limit. At three point seven five tera electron volts, r for the top pair is close to one: the two thousand eight reference point sits at the edge of the ATLAS comparison. That is a comparison with ATLAS's thirty percent width benchmark, not a validated exclusion at this width. Below the plots, the top-pair mass spectrum is computed with the interference between the Kaluza Klein gluon and the Q C D gluon, in the fifteen bins of the C M S parton-level measurement. For this point the light-quark and top couplings have opposite signs, so the interference is constructive below the pole. Now load the flat G H U coloron at four point five tera electron volts. Every quark couples equally, the couplings share one sign, and the interference turns destructive: the low bins go down instead of up. The last plot is the expected delta chi squared against the measured covariance, with ten percent S M theory uncertainty per bin. Set that uncertainty to zero and the reach moves from about three point eight to about five tera electron volts. With the same ten percent taken as one correlated normalisation, delta chi squared would be five point three instead of one point eight: the reach depends on that assumption, and the card shows both. It is a sensitivity if the data equal the S M, not an exclusion, and the open certificates show the independent Dirac-trace and L H A P D F check. 00:35:38.267 44. Boundary research: linked 2D / 3D diagnostics The boundary research card separates four questions: a fermion mass gap, independent profiles, parity-inserted traces and a restricted six-dimensional tensor condition. Load the research baseline. These are diagnostic tools, not a completed particle model. The two-dimensional map shows the lightest paired mass. The horizontal axis is boundary coupling and the vertical axis is the imposed Wilson angle. Darker means larger mass, on the fixed colour scale. The white point is the selected calculation and the red line fixes the coupling for the curve below. Select or drag a point, then release to update the input values. Switch to the three-dimensional surface. Height and colour encode exactly the same mass data as the map. Change the viewing angle to see the surface clearly; that angle changes the camera, not the physics. Selecting the surface uses the nearest sampled node. The map remains available for precise selection. Return to the map and set the boundary coupling to zero. The first normal root vanishes, and the paired and unpaired curves coincide. Restoring coupling one opens a normal gap of about zero point two seven four in units of inverse radius. The Wilson angle is supplied here; this calculation does not find the vacuum. Set the separate profile example to zero mass. One Gram eigenvalue becomes numerically zero, so these three profiles span only two independent directions. The bars use a linear scale and the printed values show their size. A numerical threshold is displayed above them. Restore profile mass one. All three eigenvalues are positive, despite nonzero overlaps. Overlap means the profiles are not orthogonal; dependence would require a null direction. This example tests linear independence, not the origin of three physical families. Switch from the six-dimensional corner insertion to the four-dimensional intersection insertion. The exact trace table changes. A nonzero evaluation detects a nonzero polynomial, but a zero at one probe cannot establish cancellation. Local normalization, mirror contributions and anomaly inflow are still required. One identical six-dimensional family with opposite lepton chirality fails the restricted doublet condition. Three families pass. The condition allows multiples of three; it does not select exactly three, and it is not the full anomaly test of the higher-dimensional orbifold. Keep the assumptions with the result. Save the card data to preserve every input, the sampled mass grid, exact moments, sources and unresolved requirements. The guide explains the equations, examples, controls and failure cases. The overall quantum consistency remains an open research question. 00:38:28.867 45. Keep the inputs, figures and scope Use a comparison snapshot before changing a point. Save the experiment JSON to retain the inputs, calculated arrays, assumptions, provenance and optional saved reference. The global result card and LaTeX exports provide another view of the selected calculation. Choose a figure and save its vector SVG. The new neutrino figures carry sampled data and provenance in their metadata. The link button preserves controls in the address; archive external results and comparisons in JSON as well. The browser calculations and stored references run offline. New HiggsTools and PhaseTracer points use the optional local engine. The source repository contains the reproduction commands, independent checks and archived studies. Return to a chapter, vary one assumption, and keep the scope beside every result. 00:39:22.400 46. Quantization and certificates Open Quantization and certificates in the new research menu. These are independent diagnostics, with exact rational inputs and separate assumptions. The guided demo changes real controls. A passing arithmetic criterion is one ingredient of consistency. It does not certify a complete gauge Higgs model. Choose C over two. The universal class fails, while periods on closed spin four manifolds pass. This is not a contradiction. The tests use different backgrounds. The universal test detects a period of one half. On the stated spin backgrounds, the period of Y squared is even. That topological fact is external to the Lean arithmetic proof. The diamonds are universal integral classes. The rings between them pass only the closed spin four period test. The cross marks the current alpha and delta, at fixed beta. Select a lattice point in the application and the input gamma changes exactly. These are mathematical criteria, not experimental measurements. Outside the displayed window, the interface reports the exact coordinates instead of clipping a point to the border. Now choose C over thirty six. The covering direction gives an integer, one. But the displayed quotient cocharacter gives one over thirty six. Checking a convenient covering direction can miss a forbidden period. Read the witness together with the criterion. The application uses exact fractions, not a floating point tolerance. Choose A plus B. Alpha and beta are one; gamma is seven twelfths. After changing to the integral basis, delta is zero. Both criteria pass. The fractional contributions have to be combined before judging the total class. The controls, the witness and the exported result all use the same calculation. The axion panel uses the normalization of Choi and collaborators. The integer combination eighteen K two plus twenty four K three plus K one must be divisible by thirty six. The default zero, one, twelve satisfies it. This reproduces the published q equals six condition. Identifying this axion with the gauge Higgs field remains a separate, unresolved physical question. The parent map has two columns and a common annihilator. With the inherited spectrum and ordinary integral Green Schwarz sources, six times the annihilator is sixteen minus three p minus three q minus six r. For integer pairings it is one modulo three, so it cannot vanish. Lean proves that arithmetic for all integers. Allowed orbifold backgrounds and extra corner responses are not settled by this result. The U two example shows why joint integrality differs from separate factor requirements. With b zero equal to one and b one equal to six, the quadratic form is m squared plus m n plus n squared. It is integral for every integer pair. The formal criterion also covers rational coefficients with a common nonzero denominator. This example is not an anomaly free supergravity spectrum. Change b one from six to five. Each cell is a cocharacter labelled by integers m and n. Its printed fraction and color are Q modulo one, calculated with exact integer arithmetic. The point one, zero now has period seven eighths: a concrete witness of failure. Returning b one to six makes every cell integral. The eighty one cells illustrate the criterion; the Lean theorem establishes it for all integer pairs. For the Spin twenty audit, the degree eighteen Clifford element squares to minus one. Multiplication by minus i makes the representation matrix square to plus one. This distinction matters for an ordinary isotropy lift. It does not prove the model inconsistent: a twisted or combined action may be possible. Every field and interaction, including bosonic Omega, must share a specified action. The catalogue now includes five Lean files with fifty nine theorem declarations. A theorem is a statement checked under explicit assumptions. The ten hypothesis algebra declarations have their own scope. Download the evidence, verify its file hashes and repeat the listed checks. File integrity, numerical agreement and mathematical proof answer different questions; none alone establishes a complete physical model. 00:43:45.467 47. Hypotheses: response, measurements and certificates Open the hypothesis card inside Same potential. It brings together four views with two separate scientific contexts: nine recalibrated gauge Higgs models and one measured C M S spectrum. Each selection includes an interpretation. The card does not yet fit these models to the measurement. Choose case one. The square marks the reference in parameter space. The potential difference is exactly zero because the reference is compared with itself. The horizontal variable is the field phase theta. The vacuum phase remains fixed at zero point one. Change to case six. The labels c F and m V name two parameters of the fermion sector in this model. Several inputs change together and were recalibrated to preserve the vacuum and Higgs mass. Lambda three and lambda four describe the cubic and quartic response near that vacuum. They are calculated outputs. Read their percentage changes below the figures: this compares complete cases, not one isolated parameter. Expand the field interval. Each potential has its own vacuum value subtracted; we then subtract case one and divide by the same mass and field scale. The vertical exponent changes with the interval. A small local difference can coexist with a different shape away from the vacuum. Lines connect calculated samples; they do not prove a global minimum. Select the last measured mass interval. C M S reports a differential top pair cross section at thirteen tera electron volts. The vertical axis is logarithmic. Vertical bars show total marginal uncertainties; horizontal bars show bin widths. These are measured cross sections, unlike the observed resonance upper limits in other cards. Set the two interval selectors equal. Their correlation is one by definition. Now choose the neighbouring interval. The sign and magnitude describe how experimental errors move together, not how similar two physical models are. Combining bins requires the complete covariance matrix, which is included in the JSON export. Open Certificates. Lean is a proof assistant: it checks the mathematical steps of a stated claim. Ten additional declarations check rational algebra used by the hypothesis study. A separate exact calculation verifies the published covariance matrix. Read each row from left to right: what is checked, what evidence supports it, and where that guarantee stops. A correct identity does not establish that a physical model describes nature. Three rational interval probes bound logarithm derivatives through fourth order. They exclude the error in the Bessel functions and the full integral. Quadrature refinement remains a convergence diagnostic. The global minimum, omitted physical sectors and the roughly seven point four percent quartic fit discrepancy remain open. Read the pending items before interpreting agreement. Save the inputs and results as JSON, and download the certificate evidence. The JSON preserves the selected cases, measured bins, full covariance, sources and scientific scope. Importing this file restores a valid selection against the bundled references. It does not import a new measurement or accept a verdict from another file. Use the certificate catalogue for the replay scripts and source hashes. Now try a comparison yourself. Choose another case and read which inputs changed, how the two couplings responded and where the potential differs. Then choose two measured intervals and explain their correlation in words. Save your selection with its sources. Before claiming that data distinguish the models, identify the missing prediction and its uncertainties. The Demo button repeats this walkthrough and the information buttons explain each card.